Veritas: A Grounding Framework for Reliable Vulnerability Reasoning on Stripped Symbolic Binaries by LLM Agents

Researchers propose Veritas, a three-stage framework that formalizes vulnerability reasoning on stripped symbolic binaries as a semantic grounding problem, enabling LLM agents to judge vulnerabilities based on verifiable evidence rather than direct inference. The framework first uses a static analysis Slicer to recover evidence-backed source-to-sink flows from lifted LLVM IR, then an LLM-based Discover stage aligns decompiled code with IR evidence to generate vulnerability claims, and finally a multi-agent Validator verifies them through guided debugging and runtime oracles. On a curated benchmark targeting out-of-bounds vulnerabilities with flow-level annotations, Veritas achieves 90% recall, surpassing static, dynamic, binary analysis and agent baselines, with no false positives among 623 exhaustively verified candidates and only 2 false positives observed in sampled audits. In a real-world case study, Veritas discovered a previously unknown Apple vulnerability, which was confirmed and assigned a CVE.