論文の概要: Beyond Code Reasoning: A Specification-Anchored Audit Framework for Expert-Augmented Security Verification
- arxiv url: http://arxiv.org/abs/2604.26495v1
- Date: Wed, 29 Apr 2026 09:57:07 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-30 15:59:36.344919
- Title: Beyond Code Reasoning: A Specification-Anchored Audit Framework for Expert-Augmented Security Verification
- Title（参考訳）: コード推論を超えて - 専門家によるセキュリティ検証のための仕様書監査フレームワーク
- Authors: Masato Kamba, Hirotake Murakami, Akiyoshi Sannai,
- Abstract要約: SPECAは、仕様書によるセキュリティ監査フレームワークである。
明示的で型付けされたセキュリティ特性は、自然言語仕様に由来する。
それぞれのプロパティに基礎を置く構造化された証明-意図的推論を通じて実装を監査する。
- 参考スコア（独自算出の注目度）: 1.5229705287183657
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Security-critical software is routinely audited by tools that reason about vulnerabilities as repository-local code patterns. Yet specification-governed systems -- protocol stacks, consensus implementations, cryptographic libraries -- are constrained by invariants and correctness conditions defined in natural-language specifications. When a vulnerability arises from what the specification requires rather than how code is written, code-level approaches lack the representational vocabulary to detect it, and their false positives resist systematic diagnosis. We present SPECA, a specification-anchored security audit framework that derives explicit, typed security properties from natural-language specifications and audits implementations through structured proof-attempt reasoning grounded in each property. The framework yields three capabilities absent from code-driven auditing: spec-dependent detections, controlled cross-implementation comparison under a shared property vocabulary, and false positives that decompose into interpretable, pipeline-phase-traceable root causes. On the Sherlock Ethereum Fusaka Audit Contest (366 submissions, 10 implementations), SPECA recovers all 15 in-scope vulnerabilities and independently discovers 4 bugs confirmed by developer fix commits. On the RepoAudit C/C++ benchmark (15 projects), SPECA matches the best published precision (88.9\%) while surfacing 12 candidate bugs beyond the established ground truth, two confirmed by upstream maintainers. A multi-model analysis reveals that more capable models audit more faithfully within property scope, shifting the detection bottleneck from model reasoning to property generation quality. All false positives trace to three recurring root causes -- trust boundary misunderstanding, code reading errors, and specification misinterpretation -- each yielding actionable improvement targets.
- Abstract（参考訳）: セキュリティクリティカルなソフトウェアは、リポジトリローカルなコードパターンとして脆弱性を推論するツールによって定期的に監査される。
しかし、プロトコルスタック、コンセンサス実装、暗号化ライブラリといった仕様管理されたシステムは、自然言語仕様で定義された不変性と正確性条件によって制約される。
コードの書き方よりも仕様が要求するものから脆弱性が発生すると、コードレベルのアプローチでは、それを検出するための表現語彙が欠如し、偽陽性は体系的な診断に抵抗する。
SPECAは、自然言語仕様から明示的で型付けされたセキュリティプロパティを導出し、各プロパティに根ざした構造化された証明-意図的推論を通じて実装を監査する、仕様記述型セキュリティ監査フレームワークである。
このフレームワークは、仕様に依存した検出、共有プロパティの語彙の下での相互実装比較の制御、解釈可能なパイプラインフェーズトレース可能なルート原因に分解される偽陽性の3つの機能を持つ。
Sherlock Ethereum Fusaka Audit Contest (366の提出、10実装)では、SPECAが15のインスコープ脆弱性をすべて回復し、開発者修正コミットによって確認された4つのバグを独立して発見する。
RepoAudit C/C++ベンチマーク(15のプロジェクト)では、SPECAは最高の公開精度 (88.9\%) と一致し、また、確立された基盤の真理を超えた12のバグを指摘し、上流のメンテナが確認した。
マルチモデル解析により、より有能なモデルがプロパティの範囲内でより忠実に監査し、検出ボトルネックをモデル推論からプロパティ生成品質にシフトすることが明らかとなった。
すべての偽陽性は、信頼境界の誤解、コード読み込みエラー、仕様の誤解釈という、3つの繰り返し発生する根本原因に遡る。
関連論文リスト
- Detect Repair Verify for Securing LLM Generated Code: A Multi-Language Empirical Study [10.18490328199727]
セキュリティは、問題を検出し、修正を適用し、結果を検証するDerction-Repair--Verify (DRV)ループを通じて対処されることが多い。
この研究は、プロジェクトレベルのアーティファクトのワークフローを研究し、以下の4つのギャップに対処する: L1、実行可能な機能とセキュリティテストを備えたプロジェクトレベルのベンチマークの欠如 L2、検出や修復のみを研究すること以外のパイプラインレベルの有効性に関する限られた証拠 L3、修正ガイダンスとしての検出レポートの不確実な信頼性、そしてL4、検証中の不確実な修復信頼性と副作用。
論文 参考訳（メタデータ） (2026-03-01T03:41:24Z) - 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) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - Specification-Guided Vulnerability Detection with Large Language Models [32.77684612568584]
VulInstructは、過去の脆弱性からセキュリティ仕様を抽出して、新たな脆弱性を検出する仕様誘導型アプローチである。
PrimeVulでは、VulInstructの45.0%のF1スコア(32.7%の改善)と37.7%のリコール(50.8%の改善)がベースラインと比較している。
論文 参考訳（メタデータ） (2025-11-06T03:21:46Z) - SWAP: Towards Copyright Auditing of Soft Prompts via Sequential Watermarking [58.475471437150674]
ソフトプロンプト(SWAP)のための逐次透かしを提案する。
SWAPは、特定のディフェンダー指定のアウト・オブ・ディストリビューション・クラスを通じて、透かしを符号化する。
11のデータセットの実験では、SWAPの有効性、無害性、および潜在的適応攻撃に対する堅牢性を示す。
論文 参考訳（メタデータ） (2025-11-05T13:48:48Z) - Do LLMs Know They Are Being Tested? Evaluation Awareness and Incentive-Sensitive Failures in GPT-OSS-20B [1.948261185683419]
本研究では,「評価香り」がコンメンシュレート能力を得ることなく測定性能を膨らませるかどうかを考察する。
6つのペアのA/Bシナリオを実行し、タスク内容を保持し、フレーミングの異なる状態でデコードします。
再現可能なA/Bフレームワーク(バンキング、バリデータ、ラン毎のスコア、スクリプト)と実践的なガイダンスを提供する。
論文 参考訳（メタデータ） (2025-10-08T09:49:05Z) - Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models [0.0]
本稿では,Slither-based detectors, Large Language Models (LLMs), Kontrol, Forgeを統合した新しい検出パイプラインを提案する。
私たちのアプローチは、欠陥を確実に検出し、証明を生成するように設計されています。
論文 参考訳（メタデータ） (2025-09-16T12:46:11Z) - VulAgent: Hypothesis-Validation based Multi-Agent Vulnerability Detection [55.957275374847484]
VulAgentは仮説検証に基づくマルチエージェント脆弱性検出フレームワークである。
セマンティクスに敏感なマルチビュー検出パイプラインを実装しており、それぞれが特定の分析の観点から一致している。
平均して、VulAgentは全体的な精度を6.6%改善し、脆弱性のある固定されたコードペアの正確な識別率を最大450%向上させ、偽陽性率を約36%削減する。
論文 参考訳（メタデータ） (2025-09-15T02:25:38Z) - Probing Pre-trained Language Models on Code Changes: Insights from ReDef, a High-Confidence Just-in-Time Defect Prediction Dataset [0.0]
本稿では,22の大規模C/C++プロジェクトから得られた関数レベル修正の信頼性の高いベンチマークであるReDefを紹介する。
欠陥ケースはコミットの反転によって固定され、クリーンケースはポストホック履歴チェックによって検証される。
このパイプラインは3,164の欠陥と10,268のクリーンな修正をもたらし、既存のリソースよりも信頼性の高いラベルを提供する。
論文 参考訳（メタデータ） (2025-09-11T07:07:11Z) - CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
評価と結果報酬のための正確で堅牢な軽量検証モデルであるCompassVerifierを開発した。
数学、知識、多種多様な推論タスクにまたがる多分野の能力を示し、様々な答えの型を処理する能力を示す。
我々は,複数のデータソースから収集したモデル出力からなるVerifierBenchベンチマークを導入し,メタエラーパターンを手動で解析してCompassVerifierを強化する。
論文 参考訳（メタデータ） (2025-08-05T17:55:24Z) - Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。
AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
論文 参考訳（メタデータ） (2021-09-25T22:53:24Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。