論文の概要: KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification
- arxiv url: http://arxiv.org/abs/2607.21957v1
- Date: Fri, 24 Jul 2026 04:10:12 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-27 20:58:57.042936
- Title: KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification
- Title（参考訳）: KaPilot: 安全でないRust検証のためのKani仕様の生成を支援するLLM
- Abstract要約: Rustのオーナシップと型システムは、強いメモリ安全性を保証するが、安全でないコードは依然としてメモリ安全性のリスクを示す。
KaPilotは、安全でないRustメモリ安全性を検証するために仕様を自動的に生成するフレームワークである。
AutoSpecと比較すると、KaPilotは14.8%以上の検証可能な仕様と25.9%以上の等価な仕様を生成している。
- 参考スコア（独自算出の注目度）: 8.36913747598685
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Rust's ownership and type system provide strong memory safety guarantees, but unsafe code still presents memory safety risks. Formal verification is crucial for ensuring memory safety, but writing precise specifications for unsafe Rust is challenging and largely manual. Large language models (LLMs) have shown promise in generating formal specifications but are often code-centric, prone to inheriting implementation flaws, and lack systematic quality assessment. In this paper, we present KaPilot, a multi-agent framework for automatically generating specifications to verify unsafe Rust memory safety using Kani. The process begins with lightweight program analysis and proof harness generation. The SafetyReq agent extracts a concise, refined list of safety requirements from the target Rust function's documentation, which guides the SpecGenerate agent in producing initial specifications that specify memory safety concerns. Then, the specifications are iteratively refined through a generate-precheck-verify loop involving SpecGenerate, SpecPrecheck, and SpecVerify agents, which assess quality and feed errors back. By executing this loop multiple times, KaPilot generates a set of candidate specifications. Finally, the shuffle-and-implication strategy is applied to systematically determine the best specification from these candidates. We evaluated KaPilot on 54 unsafe Rust functions with ground truth and 70 without. KaPilot achieved 88.9% and 71.4% specification generation success, respectively, with 57.4% of generated specifications equivalent to or stronger than the ground truth. Compared with AutoSpec, KaPilot produces 14.8% more verifiable specifications and 25.9% more equivalent-or-better specifications.
- Abstract（参考訳）: Rustのオーナシップと型システムは、強いメモリ安全性を保証するが、安全でないコードは依然としてメモリ安全性のリスクを示す。
メモリ安全性を確保するためには形式的検証が不可欠だが、安全でないRustの正確な仕様を書くことは困難で、大部分が手作業である。
大型言語モデル(LLM)は形式的な仕様を生成する上で有望であるが、しばしばコード中心であり、実装上の欠陥を継承し、体系的な品質評価を欠いている。
In this paper, we present KaPilot, a multi-agent framework for automatically generation specification to confirmed unsafe Rust memory safety using Kani。
プロセスは、軽量なプログラム分析と証明ハーネス生成から始まります。
SafetyReqエージェントは、ターゲットのRust関数のドキュメントから、簡潔で洗練された安全要件のリストを抽出する。
次に、仕様はSpecGenerate、SpecPrecheck、SpecVerifyエージェントを含むGenerator-precheck-verifyループを通じて反復的に洗練され、品質を評価し、エラーを返送する。
このループを複数回実行することで、KaPilotは候補仕様のセットを生成する。
最後に、これらの候補から最適な仕様を体系的に決定するためにシャッフル・アンド・インプリケーション戦略を適用する。
KaPilotを54の安全でないRust関数と70の非安全性で評価した。
KaPilotは、それぞれ88.9%と71.4%の仕様生成に成功した。
AutoSpecと比較すると、KaPilotは14.8%以上の検証可能な仕様と25.9%以上の等価な仕様を生成している。
関連論文リスト
- HarnessLLM: Rust Verification Harness Generation with Large Language Models [8.14069260667009]
Rustのオーナシップモデルと型システムは、強力なメモリ安全保証を提供するが、安全でないコードとランタイムパニックは依然として重大なリスクを伴っている。
メモリ安全性を確保するためには形式的検証が不可欠だが、検証ハーネスの開発は依然として困難な作業である。
私たちは、大規模な言語モデルを活用して、既存のテストスイートから直接Rustコードの検証ハーネスを生成する自動化ワークフローであるHarnessLLMを紹介します。
論文 参考訳（メタデータ） (2026-07-24T10:06:52Z) - HyperSafe: Inference-Time Safety Recovery for Fine-Tuned Language Models [65.08794811632073]
HyperSafeは、細調整されたチェックポイント毎にモデル固有のSafe Side Networkを生成することで、安全性の挙動を復元する。
モデル群であるQwen2-7BとLLaMA-3-8Bを複数の安全性ベンチマークで評価した。
論文 参考訳（メタデータ） (2026-07-13T12:28:43Z) - Kani: A Model Checker for Rust [3.019677299390329]
KaniはRustのオープンソースモデルチェッカーである。
バグフィニング以外のバウンドモデルチェックをプッシュして、正確性を保証する。
KaniはプロダクションCIで大規模に運用されており、コード変更毎に16,000以上のハーネスが検証されている。
論文 参考訳（メタデータ） (2026-07-01T22:05:33Z) - CHILLGuard: Towards Fine-Grained Chinese LLM Safety Guardrail with Scalable Data Construction and Model-aware Preference Alignment [55.74660714572696]
大きな言語モデル(LLM)から生成された悪意のあるコンテンツは、深刻な安全リスクと倫理的懸念を引き起こす可能性がある。
既存のLLMの安全ガードレールは英語や多言語の設定では優れているが、中国固有の規制政策、文化的文脈、言語的ニュアンスには適応していない。
我々は,中国のシナリオに対して,5マクロ,31マイクロカテゴリの細粒度リスク分類を導入し,中国向けLLMコンテンツ安全ガードレールであるCHILLGuardを構築した。
論文 参考訳（メタデータ） (2026-06-13T16:57:51Z) - Intent-aligned Formal Specification Synthesis via Traceable Refinement [43.72968325799861]
VeriSpecGenは、要求レベルの属性と局所的な修復を通じて、リーンで意図に整合した仕様を合成する、トレーサブルな改善フレームワークです。
VeriSpecGenは自然言語をアトミックな要件に分解し、明示的なトレーサビリティマップで要求対象のテストを生成する。
我々は、Claude Opus 4.5を使用してVERINA SpecGenタスクの86.6%を達成し、モデルファミリとスケールで最大31.8ポイントのベースラインを改善する。
論文 参考訳（メタデータ） (2026-04-12T00:52:27Z) - 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) - LiteRSan: Lightweight Memory Safety Via Rust-specific Program Analysis and Selective Instrumentation [19.377860990540444]
Rustはメモリセーフな言語であり、強力な安全性保証が広く採用されている。
Rustのメモリ安全性バグを検出するための広く採用されているアプローチとして、Address Sanitizer(ASan)がある。
本稿では、従来のアプローチの限界に対処する新しいメモリセーフティサニタイザであるLiteRSanを紹介する。
論文 参考訳（メタデータ） (2025-09-19T20:09:20Z) - 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) - 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) - Is unsafe an Achilles' Heel? A Comprehensive Study of Safety
Requirements in Unsafe Rust Programming [4.981203415693332]
Rustは、効率性とメモリ安全性を重視した、新しく、強く型付けされたプログラミング言語である。
標準ライブラリの現在の安全でないAPIドキュメントには、一貫性や不十分さなど、さまざまなバリエーションがあった。
Rustのセキュリティを強化するために、ユーザに従うべき安全要件の体系的な記述をリストアップするために、安全でないAPIドキュメントを提案する。
論文 参考訳（メタデータ） (2023-08-09T08:16:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。