Veritas：程序语义依据关联 LLM 代理以对剥离的二进制文件进行可靠的漏洞推理

Frontier LLM 代理本地化可疑代码的能力越来越强，但漏洞推理需要的不仅仅是访问程序工件。代理必须携带实际决定漏洞是否存在的证据。否则，与安全相关的事实可能存在于工件中，但在用于证明声明合理性的推理中却缺失，从而在可用的程序事实和代理使用的证据之间产生语义差距。对于剥离的二进制文件来说，这个问题尤其严重，其中源级线索被删除，相关证据在嘈杂的提升 IR 和有损反编译视图中支离破碎。我们将剥离二进制漏洞推理制定为语义基础问题，并提出 Veritas，这是一个用于可靠分析的三阶段框架。首先，静态分析切片器从提升的 LLVM IR 恢复见证支持的源到接收器流。其次，基于 LLM 的 Discover 阶段将反编译代码与 IR 见证进行对齐，以构建漏洞声明。第三，多代理验证器通过引导调试和运行时预言机检查这些声明。这些阶段共同将碎片化的二进制视图转变为可检查的声明，而不是依赖于直接代理推理。我们针对越界漏洞实例化 Veritas，并在带有流级注释的策划基准上对其进行评估。 Veritas 实现了 90% 的召回率，优于静态、动态、二元分析和代理基线，并且在 623 个经过详尽验证的候选者中没有报告误报，并且在抽样审计中仅观察到两个误报。在现实世界的案例研究中，Veritas 发现了一个以前未知的 Apple 漏洞，该漏洞已得到确认并分配了 CVE，这表明有根据的推理可以产生超出策划基准的可操作的发现。