論文の概要: Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST
- arxiv url: http://arxiv.org/abs/2608.29716v1
- Date: Sun, 30 Aug 2026 10:50:56 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-01 18:31:31.052049
- Title: Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST
- Title（参考訳）: VSTを用いたLiblzma Decoderコンポーネントのメモリ安全性のエージェント駆動検証
- Abstract要約: Liblzmaのデコーダコンポーネントのメモリ安全性の検証について報告する。
検証の結果、生のLZMA1ゼロインプット処理における未定義の動作が明らかになった。
検証済みコードを合成する類似の作業とは異なり、既存のプロダクションスケールCを検証する。
- 参考スコア（独自算出の注目度）: 32.505127447635864
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We report on the verification of memory safety for decoder components of liblzma, the compression library underlying xz-utils: the LZMA2 state machine, the LZMA1 decoder it controls, the outer decoding path, and the shared sliding-window dictionary. Built with the Verified Software Toolchain (VST), machine-checked body theorems establish memory safety and partial functional correctness. Across 27 completed body proofs, the largest covers lzma decode, whose 338 source lines expand to 1,934 lines of C after preprocessing; its proof comprises 183,268 lines of proof script over 775,768 lines of mechanically extracted goal statements. The verification exposed undefined behavior in raw LZMA1 zero-input handling, where range-decoder macros add zero to a null pointer and subtract two null pointers. Unlike similar work that synthesizes verified code, we verify pre-existing, production-scale C. AI agents complete proof goals and propose refinements; humans write and review models and specifications, and approve semantic changes; the Rocq kernel checks the proof terms. With agents constructing the proof scripts, the main engineering problems lay in translating and modeling production C, building a robust harness for driving Rocq, and providing feedback for proving agents. VST's assertion logic expressed every contract required by the development. We describe the pipeline, coordination mechanisms, and proof-engineering techniques that resolved these frictions.
- Abstract（参考訳）: 我々は,LZMA2ステートマシン,LZMA1デコーダ,外部デコーダパス,共有スライディングウィンドウ辞書など,xz-utilsの基礎となる圧縮ライブラリである liblzma のデコーダコンポーネントのメモリ安全性の検証について報告する。
Verified Software Toolchain (VST)で構築されたマシンチェックボディ定理は、メモリ安全性と部分的機能的正当性を確立する。
27の証明が完了し、最大のカバーである lzma decode は、338 のソースラインが前処理後に 1,934 行に拡張され、その証明は 775,768 行の機械的に抽出されたゴールステートメントの上に 183,268 行の証明スクリプトからなる。
LZMA1ゼロインプット処理では、レンジデコーダマクロがnullポインタに0を追加し、2つのnullポインタを減算する。
検証済みコードを合成する類似の作業とは異なり、既存のプロダクションスケールのAIエージェントが証明目標を完了し、改善を提案すること、人間がモデルや仕様を書いてレビューし、意味的な変更を承認すること、Rocqカーネルが証明条件をチェックすること、などである。
エージェントが証明スクリプトを構築することで、主なエンジニアリング上の問題は、プロダクションCの翻訳とモデリング、Rocqを駆動するための堅牢なハーネスの構築、エージェントの証明のためのフィードバックの提供にあった。
VSTのアサーションロジックは、開発に必要なすべての契約を表現した。
これらの摩擦を解消したパイプライン、調整機構、証明工学技術について述べる。
関連論文リスト
- Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
Veroはリポジトリレベルで共同実装と証明を評価する最初のベンチマークである。
Python、Dafny、Verus、Coqにまたがる実世界のリポジトリから43のマルチモジュールインスタンスが含まれている。
ベンチマークの信頼性を改善するため、Veroには、エージェントが提供された仕様の不満足さを正式に証明できる監査メカニズムも含まれている。
論文 参考訳（メタデータ） (2026-08-13T17:41:27Z) - An AI Approach to Verified Production Cryptographic Libraries [5.564288012051712]
我々は、高レベルのAPI契約から内部仕様とVerusチェックされた証明を合成するAIベースのシステムであるCryptoProverを提案する。
実行可能なコードを変更することなく、CryptoProverはCrypto25519-dalekの新しい独立した証明を構築している。
論文 参考訳（メタデータ） (2026-08-02T03:32:08Z) - The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK [0.0]
検証者主導のループにおいて、AIエージェントは古典的および後量子暗号、TLS 1.3、IKEv2、X.509、マトリックスクライアントにまたがるAda/SPARKのベアメタルセキュリティソフトウェアを書いて検証した。
GNATproveは49,280の証明義務を解除し、選択されたプリミティブに対して機能的正当性を確立し、残りのプリミティブに対して実行時のエラーがないことを証明した。
それぞれのレイヤが障害をキャッチし,中心的な教訓を引き出す方法を報告します。エージェントが確立するために信頼できるものは,そのフィードバックの強さに縛られているのです。
論文 参考訳（メタデータ） (2026-07-15T20:09:05Z) - From Prompts to Contracts: Harness Engineering for Auditable Enterprise LLM Agents [0.24554686192257424]
製品化は、ソースバウンダリ、エンティティルーティング、回答コントラクト、再現可能なトレースの要件を追加します。
本稿では,このパターンをトレース可能な監査可能なLLMエージェントアーキテクチャに再構成するハーネスエンジニアリング手法を提案する。
韓国の5つの企業グループの公開データスライスでインスタンス化し、3つの研究課題を評価する。
論文 参考訳（メタデータ） (2026-07-09T01:08:33Z) - Symfrog-512: High-Capacity Sponge-Based AEAD Cipher (1024-bit State) [0.0]
この提案には、決定論的テストベクタと再現可能なベンチマークスイートとともに、完全なリファレンス実装が含まれている。
AEADの構築は、ドメイン分離、レートとキャパシティの選択、タグ生成、参照CLIで使用される正確なファイルフォーマットなど、完全に規定されている。
報告されたパフォーマンス数値は、ドキュメンテーションされたハードウェアとコンパイラ設定の下で、組み込みのベンチマークツールによって生成される。
論文 参考訳（メタデータ） (2026-02-19T23:39:54Z) - Verifiable Provenance of Software Artifacts with Zero-Knowledge Compilation [5.939983212292006]
ゼロ知識仮想マシン(zkVM)を用いたソフトウェアをコンパイルし,検証可能な証明手法を提案する。
コンパイラをzkVM内で実行することにより,コンパイルされた出力と暗号証明の両方を生成し,そのコンパイルがクレームコンパイラでクレームされたソースコード上で実行されたことを実証する。
この結果から,zkコンパイルは実世界のソフトウェアに適用可能であり,強力なセキュリティ保証を提供することがわかった。
論文 参考訳（メタデータ） (2026-02-12T12:36:36Z) - 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) - Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳（メタデータ） (2025-05-28T17:57:47Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。