論文の概要: Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols
- arxiv url: http://arxiv.org/abs/2604.26495v2
- Date: Tue, 05 May 2026 15:44:33 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-06 14:45:21.128442
- Title: Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols
- Title（参考訳）: コード推論を超えて - マルチ実装分散プロトコルの仕様監査
- Authors: Masato Kamba, Hirotake Murakami, Akiyoshi Sannai,
- Abstract要約: SPECAは、明示的で分類されたセキュリティプロパティを自然言語仕様から導き出し、実装間で再利用する監査フレームワークである。
RepoAuditのベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化している。
Sherlock Fusaka Audit Contest(10のターゲット、366の応募)では、SPECAが専門家が強化した15の脆弱性をすべて回復し、4つの修正確認バグが浮上した。
- 参考スコア（独自算出の注目度）: 1.5229705287183657
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Code-driven auditing fails when correctness depends on what the specification requires rather than how the code is written. Production blockchain networks expose this directly: byzantine consensus runs many independent clients of a shared specification, so a specification-divergence defect in one client can fork the network or halt finality. Existing tools reason one repository at a time, with no shared baseline held constant across implementations. We present SPECA, an LLM-driven audit framework that derives explicit, categorized security properties (invariants, pre/postconditions, trust assumptions) from natural-language specifications and reuses them across implementations. SPECA enables controlled cross-implementation comparison, detections grounded in specification invariants no code pattern encodes, and false positives traceable to a specific pipeline phase rather than opaque model errors. On the Sherlock Ethereum Fusaka Audit Contest (10 targets, 366 submissions), SPECA recovers all 15 in-scope H/M/L vulnerabilities expert-augmented (8/15 automated-only) and surfaces 4 fix-confirmed bugs, including a cryptographic-invariant violation missed by every adjudicated finding. On the RepoAudit C/C++ benchmark, SPECA reaches 88.9% precision at 100% recall (F1=0.94) and surfaces 12 author-validated bugs beyond ground truth, two externally validated. SPECA also flags 5 of RepoAudit's 40 published bugs as defensive-coding fixes with no reachable exploit path. False positives trace to three pipeline-pinned root causes; a multi-model study identifies property-generation quality as the binding constraint. End-to-end cost is ~$30 per H/M/L bug (~42 min wall-clock under parallel execution).
- Abstract（参考訳）: コードの書き方よりも仕様が必要とするものに依存している場合、コード駆動監査は失敗する。
byzantineコンセンサスは、共有仕様の多くの独立したクライアントを実行するため、あるクライアントの仕様分割欠陥がネットワークをフォークしたり、ファイナリティを停止することができる。
既存のツールでは、実装間で共有ベースラインが一定に保たれていないため、一度に1つのリポジトリがある。
SPECAは、自然言語仕様から明示的で分類されたセキュリティ特性(不変性、前/後条件、信頼前提)を導出し、それらを実装間で再利用するLLM主導の監査フレームワークである。
SPECAは、クロス実装比較の制御、コードパターンエンコードのない仕様不変量に基づく検出、不透明なモデルエラーよりも特定のパイプラインフェーズにトレース可能な偽陽性を可能にする。
Sherlock Ethereum Fusaka Audit Contest (10のターゲット、366の応募)では、SPECAが15のスコープ内H/M/L脆弱性をすべて回復し、8/15の自動オンリー)、修正確認済みの4つのバグをサーフェスする。
RepoAudit C/C++ベンチマークでは、SPECAは100%リコール(F1=0.94)で88.9%の精度に達し、著者が検証した12のバグを地上の真実を超えて表面化し、2つの外部検証を行った。
SPECAはまた、RepoAudit氏が発行した40のバグのうち5つを、到達可能なエクスプロイトパスのない防御コード修正としてフラグ付けしている。
False positives trace to three pipeline-pinned root cause; a multi-model study that property-generation quality as the binding constraint。
エンドツーエンドのコストは、H/M/Lバグあたり30ドル(並列実行時には42分)である。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。