Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols

• URL: http://arxiv.org/abs/2604.26495v2
• Date: Tue, 05 May 2026 15:44:33 GMT
• Title: Beyond Code Reasoning: Specification-Anchored Auditing of Multi-Implementation Distributed Protocols
• Abstract summary: SPECA is an audit framework that derives explicit, categorized security properties from natural-language specifications and reuses them across implementations.<n>On the RepoAudit benchmark, SPECA reaches 88.9% precision at 100% recall (F1=0.94) and surfaces 12 author-validated bugs beyond ground truth.<n>On the Sherlock Fusaka Audit Contest (10 targets, 366 submissions), SPECA recovers all 15 vulnerabilities expert-augmented and surfaces 4 fix-confirmed bugs.
• Score: 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).

Related papers

• IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
  A research idea may be novel, coherent, and scientifically plausible, yet its proposed method may remain insufficiently specified for faithful implementation.<n>We study the codification readiness of implementation-facing research-method specifications, defined by whether they provide sufficient methodological information for a competent implementer or coding agent to construct the intended method without unsupported assumptions.<n>We introduce IdeaAMBIG, a benchmark of 660 evidence-grounded instances: 163 real-world gaps from reports and GitHub issues, and 497 controlled synthetic gaps injected into codification-ready references.
  arXiv  Detail & Related papers  (2026-09-09T17:59:04Z)
• SWE-Test: Benchmarking LLM Vulnerability Discovery via Input Prediction [13.719725391379276]
  Vulnerability discovery is an important ability of large language model (LLM) agents.<n>We recast its measurement as an input-prediction task with a closed, deterministic ground truth.<n>This decomposes discovery into three task modes over 22 real-world C/C++ programs spanning 15 domains.
  arXiv  Detail & Related papers  (2026-09-05T19:04:41Z)
• Recognition Without Enforcement: Configuration-Dependent Failures in LLM Agent Instruction Arbitration and External Control [0.0]
  LLM agents arbitrate among instructions from system prompts, users, memory, and tools, but this arbitration cannot be assumed to enforce trust boundaries.<n>We identify a recognition-enforcement gap: source-format features are linearly decodable from model activations, and models can explicitly identify forged authority when prompted.<n>We treat model self-arbitration as a capability rather than a security boundary and implement an external reference monitor combining authenticated source routing with capability-gated tool execution.
  arXiv  Detail & Related papers  (2026-08-28T16:34:05Z)
• A Reproducibility Protocol for Cross-Implementation Evaluation of Post-Quantum ACVP Test Vectors [0.0]
  This study defines a product-neutral protocol for three public implementations of NIST ML-KEM.<n> Protocol v2 freezes provider-specific capabilities, applies one validation-error symmetrically, preserves every selected case, and separates bytes, validation verdicts, unsupported operations, and adapter errors.
  arXiv  Detail & Related papers  (2026-08-13T21:29:59Z)
• Vero: Can AI Agents Build Formally Verified Software Repositories? [45.09790101960906]
  Vero is the first benchmark to evaluate joint implementation and proof at the repository level.<n>It contains 43 multi-module instances from real-world repositories spanning Python, Dafny, Verus, and Coq.<n>To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification.
  arXiv  Detail & Related papers  (2026-08-13T17:41:27Z)
• Fantastic Adaptive Taxonomies and How to Use Them [100.20614173157708]
  AdaMAST converts execution traces into a compact, evidence-grounded failure taxonomy.<n>No code is hand-authored, no trace human-annotated.<n>In agent-system search, taxonomy-coded diagnoses of failed candidates outperform free-form.
  arXiv  Detail & Related papers  (2026-07-17T17:41:16Z)
• The Patchwork Problem in LLM-Generated Code [3.4562767039451674]
  This paper formalizes structural coherence as consistency invariants over graph representations of repository artifacts.<n> Empirical evaluation across two frontier models reveals that the vast majority of structural failures evade type checking, testing, and SAST entirely.
  arXiv  Detail & Related papers  (2026-07-09T23:01:54Z)
• Teaching LLMs Program Semantics via Symbolic Execution Traces [0.7046782561282057]
  We introduce an evaluation framework of 500 C verification tasks built on SV-COMP 2025.<n>We evaluate 14 models across six families and find high overall accuracy masks a critical weakness.<n>Just $sim$3,000 bug traces combined with chain-of-thought reasoning at inference time improve violation detection by over 17 percentage points.
  arXiv  Detail & Related papers  (2026-05-07T13:01:06Z)
