論文の概要: AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification
- arxiv url: http://arxiv.org/abs/2605.10712v1
- Date: Mon, 11 May 2026 15:23:26 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-12 23:28:50.934718
- Title: AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification
- Title（参考訳）: AutoSOUP:コンポーネントレベルのメモリ安全性検証のための安全指向ユニットプロー生成
- Authors: Paschal C. Amusuo, Ricardo Calvo, Dharun Anandayuvaraj, Taylor Le Lievre, Kevin Kolyakov, Elijah Jorgensen, Aravind Machiry, James C. Davis,
- Abstract要約: メモリセーフティエラーは、低レベルソフトウェアにおけるゼロデイ脆弱性の永続的な原因である。
現在の検証はほとんど手作業で行われており、専門的な専門知識が必要である。
本稿では,コンポーネントレベルのメモリ安全性検証を自動化するシステムであるAutoSOUPを提案する。
- 参考スコア（独自算出の注目度）: 10.258883626292265
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Memory-safety errors remain a persistent source of zero-day vulnerabilities in low-level software. The problem is especially acute in embedded systems, where hardware protections are often limited and dynamic analysis is difficult to apply effectively. Memory-safety verification can provide stronger assurance by proving the absence of such errors or exposing violations when they exist. However, current verification workflows remain largely manual and require substantial specialized expertise, limiting their adoption in practice. We present AutoSOUP, a system for automating component-level memory-safety verification through Safety-Oriented Unit Proofs. We formalize these unit proofs as artifacts that encode verification choices (scope, loop bounds, and environment models) for verifying safety properties, and introduce three techniques for deriving them automatically. To overcome the limitations of existing automation approaches, we further introduce LLM-As-Function-Call, a hybrid architecture that combines deterministic program synthesis with LLMs to automate these techniques and produce justifiable unit proofs. We evaluate AutoSOUP by assessing its ability to automate memory-safety verification and expose vulnerabilities in verified components, and we characterize the assumptions and guarantees of the resulting proofs.
- Abstract（参考訳）: メモリセーフティエラーは、低レベルソフトウェアにおけるゼロデイ脆弱性の永続的な原因である。
特に組込みシステムではハードウェア保護が制限されることが多く、動的解析を効果的に適用することは困難である。
メモリセーフティ検証は、そのようなエラーの欠如を証明したり、それらが存在する場合に違反を暴露することによって、より強力な保証を提供することができる。
しかし、現在の検証ワークフローはほとんど手作業のままで、専門的な専門知識が必要であり、実際には採用を制限している。
本稿では,コンポーネントレベルのメモリ安全性検証を自動化するシステムであるAutoSOUPを提案する。
安全性を検証するための検証選択(スコープ,ループ境界,環境モデル)を符号化するアーティファクトとして,これらの証明を形式化し,自動抽出する3つの手法を導入する。
LLM-As-Function-Callは、決定論的プログラム合成とLLMを組み合わせたハイブリッドアーキテクチャで、これらの手法を自動化し、妥当なユニット証明を生成する。
我々は、メモリセーフティ検証の自動化と、検証済みコンポーネントの脆弱性の暴露能力を評価することにより、AutoSOUPを評価し、その結果の仮定と保証を特徴付ける。
関連論文リスト
- SecureForge: Finding and Preventing Vulnerabilities in LLM-Generated Code via Prompt Optimization [61.91729298584227]
SecureForgeは、フロンティアモデルのセキュリティリスクを監査し、監査インフォームされたセキュアなシステムプロンプトを生成する自動化パイプラインである。
SecureForgeは、まず静的に検出可能な脆弱性を生成する良性プロンプトを特定し、その後、さまざまなシナリオの大規模な合成プロンプトコーパスに増幅する。
フロンティアモデルでは、SecureForgeは、ユニットテストの成功と出力セキュリティの両方において統計的に有意な改善をもたらし、出力脆弱性は最大48%削減された。
論文 参考訳（メタデータ） (2026-05-08T18:40:47Z) - 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) - 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) - Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
大規模言語モデル(LLM)ベースのAIエージェントは、データソース、API、検索エンジン、コードサンドボックス、さらにはその他のエージェントなどのツールへのアクセスを可能にすることで、機能を拡張する。
LLMは意図しないツールインタラクションを起動し、機密データを漏洩したり、クリティカルレコードを上書きしたりするリスクを発生させる。
モデルベースセーフガードのようなリスクを軽減するための現在のアプローチは、エージェントの信頼性を高めるが、システムの安全性を保証することはできない。
論文 参考訳（メタデータ） (2026-01-12T21:31:38Z) - AI Bill of Materials and Beyond: Systematizing Security Assurance through the AI Risk Scanning (AIRS) Framework [31.261980405052938]
人工知能(AI)システムの保証は、ソフトウェアサプライチェーンセキュリティ、敵機械学習、ガバナンスドキュメントに分散している。
本稿では,AI保証の運用を目的とした脅威モデルに基づくエビデンス発生フレームワークであるAI Risk Scanning(AIRS)フレームワークを紹介する。
論文 参考訳（メタデータ） (2025-11-16T16:10:38Z) - AttestLLM: Efficient Attestation Framework for Billion-scale On-device LLMs [19.00344718051438]
本稿では,デバイスベンダのハードウェアレベルの知的財産権(IP)を保護するための,最初のテストフレームワークであるAttestLLMを紹介する。
AttestLLMはモデルの正当性を強制し,モデル偽造や攻撃に対するレジリエンスを示す。
論文 参考訳（メタデータ） (2025-09-08T04:17:02Z) - BugWhisperer: Fine-Tuning LLMs for SoC Hardware Vulnerability Detection [1.0816123715383426]
本稿では,システムオンチップ(SoC)セキュリティ検証の課題を解決するために,BugWhispererという新しいフレームワークを提案する。
我々は、SoCのセキュリティ脆弱性を検出するために特別に設計された、オープンソースで微調整されたLarge Language Model (LLM)を紹介する。
論文 参考訳（メタデータ） (2025-05-28T21:25:06Z) - Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳（メタデータ） (2025-05-28T17:57:47Z) - Exposing the Ghost in the Transformer: Abnormal Detection for Large Language Models via Hidden State Forensics [5.384257830522198]
重要なアプリケーションにおける大規模言語モデル(LLM)は、重大な信頼性とセキュリティリスクを導入している。
これらの脆弱性は悪意あるアクターによって武器化され、不正アクセス、広範囲にわたる誤報、システムの完全性を侵害した。
本研究では,LLMの異常な挙動を隠蔽法で検出する手法を提案する。
論文 参考訳（メタデータ） (2025-04-01T05:58:14Z) - Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。
RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。
これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。
我々は、無害な」知識基盤の著作権保護の名称を提案する。
論文 参考訳（メタデータ） (2025-02-10T09:15:56Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。