Veritas: Grounded Binary Vulnerability Discovery

Arxiv pdf 2026-05-01T00:00:00
arXiv Paper — PDF not available. Only the Executive Summary is available here. To read or download the full paper, visit the arXiv abstract page.

Abstract

Frontier LLM agents show promise for vulnerability reasoning and can often localize suspicious code. However, access to program artifacts does not itself specify which facts an agent should carry forward to justify a vulnerability claim. Without an explicit obligation to justify each vulnerability claim against the evidence that decides it, safety-relevant facts may be present in the artifact yet absent from the reasoning that supports the claim. This creates a semantic gap between the facts available in the artifact and the evidence the agent actually uses to support the claim. In stripped-binary analysis, this gap is especially acute because source-level cues are removed and evidence is fragmented across noisy lifted IR and lossy decompiled views. Closing it requires grounding reasoning in recovered program semantics and checking the resulting claims against executable behavior. Building on this principle, we formulate binary vulnerability reasoning as a semantic grounding problem and present Veritas, a three-stage framework for reliable analysis over stripped binaries: a static-analysis Slicer recovers witness-backed sourceto-sink flows from lifted LLVM IR, an LLM-based Discover stage aligns decompiled code with IR witnesses to construct vulnerability claims, and a multi-agent Validator checks these claims through guided debugging and runtime oracles. Together, these stages turn fragmented binary views into checkable claims rather than direct agent inference. We instantiate Veritas for outof-bounds vulnerabilities and evaluate it on a curated benchmark with flow-level annotations. Veritas achieves 90% recall, outperforms static, dynamic, binary-analysis, and agentic baselines, and reports no false positives among 623 exhaustively validated candidates and only two observed false positives in sampled audits. In a real-world case study, Veritas discovered a previously unknown Apple vulnerability that was confirmed and assigned a CVE, showing that grounded reasoning can produce actionable findings beyond the curated benchmark.

Loading executive summary...

LINK COPIED TO CLIPBOARD