• Detect Repair Verify for Securing LLM Generated Code: A Multi-Language Empirical Study [10.18490328199727]
  Security is often addressed through a Detect--Repair--Verify (DRV) loop that detects issues, applies fixes, and verifies the result.<n>This work studies such a workflow for project-level artifacts and addresses four gaps: L1, the lack of project-level benchmarks with executable function and security tests; L2, limited evidence on pipeline-level effectiveness beyond studying detection or repair alone; L3, unclear reliability of detection reports as repair guidance; and L4, uncertain repair trustworthiness and side effects under verification.
  arXiv  Detail & Related papers  (2026-03-01T03:41:24Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Specification-Guided Vulnerability Detection with Large Language Models [32.77684612568584]
  VulInstruct is a specification-guided approach that extracts security specifications from historical vulnerabilities to detect new ones.<n>On PrimeVul, VulInstruct 45.0% F1-score (32.7% improvement) and 37.7% recall (50.8% improvement) compared to baselines, while uniquely detecting 24.3% of vulnerabilities -- 2.4x more than any baseline.
  arXiv  Detail & Related papers  (2025-11-06T03:21:46Z)
• SWAP: Towards Copyright Auditing of Soft Prompts via Sequential Watermarking [58.475471437150674]
  We propose sequential watermarking for soft prompts (SWAP)<n>SWAP encodes watermarks through a specific order of defender-specified out-of-distribution classes.<n>Experiments on 11 datasets demonstrate SWAP's effectiveness, harmlessness, and robustness against potential adaptive attacks.
  arXiv  Detail & Related papers  (2025-11-05T13:48:48Z)
• Do LLMs Know They Are Being Tested? Evaluation Awareness and Incentive-Sensitive Failures in GPT-OSS-20B [1.948261185683419]
  We investigate whether "evaluation scent" inflates measured performance without commensurate capability gains.<n>We run six paired A/B scenarios that hold task content and decoding fixed while varying framing.<n>We provide a reproducible A/B framework (prompt banks, validators, per-run scores, scripts) and practical guidance.
  arXiv  Detail & Related papers  (2025-10-08T09:49:05Z)
• What Do They Fix? LLM-Aided Categorization of Security Patches for Critical Memory Bugs [46.325755802511026]
  We developLM, a dual-method pipeline that integrates two approaches based on a Large Language Model (LLM) and a fine-tuned small language model.<n>LM successfully identified 111 of 5,140 recent Linux kernel patches addressing OOB or UAF vulnerabilities, with 90 true positives confirmed by manual verification.
  arXiv  Detail & Related papers  (2025-09-26T18:06:36Z)
• Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models [0.0]
  This paper introduces a novel detection pipeline that integrates custom Slither-based detectors, Large Language Models (LLMs), Kontrol, and Forge.<n>Our approach is designed to reliably detect defects and generate proofs.
  arXiv  Detail & Related papers  (2025-09-16T12:46:11Z)
• VulAgent: Hypothesis-Validation based Multi-Agent Vulnerability Detection [55.957275374847484]
  VulAgent is a multi-agent vulnerability detection framework based on hypothesis validation.<n>It implements a semantics-sensitive, multi-view detection pipeline, each aligned to a specific analysis perspective.<n>On average, VulAgent improves overall accuracy by 6.6%, increases the correct identification rate of vulnerable--fixed code pairs by up to 450%, and reduces the false positive rate by about 36%.
  arXiv  Detail & Related papers  (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]
  We present ReDef, a high-confidence benchmark of function-level modifications curated from 22 large-scale C/C++ projects.<n>Defective cases are anchored by revert commits, while clean cases are validated through post-hoc history checks.<n>This pipeline yields 3,164 defective and 10,268 clean modifications, offering substantially more reliable labels than prior existing resources.
  arXiv  Detail & Related papers  (2025-09-11T07:07:11Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  We develop CompassVerifier, an accurate and robust lightweight verifier model for evaluation and outcome reward.<n>It demonstrates multi-domain competency spanning math, knowledge, and diverse reasoning tasks, with the capability to process various answer types.<n>We introduce VerifierBench benchmark comprising model outputs collected from multiple data sources, augmented through manual analysis of metaerror patterns to enhance CompassVerifier.
  arXiv  Detail & Related papers  (2025-08-05T17:55:24Z)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAI bridges the gap between interpretable formal verification and scalability. We show how AuditAI allows us to obtain controlled variations for verification and certified training while addressing the limitations of verifying using only pixel-space perturbations.
  arXiv  Detail & Related papers  (2021-09-25T22:53:24Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.