論文の概要: Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
- arxiv url: http://arxiv.org/abs/2609.15648v1
- Date: Mon, 14 Sep 2026 14:32:51 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-16 07:15:06.437976
- Title: Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
- Title（参考訳）: Aeneas、Rust、Leanによる暗号化ソフトウェアのスケーリング検証
- Abstract要約: Rustで書かれた暗号ソフトウェアを検証するための新しい方法論を開発した。
Rustのオーナシップの規律により、Aeneas氏は、リーンでこのコードの純粋なモデルを取り出すことができる。
エージェントは、Leanカーネルによって独立して検証される形式的な証明を、自律的に記述する。
- 参考スコア（独自算出の注目度）: 36.30712689467804
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We develop a new methodology for verifying cryptographic software. We target production code written in Rust for performance and system integration, rather than verification convenience. Rust's ownership discipline enables Aeneas to extract a pure model of this code in Lean, relieving us from low-level reasoning about pointer liveness and aliasing. Lean's extensibility lets us develop tactics and libraries that greatly simplify reasoning about extracted Rust code. We design and tune our toolchain to facilitate the use of AI. Agents autonomously write formal proofs, which are independently verified by the Lean kernel. Agents also assist in the formalization of cryptographic standards and platform-specific intrinsics, which still requires expert design and review. We apply our methodology to SymCrypt, Microsoft's cryptographic provider. We verify its implementations of algorithms such as SHA-3 and ML-KEM, which were ported from C to Rust. We also extend SymCrypt with experimental optimizations and implementations of algorithms such as FrodoKEM, ML-DSA, and HPKE to explore the scalability of writing, adapting, and verifying cryptographic code. Our 237~KLOC Lean development establishes safety, panic-freedom, and functional correctness of 16.7~KLOC of Rust code supporting post-quantum cipher suites for x86-64 and ARM platforms. Our evaluation shows that verified Rust can meet SymCrypt's performance, portability, deployment, and maintainability requirements.
- Abstract（参考訳）: 我々は,暗号ソフトウェアを検証するための新しい手法を開発した。
検証の利便性ではなく、パフォーマンスとシステム統合のためにRustで記述されたプロダクションコードをターゲットにしています。
Rustのオーナシップの規律により、Aeneas氏は、リーンでこのコードの純粋なモデルを取り出すことができ、ポインタの生きやすさとエイリアスに関する低レベルな推論から身を守ることができます。
Leanの拡張性によって、抽出されたRustコードの推論を大幅に単純化する、戦術とライブラリの開発が可能になります。
AIの使用を容易にするために、ツールチェーンを設計し、調整します。
エージェントは、Leanカーネルによって独立して検証される形式的な証明を、自律的に記述する。
エージェントはまた、専門家の設計とレビューを必要とする暗号標準とプラットフォーム固有の内在論の形式化を支援している。
当社の方法論をMicrosoftの暗号プロバイダであるSymCryptに適用する。
我々は、CからRustに移植されたSHA-3やML-KEMなどのアルゴリズムの実装を検証する。
また、FrodoKEM、ML-DSA、HPKEといったアルゴリズムの実験的な最適化と実装により、SymCryptを拡張して、書込み、適応、暗号コードの検証のスケーラビリティを探求する。
当社の237~KLOCリーン開発は、x86-64とARMプラットフォーム用のポスト量子暗号スイートをサポートするRustコードの16.7～KLOCの安全性、パニックフリーダム、機能的正しさを確立しています。
我々の評価によると、検証済みのRustは、SymCryptのパフォーマンス、ポータビリティ、デプロイメント、保守性要件を満たすことができる。
関連論文リスト
- Kani: A Model Checker for Rust [3.019677299390329]
KaniはRustのオープンソースモデルチェッカーである。
バグフィニング以外のバウンドモデルチェックをプッシュして、正確性を保証する。
KaniはプロダクションCIで大規模に運用されており、コード変更毎に16,000以上のハーネスが検証されている。
論文 参考訳（メタデータ） (2026-07-01T22:05:33Z) - CREBench: Evaluating Large Language Models in Cryptographic Binary Reverse Engineering [12.401873262343862]
大規模言語モデル(LLM)の暗号バイナリリバースエンジニアリング機能について検討する。
ベンチマークでは,48の標準暗号アルゴリズム,3つの安全でない暗号鍵使用シナリオ,3つの難易度から構築した432の課題で構成されている。
また、92.19ポイントの強力な人間専門家ベースラインを確立し、暗号REタスクにおいて人間が優位を維持していることを示す。
論文 参考訳（メタデータ） (2026-04-04T14:51:09Z) - RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。
我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
論文 参考訳（メタデータ） (2026-01-30T08:29:01Z) - 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) - Targeted Fuzzing for Unsafe Rust Code: Leveraging Selective Instrumentation [3.6968220664227633]
Rustは、ユーザビリティとセキュリティに焦点を当てた、有望なプログラミング言語である。
プログラマは、厳格なRustセキュリティポリシーに従わない、安全でないコードを書くことができる。
ファジィアが注目すべきプログラムのどの部分にフォーカスするかを決定するために、安全で安全なコードコンポーネントを自動的に検出する手法を提案する。
論文 参考訳（メタデータ） (2025-05-05T08:48:42Z) - CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [51.18863297461463]
CRUST-Benchは100のCリポジトリのデータセットで、それぞれが安全なRustとテストケースで手書きのインターフェースとペアリングされている。
我々は、このタスクで最先端の大規模言語モデル(LLM)を評価し、安全で慣用的なRust生成が依然として難しい問題であることを確認した。
最高のパフォーマンスモデルであるOpenAI o1は、ワンショット設定で15タスクしか解決できない。
論文 参考訳（メタデータ） (2025-04-21T17:33:33Z) - A Proof-Producing Compiler for Blockchain Applications [0.0873811641236639]
CairoZeroは、分散アプリケーション(dApps)を大規模に実行するためのプログラミング言語である。
暗号化プロトコルは、ブロックチェーン上での実行結果を効率的に検証するために使用される。
ユーザがLean 3の証明アシスタントで、コンパイルされたコードが高レベルの機能仕様を満たすことを証明できるように、CairoZeroコンパイラをいかに拡張したかを示します。
論文 参考訳（メタデータ） (2025-01-25T00:31:47Z) - Syzygy: Dual Code-Test C to (safe) Rust Translation using LLMs and Dynamic Analysis [8.361424157571468]
Syzygyは、C言語を安全なRustに変換する自動化アプローチである。
これは、Rustのコード翻訳を安全にする上で、これまでで最大の自動化およびテスト検証済みのCである。
論文 参考訳（メタデータ） (2024-12-18T18:55:46Z) - FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [51.898805184427545]
削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。
まず、自然言語における暗号関数のセマンティクスを要約するために、バイナリ大言語モデル(FoC-BinLLM)を構築した。
次に、FoC-BinLLM上にバイナリコード類似モデル(FoC-Sim)を構築し、変更に敏感な表現を作成し、データベース内の未知の暗号関数の類似実装を検索する。
論文 参考訳（メタデータ） (2024-03-27T09:45:33Z) - CLAWSAT: Towards Both Robust and Accurate Code Models [74.57590254102311]
比較学習(CL)と逆学習を統合して、コードモデルの堅牢性と精度を協調的に最適化する。
私たちの知る限りでは、これはコードモデルにおける(マルチビュー)コードの難読化の堅牢性と正確性について調査し、活用する最初の体系的な研究です。
論文 参考訳（メタデータ） (2022-11-21T18:32:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。