Fugu-MT 論文翻訳(概要): Formalization of security

論文の概要: Formalization of security

arxiv url: http://arxiv.org/abs/2607.28551v1
Date: Thu, 30 Jul 2026 17:21:14 GMT
ステータス: 翻訳完了
システム内更新日: 2026-07-31 21:37:00.690155
Title: Formalization of security
Title（参考訳）: セキュリティの形式化
Abstract要約: 証明アシスタントを使用する動機は、認証をサポートすることである。この章は、システムセキュリティ、言語ベースのセキュリティ、セキュアコンパイル、暗号化への彼らの応用に焦点を当てている。
参考スコア（独自算出の注目度）: 6.725489768165861
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Proof assistants are often used to validate that designs and implementations meet their expected security properties. A further motivation for using proof assistants is to support certification. This chapter focuses on their applications to system security, language-based security, secure compilation, and cryptography.
Abstract（参考訳）: 証明アシスタントは、しばしば、設計と実装が期待されるセキュリティ特性を満たすことを検証するために使用される。証明アシスタントを使用する動機は、認証をサポートすることである。この章は、システムセキュリティ、言語ベースのセキュリティ、セキュアコンパイル、暗号化への彼らの応用に焦点を当てている。

関連論文リスト

Safeguards Based on Copyable Context Cannot Provide Reliable Safety for LLMs [61.39153106347947]
大規模な言語モデルのセーフガードは、答えがどのように使われるかを見る前に、答えるかどうかを決定する。同じ回答は、認定されたプロフェッショナルやアタッカーを助け、攻撃者は、良心的な要求とインタラクション履歴を模倣することができる。我々は、下流での使用に関する証拠からモデルがリリースした能力を分離する。その証拠がコピー可能である場合、有効な回答を保ちながら、アタッカー支援の正確な最悪のフロアを導出する。
論文参考訳（メタデータ） (2026-07-30T09:59:08Z)
Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin [0.9339654135645749]
セキュリティは、現代のデジタルシステムに依存するものすべてにとって重要だ。 ProVerifやTamarinといったツールは、自動検証を行うために広く利用されている。この研究は、理論的セキュリティプロパティ定義と実用的で実行可能な検証モデルの間のギャップを埋めることによって、技術の現状を前進させる。
論文参考訳（メタデータ） (2026-05-28T06:57:08Z)
SecPI: Secure Code Generation with Reasoning Models via Security Reasoning Internalization [50.71047638695205]
RLM(Reasoning Language Model)は、プログラミングにおいてますます使われている言語モデルである。しかし、最先端のRLMでさえ、生成されたコードに重大なセキュリティ脆弱性を頻繁に導入する。我々は、構造化されたセキュリティ推論を内部化するためのRTMを教える微調整パイプラインであるSecPIを提案する。
論文参考訳（メタデータ） (2026-04-04T04:29:11Z)
A Framework for Formalizing LLM Agent Security [46.86073273904095]
LLMエージェントのセキュリティは本質的にコンテキスト的です。 LLMエージェントに対する既存のセキュリティ攻撃の定義は、しばしばこの文脈の性質を捉えない。本稿では,文脈的セキュリティの観点から,既存の攻撃と防御を体系化するフレームワークを提案する。
論文参考訳（メタデータ） (2026-03-19T21:01:49Z)
From Detection to Prevention: Explaining Security-Critical Code to Avoid Vulnerabilities [2.490168997159702]
この研究は、セキュリティクリティカルな機能を実装するコード領域を強調することによって、脆弱性を防止するための積極的な戦略を探求する。コードレベルのソフトウェアメトリクスを使用してセキュリティクリティカルなメソッドを識別するIntelliJ IDEAプラグインのプロトタイプを提示する。
論文参考訳（メタデータ） (2026-01-31T13:16:01Z)
Tit-for-Tat: Safeguarding Large Vision-Language Models Against Jailbreak Attacks via Adversarial Defense [90.71884758066042]
大きな視覚言語モデル(LVLM)は、視覚入力による悪意のある攻撃に対する感受性という、ユニークな脆弱性を導入している。本稿では,脆弱性発生源からアクティブ防衛機構へ視覚空間を変換するための新しい手法であるESIIIを提案する。
論文参考訳（メタデータ） (2025-03-14T17:39:45Z)
A Taxonomy of Functional Security Features and How They Can Be Located [12.003504134747951]
本稿では,一般的なセキュリティフレームワークにおける文献のセキュリティ機能とそのカバレッジについて述べる。我々は,広く使用されているセキュリティ標準へのマッピングを含む,68の機能的実装レベルのセキュリティ特徴の分類に貢献する。
論文参考訳（メタデータ） (2025-01-08T12:17:30Z)
Formal Verification of Permission Voucher [1.4732811715354452]
Permission Voucher Protocolは、分散環境におけるセキュアで認証されたアクセス制御のために設計されたシステムである。この分析では、重要なセキュリティ特性を評価するために、象徴的検証のための最先端のツールであるTamarin Proverを使用している。結果は、メッセージの改ざん、偽装、リプレイなどの一般的な攻撃に対するプロトコルの堅牢性を確認する。
論文参考訳（メタデータ） (2024-12-18T14:11:50Z)
CodeChameleon: Personalized Encryption Framework for Jailbreaking Large Language Models [49.60006012946767]
パーソナライズされた暗号化手法に基づく新しいジェイルブレイクフレームワークであるCodeChameleonを提案する。我々は、7つの大規模言語モデルに関する広範な実験を行い、最先端の平均アタック成功率(ASR)を達成する。 GPT-4-1106上で86.6%のASRを実現する。
論文参考訳（メタデータ） (2024-02-26T16:35:59Z)
(Security) Assertions by Large Language Models [25.270188328436618]
セキュリティのためのハードウェアアサーション生成において,コード生成に新たな大規模言語モデル(LLM)を用いることを検討する。我々は、人気のあるLCMに注目し、プロンプトの様々なレベルの詳細を考慮し、アサーションを箱から書き出す能力を特徴付ける。
論文参考訳（メタデータ） (2023-06-24T17:44:36Z)
Secure access system using signature verification over tablet PC [62.21072852729544]
我々は,シグネチャ検証を用いたWebベースのセキュアアクセスのための,高度に汎用的でスケーラブルなプロトタイプについて述べる。提案アーキテクチャは,様々な種類のセンサや大規模データベースで動作するように容易に拡張することができる。
論文参考訳（メタデータ） (2023-01-11T11:05:47Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。