AI 中文总结
研究旨在在不过高成本下实现高召回率漏洞发现与可靠自动验证。核心方法是结合神经符号检测器合成与可利用性预言机的反证法系统。主要贡献是在多数据集和系统扫描中表现出色，发现大量未知漏洞并获多个CVE编号。
AI 中文摘要
在攻击者利用漏洞之前发现漏洞需要高召回率和可靠的自动验证，但现有方法难以在不过高成本的情况下同时实现这两点。我们提出了反证法（Antiproof），这是一个端到端的漏洞发现系统，它将用于高召回率发现的神经符号检测器合成与用于自动验证的可利用性预言机相结合。反证法从漏洞数据集中学习并迭代改进静态检测器，然后通过验证可执行证明是否展示了具体攻击者能力来验证候选漏洞。在BountyBench和我们精心整理的KEVBench数据集上进行评估，反证法检测出66个漏洞中的64个，比静态分析和神经符号基线的召回率提高了60多个百分点。在对50个广泛部署的系统进行扫描时，反证法发现了数百个以前未知的漏洞。我们正在负责任地披露所有已确认的零日漏洞，到目前为止已获得12个CVE编号，包括Ray、SGLang、vLLM和LiteLLM中的远程代码执行漏洞，这些漏洞可能使攻击者接管大语言模型训练和推理系统。
英文摘要
Discovering vulnerabilities before attackers exploit them requires high recall and reliable automatic validation, but existing approaches struggle to achieve both without prohibitive cost. We present Antiproof, an end-to-end vulnerability discovery system that combines neuro-symbolic detector synthesis for high-recall discovery with proof-of-exploitability oracles for automatic validation. Antiproof learns and iteratively refines static detectors from vulnerability datasets, then validates candidates by verifying whether executable proofs demonstrate concrete attacker capabilities. Evaluated on BountyBench and our curated KEVBench dataset, Antiproof detects 64 of 66 vulnerabilities, improving recall by more than 60 percentage points over static-analysis and neuro-symbolic baselines. In a scan of 50 widely deployed systems, Antiproof uncovered several hundred previously unknown vulnerabilities. We are responsibly disclosing all confirmed zero-days and have received 12 CVE assignments to date, including remote code execution vulnerabilities in Ray, SGLang, vLLM, and LiteLLM that could allow attackers to take over LLM training and inference systems.
Comments17 pages, 7 figures
