論文の概要: 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（参考訳）: コード推論を超えて - 専門家によるセキュリティ検証のための仕様書監査フレームワーク
• 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つの繰り返し発生する根本原因に遡る。

関連論文リスト

• IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
  研究のアイデアは、新しく、一貫性があり、科学的に妥当であるが、その提案された手法は、忠実な実装のために不十分に指定されている。 提案手法は,実装を対象とする研究手法仕様の体系化の可否を,有能な実装者やコーディングエージェントに十分な方法論的情報を提供して,前提条件を満たさずに目的とする手法を構築することができるかを検討する。 IdeaAMBIGは660のエビデンス基底インスタンスのベンチマークで、レポートとGitHubの問題から163の現実世界のギャップと、コーディフィケーション対応のリファレンスに注入される合成ギャップを497のコントロールで管理する。
  論文  参考訳（メタデータ） (2026-09-09T17:59:04Z)
• SWE-Test: Benchmarking LLM Vulnerability Discovery via Input Prediction [13.719725391379276]
  脆弱性発見は、大規模言語モデル(LLM)エージェントの重要な機能である。 我々は、その測定を、クローズドな決定論的基底真理を持つ入力予測タスクとして再放送する。 これにより、発見は15ドメインにまたがる22の現実世界のC/C++プログラムで3つのタスクモードに分解される。
  論文  参考訳（メタデータ） (2026-09-05T19:04:41Z)
• Recognition Without Enforcement: Configuration-Dependent Failures in LLM Agent Instruction Arbitration and External Control [0.0]
  LLMエージェントはシステムプロンプト、ユーザ、メモリ、ツールから命令を仲裁するが、この仲裁は信頼境界を強制するものではない。 ソースフォーマット機能はモデルアクティベーションから線形にデオード可能であり、モデルがトリガーされたときの偽の権威を明示的に識別することができる。 モデル自己配置をセキュリティ境界ではなく機能として扱い、認証されたソースルーティングと機能限定ツールの実行を組み合わせた外部参照モニタを実装します。
  論文  参考訳（メタデータ） (2026-08-28T16:34:05Z)
• A Reproducibility Protocol for Cross-Implementation Evaluation of Post-Quantum ACVP Test Vectors [0.0]
  本研究ではNIST ML-KEMの3つの公開実装のための製品中立プロトコルを定義する。 Protocol v2はプロバイダ固有の機能を凍結し、1つのバリデーションエラーを対称に適用し、選択されたすべてのケースを保存し、バイト、バリデーションバリデーション、サポートされた操作、アダプタエラーを分離する。
  論文  参考訳（メタデータ） (2026-08-13T21:29:59Z)
• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Veroはリポジトリレベルで共同実装と証明を評価する最初のベンチマークである。 Python、Dafny、Verus、Coqにまたがる実世界のリポジトリから43のマルチモジュールインスタンスが含まれている。 ベンチマークの信頼性を改善するため、Veroには、エージェントが提供された仕様の不満足さを正式に証明できる監査メカニズムも含まれている。
  論文  参考訳（メタデータ） (2026-08-13T17:41:27Z)
• Fantastic Adaptive Taxonomies and How to Use Them [100.20614173157708]
  AdaMASTは、実行トレースをコンパクトでエビデンスに基づく障害分類に変換する。 コードには手書きのコードはなく、人間による注釈もない。 エージェント・システム・サーチでは、失敗候補の分類コード診断が自由形式より優れている。
  論文  参考訳（メタデータ） (2026-07-17T17:41:16Z)
• The Patchwork Problem in LLM-Generated Code [3.4562767039451674]
  本稿では,リポジトリアーティファクトのグラフ表現に対する一貫性不変量として構造コヒーレンスを定式化する。 2つのフロンティアモデルに対する実証的な評価によると、構造的失敗の大部分は、型チェック、テスト、SASTを完全に回避している。
  論文  参考訳（メタデータ） (2026-07-09T23:01:54Z)
• Teaching LLMs Program Semantics via Symbolic Execution Traces [0.7046782561282057]
  SV-COMP 2025上に構築された500 C 検証タスクの評価フレームワークを提案する。 6家族の14モデルを評価し,総合的精度の高いマスクが致命的な弱点であることを確認した。 わずか$sim$3,000のバグトレースと、推論時の連鎖推論を組み合わせることで、違反検出を17ポイント以上改善する。
  論文  参考訳（メタデータ） (2026-05-07T13:01:06Z)
• 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)
• What Do They Fix? LLM-Aided Categorization of Security Patches for Critical Memory Bugs [46.325755802511026]
  我々は、LLM(Large Language Model)と細調整された小言語モデルに基づく2つのアプローチを統合するデュアルメタルパイプラインであるLMを開発した。 LMは、OOBまたはUAFの脆弱性に対処する最近のLinuxカーネルのパッチ5,140のうち111つを、手作業による検証によって90の正の正が確認された。
  論文  参考訳（メタデータ） (2025-09-26T18:06:36Z)
• 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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。