Veritas: A Semantically Grounded Agentic Framework for Memory Corruption Vulnerability Detection in Binaries

🕒 Published (v1): 2026-05-14 17:16 UTC · Source: Arxiv · link

Why this paper was selected

Veritas: semantically grounded agentic framework for binary memory-corruption detection

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

Veritas is a three-stage agentic framework for detecting memory corruption vulnerabilities in stripped binaries by grounding LLM reasoning in static interprocedural data-flow evidence and concrete runtime validation. It chains a deterministic slicer, a dual-view LLM detector (decompiled C + selective LLVM IR), and a multi-agent debugger-based validator into a modular pipeline. On a curated binary benchmark, Veritas achieves 90% recall with near-zero false positives and discovered a previously unknown Apple 0day vulnerability assigned a CVE.

Problem

Detecting binary memory corruption vulnerabilities (BMCVs) requires recovering interprocedural object semantics, value-flow propagation, and path-feasibility evidence from stripped binaries where compilation and stripping destroy field boundaries, pointer relations, and high-level control flow. Existing LLM-based agentic approaches developed for source-level analysis—call-graph expansion, summarization, retrieval—fail because they do not reconstruct the memory-relevant semantic structure lost during compilation; without explicit grounding, LLMs hallucinate vulnerability hypotheses from syntactic proxies rather than actual attacker-controlled data propagation paths.

Method

Veritas organizes analysis into three stages around two grounding layers:

Stage 1 — Semantic-driven Context Slicer (defuse): Lifts the binary with RetDec to LLVM IR, then constructs an interprocedural propagation graph encoding def-use, call, return, global access, and pointer operation relations. Performs taint propagation from attacker-controlled sources (file/network/CLI) to memory-risk sinks, emitting compact witness-backed flow objects (source-to-sink chains with taint tokens) for downstream analysis. Operates entirely without LLMs.

Stage 2 — Dual-view Vulnerability Detector (discovery): Reasons over each witness-backed flow function-by-function. Uses RetDec-decompiled C as the primary substrate for control-flow reasoning, and selectively instantiates LLVM IR only at anchor loci (source and sink functions) where decompiled code collapses memory semantics (e.g., param_2 + 0x48 vs. explicit getelementptr). Shared flow prefixes are cached via trie-based memoization to avoid redundant LLM calls. A final self-consistency check verifies end-to-end taint propagation, bounds constraints, and sink conditions before reporting a candidate.

Stage 3 — Automatic Vulnerability Validator (multi-agent): Translates detector hypotheses into executable coordinates and orchestrates three specialized agents — Strategist (sets breakpoints, identifies instrumentation targets), Verifier (generates and executes PoCs, analyzes exploitability), and Explorer (diagnoses failures, probes alternative states, provides feedback) — using Radare2 and Valgrind. A candidate is confirmed only when concrete runtime artifacts corroborate the sink, access pattern, and root cause.

Key Contributions

• Veritas framework unifying static data-flow grounding and runtime execution grounding as two complementary scaffolding layers for LLM-based BMCV detection.
• Three-stage modular pipeline: witness-backed slicer → dual-view step-wise detector with IR-anchor fusion → multi-agent debugger validator.
• Trie-based memoization of shared interprocedural flow prefixes for tractable full-pipeline execution over large binaries.
• A curated binary benchmark with trace-level ground truth covering real-world CVE cases.
• Discovery of a previously unknown Apple 0day vulnerability confirmed and assigned a CVE.

Results

• 90% recall on the curated binary benchmark, outperforming static, dynamic, binary-native, and agentic baselines.
• Exhaustive validation of 623 discovery-stage candidates via the full validator pipeline: 0 false positives in the exhaustive subset.
• Additional audit of candidates from larger cases: 2 manually confirmed false positives.
• Real-world 0day: one previously unknown Apple vulnerability discovered, confirmed, and assigned a CVE.

Limitations

• Scope restricted to out-of-bounds reads and writes; logic flaws and side-channel vulnerabilities are explicitly out of scope.
• Severe lifting or decompilation failures producing unanalyzable LLVM IR invalidate the pipeline.
• Assumes binary access and an isolated execution environment for runtime validation; does not generalize to environments where instrumented execution is unavailable.
• Benchmark is researcher-curated from repository-sourced binaries; generalization to diverse real-world stripped production binaries is not fully characterized in the provided text.

Relevance to Harnesses / Meta-Harnesses

Veritas is a textbook meta-harness: it composes three heterogeneous agents (deterministic static slicer, LLM detector, multi-agent validator) into a sequential pipeline where each stage narrows the reasoning space for the next, preventing any single stage from operating over unconstrained context. The multi-agent Validator sub-harness (Strategist/Verifier/Explorer with feedback loops) demonstrates the standard decompose-execute-verify pattern applied to runtime confirmation. The trie-based memoization of shared flow prefixes is a concrete harness-level optimization showing how structured caching across agent calls reduces redundant LLM invocations. The paper's central principle — semantic grounding constrains what the LLM may reason over and conclude — is a generalizable harness design principle directly applicable to any domain where LLM reasoning quality depends on structured context selection and output verification.