DOCSEARCHbyAlgolia
Submit Docs

SPECA Security Audit Framework

repository·main·Indexed 19 days ago

https://github.com/nyxfoundation/speca

A specification-anchored security audit framework that derives typed security properties from natural-language specifications to audit implementations through structured proof-attempt reasoning. The project includes the speca-cli for authentication and audit execution, a pipeline utilizing Model Context Protocol (MCP) servers, and evaluation harnesses for benchmark tracks including Ethereum clients (RQ1), C/C++ projects via RepoAudit (RQ2), and protocol implementations via ProFuzzBench (RQ2b).

Tokens
161K
Snippets
394
Records
643
Agent score
65%

What's inside SPECA

  1. Overview of SPECA Benchmark tracks

    main

    SPECA provides evaluation harnesses for three distinct benchmark tracks used in the SPECA paper (arXiv:2604.26495) and one exploratory track:

    • RQ1: Evaluates 10 production Ethereum clients against 15 H/M/L issues from the Sherlock Ethereum Fusaka Audit Contest.
    • RQ2: Evaluates 15 OSS C/C++ projects using the RepoAudit (ICML 2025) dataset.
    • RQ2b (Exploratory): Evaluates 6 text-based protocol implementations using the ProFuzzBench (ChatAFL, NDSS 2024) dataset.

    Detailed reproduction guides for each track are available on the official documentation site.

  2. Overview of the SPECA 2026 Roadmap

    main

    The SPECA 2026 roadmap (May–June) focuses on four parallel tracks:

    1. Track 1: SPECA CLI Construction: Building the TypeScript/Ink-based CLI (Issue #3).
    2. Track 2: Phase A Past Vulnerability Dataset: Creating a dataset of historical vulnerabilities (Issue #2).
    3. Track 3: Phase B Prompt Self-Improvement: Improving prompts, dependent on Track 1 (M3+) and Track 2 completion.
    4. Track 4: Phase C+D Ethereum 11-Client Audit: Conducting audits and disclosure, dependent on Track 1 (v0.1+) and Track 3 (locked prompts).

    Key Deadlines:

    • End of May: CLI shipment.
    • End of June: Ethereum audit report draft.

  3. Overview of SPECA Operations

    main

    The Operations category provides procedures for users responsible for 'running' SPECA. This includes refreshing datasets, executing benchmarks, and distributing artifacts.

    Target Audience

    • Researchers or implementers wanting to reproduce SPECA evaluation results.
    • Operators responsible for updating the HuggingFace audit-finding corpus (NyxFoundation/vulnerability-reports).
    • Contributors wanting to share new benchmark execution results.

    Common Prerequisites

    Before performing operational tasks, ensure you have:

    1. The speca repository checked out and installed.
    2. Access to a self-hosted GitHub Actions runner (specifically on the grandchildrice or hirorogo allowlist).
    3. The following secrets configured for your target tasks:
      • HF_TOKEN: Write permissions for the HuggingFace organization NyxFoundation.
      • GITHUB_TOKEN: Write permissions for GitHub Releases (automatically issued by GitHub Actions).

  4. What is SPECA?

    main

    SPECA is an automated tool designed to verify whether written code behaves according to its specified requirements. Unlike traditional static analysis tools or linters (such as ESLint) that focus on code style and syntax rules (e.g., variable types or unused variables), SPECA focuses on behavioral correctness relative to a specification.

    Core Methodology

    SPECA operates by using the specification as the source of truth. It follows these steps:

    1. Requirement Identification: Analyzes the specification to identify necessary processes and requirements (e.g., security requirements).
    2. Implementation Mapping: Locates the code responsible for implementing those requirements.
    3. Verification/Proof: Attempts to prove that the implementation adheres to the specification across all execution paths (e.g., ensuring 'Authentication' always precedes 'Data Access').
    4. Gap Reporting: Identifies and reports any parts of the code where the specification cannot be proven, marking them as potential vulnerabilities or implementation gaps.

  5. Overview of the RQ2a RepoAudit C/C++ benchmark harness

    main

    The rq2a directory contains the tools and data required to run the RQ2 benchmark for RepoAudit in C/C++ environments. It includes evaluation scripts, visualization tools, and ground-truth data used to measure performance against published baselines.

    Key Components:

    • Evaluation Scripts: evaluate.py, visualize.py, and analyze_deep.py.
    • Ground-Truth Data: ground_truth_bugs.yaml and published_baselines.yaml.

    For detailed instructions on how to reproduce results, interpret output files, or extend the harness to new codebases, refer to the official documentation site.

  6. Overview of the RQ2b ProFuzzBench harness

    main

    The benchmarks/rq2b directory contains the exploratory ProFuzzBench / dynamic-testing comparison track. This track is not included in the official paper and is intended for exploratory use. It includes visualization logic and ground-truth data used to compare ProFuzzBench against dynamic testing methods.

    Key components in this directory:

    • visualize.py: Python script for generating visualizations.
    • ground_truth_bugs.yaml: Data containing ground-truth bug information.
    • published_baselines.yaml: Data containing published baseline information.

    For operational details, including current status, reproduction steps, and known gaps, refer to the official documentation site.

  7. Understand the RQ1 Evaluation Report structure

    main

    The RQ1 Evaluation Report is a summary of security audit performance metrics generated by the SPECA security agent. It evaluates the agent's ability to identify vulnerabilities across different severity levels and audit classifications.

    Key components of the report include:

    • Experiment Environment: Details the AI model used (e.g., Claude 4.5 Sonnet), the specific branches/commits tested, and runtime metrics like token usage and turns.
    • Recall: Measures the percentage of actual issues correctly identified, broken down by severity (High, Medium, Low).
    • Precision: Measures the accuracy of the findings, distinguishing between True Positives (TP) and False Positives (FP).
    • F1 Score: The harmonic mean of Precision and Recall.
    • Phase Comparison: Compares performance between 'Phase 03' (initial audit) and 'Phase 04' (filtering/review phase).
    • Ground Truth Analysis: A breakdown of findings against known labels (e.g., fixed, fp_invalid, tp, tp_info).
    • Token Efficiency: Metrics regarding the cost and time required per audit item.

  8. Project Structure and Key Files

    main

    The SPECA repository is organized into several functional directories:

    • security-agent/: The core logic directory.
      • scripts/run_phase.py: The main entry point for executing pipeline phases.
      • scripts/orchestrator/: Contains the asynchronous Python orchestrator (e.g., BaseOrchestrator for parallel execution/resuming, ClaudeRunner for CLI calls).
      • prompts/: Contains worker prompts for different phases (some are inline, others are file-based).
      • outputs/: Stores pipeline results (e.g., PARTIAL_*.json).
      • .claude/skills/: Contains skill definitions for phases 01a and 01b.
    • benchmarks/: Contains evaluation data for RQ1 (Sherlock) and RQ2 (RepoAudit/ProFuzzBench).
    • tests/: Contains pytest suites, including security regression tests.

  9. Review SPECA Project Vulnerability and Bug Tracker Status

    main

    The SPECA project maintains a tracker for security vulnerabilities (SEC), orchestrator bugs (ORC), benchmark/evaluation bugs (BEN), CI/CD bugs (CI), and schema/test bugs (SCH).

    As of the latest update (2026-03-03), the status is as follows:

    • Security Vulnerabilities (SEC): 17 total (4 FIXED, 5 OPEN, 8 UNKNOWN).
    • Orchestrator (ORC): 19 total (19 FIXED, 0 OPEN).
    • Benchmark/Evaluation (BEN): 16 total (16 FIXED, 0 OPEN).
    • CI/CD (CI): 18 total (18 FIXED, 0 OPEN).
    • Schema/Test (SCH): 14 total (14 FIXED, 0 OPEN).

    Critical security vulnerabilities (SEC-C01 through SEC-C04) have been addressed in a separate PR (claude/confident-lewin, commit 384269ca), while general logic bugs (BUG-ORC/SCH/CI/BEN) were addressed in a bulk PR (bug/fix-1).

  10. Understand the SPECA project structure

    main

    The SPECA repository is organized into several key directories that separate the core orchestration logic, the user interface, and the analysis prompts:

    • scripts/orchestrator/: The core of the pipeline. It manages batch generation, parallel execution, and resuming tasks. It also handles Claude Code CLI calls and cost monitoring.
    • prompts/: Contains the analysis logic for each Phase. Some phases are defined as Claude Code skills (SKILL.md), while others use inline worker prompts.
    • cli/: The TUI (Terminal User Interface) frontend providing commands like speca init, speca run, and speca browse. It is built with Node.js and Ink.
    • outputs/: The location for pipeline input files (e.g., TARGET_INFO.json, BUG_BOUNTY_SCOPE.json) and phase-specific partial outputs ({phase}_PARTIAL_*.json). This directory is gitignored to prevent audit results from being committed.
    • tests/: The pytest-based automated test suite.
    • automation/: GitHub Actions workflow definitions for running phases independently in CI.

  11. Review SPECA performance highlights and benchmarks

    main

    This page summarizes key performance metrics from two major SPECA research papers. These benchmarks demonstrate the effectiveness of the 3-gate review process and the precision/cost trade-offs of different LLM configurations.

    RQ1: Sherlock Ethereum Fusaka Audit Contest

    Evaluates SPECA on 10 Ethereum clients (Go, Rust, Nim, TypeScript, C, C#) implementing EIP-7594 / EIP-7691. Ground truth consists of 15 valid H/M/L findings out of 366 submissions.

    • Recall-Safe Design: Recall remains at 100% across stages, while Precision improves from 56.9% to 66.7% and F1 from 0.725 to 0.800.
    • 3-Gate Effectiveness: The review order is Dead Code $\rightarrow$ Trust Boundary $\rightarrow$ Scope.
      • Dead Code gate provides the cleanest results (n=2 / 100% verified FP).
      • Trust Boundary handles the bulk of the volume (n=21).
      • Scope handles the remaining long tail.
    • False Positive (FP) Root Causes: The largest class of FPs is Specification interpretation / design choice (12 cases), which stems from property generation quality rather than the verification phase itself.

    RQ2a: RepoAudit C/C++ Benchmark

    Evaluates SPECA on 15 OSS projects (avg. 251K LoC per project) using the ICML 2025 RepoAudit benchmark.

    • Precision: SPECA + Sonnet 4.5 achieves 88.9% precision, matching top public baselines and outperforming Meta Infer (77.8%) and o3-mini (80.0%).
    • Cost vs. Performance:
      • Sonnet 4.5: 56 TPs at $101.
      • Sonnet 4: 48 TPs at $81.
      • DeepSeek R1: 40 TPs at $94 (exhibits a stricter dismissal style).

    Summary Table

    BenchmarkRecallPrecisionF1Notes
    Sherlock Fusaka (15 H/M/L)15/15 (expert-augmented) · 8/15 (auto)66.7% (broad)0.8004 new bugs found missed by 366 auditors
    RepoAudit C/C++ (35 + 5)100% for known set88.9%0.9412 author-verified candidates outside GT · ~$1.69 / bug

    For detailed reproduction steps, see the Operations Guide.

  12. Overview of the SPECA Security Agent Pipeline

    main

    SPECA (Specification-to-Property Agentic Auditing) is an automated security auditing pipeline powered by the Claude Code CLI. It follows a structured workflow to transform specifications into formal security properties and then performs formal auditing on target code.

    Core Workflow

    The pipeline operates through several distinct phases:

    1. Spec Discovery (01a): Crawls and discovers specification URLs.
    2. Subgraph Extraction (01b): Converts specifications into Mermaid state diagrams (.mmd + YAML frontmatter).
    3. Property Generation (01e): Generates domain-independent security properties using STRIDE and CWE Top 25. Note: BUG_BOUNTY_SCOPE.json is a required file for this phase.
    4. Code Pre-resolution (02c): Uses Tree-sitter MCP to resolve code locations, reducing token usage by 40-60%. Note: TARGET_INFO.json is required.
    5. Audit Map (03): Executes a 3-stage formal audit (Map → Prove → Stress-Test). A gap in proof results in a finding.
    6. Review (04): A 3-gate false positive (FP) filter (Dead Code → Trust Boundary → Scope Check) that classifies results into categories like CONFIRMED_VULNERABILITY, DISPUTED_FP, or PASS_THROUGH.

    Manual Phases

    After the automated pipeline, users can perform:

    • PoC Generation (05): Creating reproduction tests for vulnerabilities.
    • Reporting (06/06b): Generating Bug-Bounty or full Audit reports.