論文の概要: Automatically Building Machine-Checked Assurance Cases from C Codebases to Requirements
- arxiv url: http://arxiv.org/abs/2609.40119v1
- Date: Wed, 30 Sep 2026 16:44:34 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-01 18:57:28.10096
- Title: Automatically Building Machine-Checked Assurance Cases from C Codebases to Requirements
- Title（参考訳）: C言語コードベースから要件への自動機械型保証ケースの構築
- Abstract要約: 本報告では,マシンチェックによる保証ケース構築のためのLCM支援フレームワークであるCCVについて述べる。
オープンライブラリでの使用を意図したインターフェースをモデル化するために、CCVは、許可された呼び出しシーケンスとリソース仮定をレビューするために公開するインターフェースプロトコルを構築している。
CCVは6つのベンチマークで299の関数定義のメモリ安全性とリークの自由を検証している。
- 参考スコア（独自算出の注目度）: 25.859094233491728
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Large language models (LLMs) have shown promise in automating interactive theorem proving, yet verification of real-world C codebases requires more than discharging individual proof goals. The task involves jointly constructing expressive function specifications and their proofs, and ensuring that library interfaces compose along intended call sequences even without a designated client. This paper presents CCV, an LLM-assisted framework for building machine-checked assurance cases: structured, auditable artifacts supporting the claim that a C codebase meets its intended requirements. To model intended cross-interface use in open libraries, CCV constructs an interface protocol that exposes permitted call sequences and resource assumptions for review, with a conditional safety guarantee under verified contracts and caller obligations. CCV coordinates two complementary phases: (i) requirement-guided analysis and bottom-up construction of candidate specifications and protocols; and (ii) modular proof construction with feedback that revises the specifications and proofs. Implemented using VST in Rocq, CCV verifies memory safety and leak freedom for all 299 function definitions across six C benchmarks, including industrial cryptographic components, with less than one person-day of reported human effort per benchmark. The guarantees depend on disclosed contracts and assumptions; human review supplies the conformance judgments connecting the formal artifacts to the intended requirements.
- Abstract（参考訳）: 大規模言語モデル(LLM)は、インタラクティブな定理証明の自動化を約束しているが、実際のCコードベースの検証には、個々の証明目標を出力する以上のものが必要である。
このタスクは、表現力のある関数仕様とその証明を共同で構築し、指定されたクライアントがいなくても、ライブラリインターフェースが意図した呼び出しシーケンスに沿って構成されることを保証する。
本稿では,マシンチェックによる保証ケースを構築するためのLCM支援フレームワークであるCCVについて述べる。
CCVは、オープンライブラリで意図されたクロスインタフェースの使用をモデル化するために、認証された契約と呼び出し義務の下で条件付き安全保証とともに、許可された呼び出しシーケンスとリソースの仮定を公開するインターフェースプロトコルを構築している。
CCVは2つの相補相を調整します。
一 要求誘導分析及び候補仕様及びプロトコルのボトムアップ構築
(ii) 仕様と証明を改訂するフィードバックによるモジュラー証明の構成。
RocqでVSTを使用して実装されたCCVは、産業用暗号コンポーネントを含む6つのCベンチマークで299の関数定義すべてに対して、メモリ安全性とリークの自由を検証している。
保証は、開示された契約と前提に依存し、人間のレビューは、形式的なアーティファクトと意図された要件を結びつける適合性判断を提供する。
関連論文リスト
- Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST [32.505127447635864]
Liblzmaのデコーダコンポーネントのメモリ安全性の検証について報告する。
検証の結果、生のLZMA1ゼロインプット処理における未定義の動作が明らかになった。
検証済みコードを合成する類似の作業とは異なり、既存のプロダクションスケールCを検証する。
論文 参考訳（メタデータ） (2026-08-30T10:50:56Z) - Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
Veroはリポジトリレベルで共同実装と証明を評価する最初のベンチマークである。
Python、Dafny、Verus、Coqにまたがる実世界のリポジトリから43のマルチモジュールインスタンスが含まれている。
ベンチマークの信頼性を改善するため、Veroには、エージェントが提供された仕様の不満足さを正式に証明できる監査メカニズムも含まれている。
論文 参考訳（メタデータ） (2026-08-13T17:41:27Z) - Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。
既存のアプローチはそのようなシステムレベルの保証を提供していません。
本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
論文 参考訳（メタデータ） (2026-08-04T13:01:30Z) - LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean [9.293322518056357]
本稿では,タイプベースの推論とトレースベースの推論を組み合わせることで,ステートフルプロトコルとアンバウンドプロトコルのモジュール検証を実現する手法を提案する。
私たちはこのフレームワークをリーン実証アシスタント用のLeanDYライブラリとして実装し、DY*の設計を構築し拡張します。
我々は、LeanDYでSegWitスタイルのブロックチェーンプリミティブを形式化し、支払いチャネルの詳細な形式化を行うことで、その表現性を実証する。
論文 参考訳（メタデータ） (2026-07-03T15:12:30Z) - Contract Based Verification of Non-functional Requirements for Embedded Automotive C Code [0.5296470528744145]
制御フローやデータフローの制限のような非機能要件は、組み込みシステムの安全性にとって重要である。
Cモジュールのためのインタフェース仕様契約言語を提案する。
Scania trucks におけるソフトウェアを用いた安全クリティカル C コードの2つのケーススタディについて報告する。
論文 参考訳（メタデータ） (2026-05-19T21:12:45Z) - Symfrog-512: High-Capacity Sponge-Based AEAD Cipher (1024-bit State) [0.0]
この提案には、決定論的テストベクタと再現可能なベンチマークスイートとともに、完全なリファレンス実装が含まれている。
AEADの構築は、ドメイン分離、レートとキャパシティの選択、タグ生成、参照CLIで使用される正確なファイルフォーマットなど、完全に規定されている。
報告されたパフォーマンス数値は、ドキュメンテーションされたハードウェアとコンパイラ設定の下で、組み込みのベンチマークツールによって生成される。
論文 参考訳（メタデータ） (2026-02-19T23:39:54Z) - SecCodeBench-V2 Technical Report [43.10947096543533]
SecCodeBench-V2は,セキュアなコードを生成するLarge Language Model (LLM)コピロの能力を評価するためのベンチマークである。
SecCodeBench-V2は、アリババグループの工業生産から派生した98世代および修正シナリオを含む。
各シナリオに対して、SecCodeBench-V2は、機能検証とセキュリティ検証の両方に対して実行可能な概念実証(PoC)テストケースを提供する。
論文 参考訳（メタデータ） (2026-02-17T10:47:06Z) - 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) - ProtocolLLM: RTL Benchmark for SystemVerilog Generation of Communication Protocols [45.66401695351214]
本稿では,広く使用されているSystemVerilogプロトコルを対象とした最初のベンチマークスイートであるProtocolLLMを紹介する。
我々は,ほとんどのモデルがタイミング制約に従う通信プロトコルのSystemVerilogコードを生成するのに失敗したことを観察する。
論文 参考訳（メタデータ） (2025-06-09T17:10:47Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。