論文の概要: The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version)
- arxiv url: http://arxiv.org/abs/2507.00595v1
- Date: Tue, 01 Jul 2025 09:25:54 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-07-03 14:22:59.555263
- Title: The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version)
- Title（参考訳）: The Secrets Not Flow: 大規模コードベースへのセキュリティ検証のスケーリング(拡張バージョン)
- Authors: Linard Arquint, Samarth Kishor, Jason R. Koenig, Joey Dodds, Daniel Kroening, Peter Müller,
- Abstract要約: 我々はプロトコルの実装をプロトコルの実装と残りの実装に分割する*Diodon*と呼ばれる方法論を開発します。
この分割により、セキュリティクリティカルなCoreに強力な半自動検証技術を適用することができます。
完全な自動静的解析は、アプリケーションがCoreで証明されたセキュリティプロパティを無効にできないことを保証することで、検証全体を拡張します。
署名付きDiffie-Hellmanキー交換の実装と、キー交換プロトコルを実装する大規模(100k+LoC)プロダクションGoの2つのケーススタディでDiodonを評価した。
- 参考スコア（独自算出の注目度）: 6.595258607341775
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Existing program verifiers can prove advanced properties about security protocol implementations, but are difficult to scale to large codebases because of the manual effort required. We develop a novel methodology called *Diodon* that addresses this challenge by splitting the codebase into the protocol implementation (the *Core*) and the remainder (the *Application*). This split allows us to apply powerful semi-automated verification techniques to the security-critical Core, while fully-automatic static analyses scale the verification to the entire codebase by ensuring that the Application cannot invalidate the security properties proved for the Core. The static analyses achieve that by proving *I/O independence*, i.e., that the I/O operations within the Application are independent of the Core's security-relevant data (such as keys), and that the Application meets the Core's requirements. We have proved Diodon sound by first showing that we can safely allow the Application to perform I/O independent of the security protocol, and second that manual verification and static analyses soundly compose. We evaluate Diodon on two case studies: an implementation of the signed Diffie-Hellman key exchange and a large (100k+ LoC) production Go codebase implementing a key exchange protocol for which we obtained secrecy and injective agreement guarantees by verifying a Core of about 1% of the code with the auto-active program verifier Gobra in less than three person months.
- Abstract（参考訳）: 既存のプログラム検証器は、セキュリティプロトコルの実装に関する高度な特性を証明できるが、手作業を必要とするため、大規模なコードベースに拡張することは困難である。
我々は、コードベースをプロトコル実装(*Core*)と残りの(*Application*)に分割することで、この問題に対処する*Diodon*と呼ばれる新しい方法論を開発します。
この分割により、セキュリティクリティカルなCoreに強力な半自動検証技術を適用できますが、完全に自動的な静的解析は、アプリケーションがCoreで証明されたセキュリティプロパティを無効化できないことを保証して、コードベース全体に検証をスケールします。
静的解析は*I/O独立性*、すなわちアプリケーション内のI/O操作がコアのセキュリティ関連データ(キーなど)とは独立であり、アプリケーションがコアの要件を満たすことを証明することによって達成される。
最初に、Diodonがセキュリティプロトコルに依存しないI/Oを安全に実行できるようにし、次に、手動による検証と静的解析がうまく構成できることを示し、Diodonのサウンドを証明しました。
署名されたDiffie-Hellmanキー交換の実装と大規模な(100k+LoC)プロダクションGoコードベースの2つのケーススタディでDiodonの評価を行った。
関連論文リスト
- Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
Etherscanの78,047,845のスマートコントラクトがデプロイされているにも関わらず(2025年5月26日現在)、わずか767,520 (1%)がオープンソースである。
この不透明さは、オンチェーンスマートコントラクトバイトコードの自動意味解析を必要とする。
バイトコードを可読でセマンティックに忠実なSolidityコードに変換する,先駆的な逆コンパイルパイプラインを導入する。
論文 参考訳（メタデータ） (2025-06-24T13:42:59Z) - Strands Rocq: Why is a Security Protocol Correct, Mechanically? [3.6840775431698893]
StrandsRocq は Coq のストランド空間の機械化である。
新しい証明技法と、新しい最大貫入器の概念が組み込まれている。
これは2つの単純な認証プロトコルに対するセキュリティの合成証明を提供する。
論文 参考訳（メタデータ） (2025-02-18T13:34:58Z) - Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。
RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。
これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。
我々は、無害な」知識基盤の著作権保護の名称を提案する。
論文 参考訳（メタデータ） (2025-02-10T09:15:56Z) - Formal Verification of Permission Voucher [1.4732811715354452]
Permission Voucher Protocolは、分散環境におけるセキュアで認証されたアクセス制御のために設計されたシステムである。
この分析では、重要なセキュリティ特性を評価するために、象徴的検証のための最先端のツールであるTamarin Proverを使用している。
結果は、メッセージの改ざん、偽装、リプレイなどの一般的な攻撃に対するプロトコルの堅牢性を確認する。
論文 参考訳（メタデータ） (2024-12-18T14:11:50Z) - Generalized Quantum-assisted Digital Signature [2.187441808562386]
本稿では,デジタル署名のためにQKDキーを採用することで,情報理論のセキュリティを継承する手法の改良版を提案する。
偽造に対するセキュリティは、悪意のある偽造者によって取られた試行錯誤アプローチを考慮して計算され、GQaDSパラメータは偽造と鑑定確率のバランスをとる分析的アプローチによって最適化される。
論文 参考訳（メタデータ） (2024-06-28T15:04:38Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。
本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。
実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
論文 参考訳（メタデータ） (2024-01-19T14:52:04Z) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
信頼性コンピューティングは、Trusted Execution Environments(TEEs)と呼ばれる特別なハードウェア隔離ユニットを使用して、コテナントクラウドデプロイメントにおける機密コードとデータの保護を可能にする。
低レベルのC/C++ベースのツールチェーンを提供するTEEは、固有のメモリ安全性の脆弱性の影響を受けやすく、明示的で暗黙的な情報フローのリークを監視するための言語構造が欠如している。
私たちは、Haskellに埋め込まれたドメイン固有言語(cla)であるHasTEE+を使って、上記の問題に対処します。
論文 参考訳（メタデータ） (2024-01-17T00:56:23Z) - Secure Synthesis of Distributed Cryptographic Applications (Technical Report) [1.9707603524984119]
我々はセキュアなプログラムパーティショニングを用いて暗号アプリケーションを合成することを提唱する。
このアプローチは有望だが、そのようなコンパイラのセキュリティに関する公式な結果はスコープに限られている。
我々は、堅牢で効率的なアプリケーションに不可欠な微妙さを扱うコンパイラのセキュリティ証明を開発した。
論文 参考訳（メタデータ） (2024-01-06T02:57:44Z) - Simple and Rigorous Proof Method for the Security of Practical Quantum
Key Distribution in the Single-Qubit Regime Using Mismatched Basis
Measurements [0.2519906683279153]
量子鍵分配(QKD)プロトコルは、2つのパーティが秘密の共有鍵を生成できるようにすることを目的としている。
理論上、多くのQKDプロトコルは無条件で安全であることが証明されているが、実験的なQKD実装の実際のセキュリティ分析は、可能なすべての抜け穴を考慮していないのが一般的である。
本稿では、離散変数QKDの実用的な実装に対して、安全な鍵レートを計算するための簡単な方法を提案する。
論文 参考訳（メタデータ） (2022-08-29T17:37:58Z) - Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。
我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文 参考訳（メタデータ） (2022-03-03T10:07:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。