💻 computer science

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

Veritas 是一个基于语义的多智能体框架，它结合了对提升后 LLVM IR 的静态分析、双视图大语言模型推理以及运行时验证，以实现对 stripped 二进制文件中内存破坏漏洞的高召回率、低误报检测，并成功发现了一个此前未知的 Apple 漏洞。

原作者： Xinran Zheng, Alfredo Pesoli, Marco Valleri, Suman Jana, Lorenzo Cavallaro

发布于 2026-05-15

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Xinran Zheng, Alfredo Pesoli, Marco Valleri, Suman Jana, Lorenzo Cavallaro

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

以下是用通俗易懂的语言和生动的类比对论文《Veritas》的解读。

核心难题：“丢失的翻译”

想象你有一台在工厂制造的复杂机器（计算机程序）。工厂保留着原始蓝图（源代码），但你实际收到的机器是一个经过精简的黑盒版本（二进制文件），所有的标签、指令和图表都被移除了。

安全专家需要在这种黑盒中找出“内存破坏”漏洞。这些漏洞就像机器地基中隐藏的裂缝，允许黑客趁虚而入。

问题在于，如果没有蓝图，要看出机器的一个小部件（比如你按下的按钮）如何与盒子内部数英里外的危险部件（比如压力阀）相连，简直难如登天。

旧方法：靠 AI 猜测

最近，人们开始利用强大的 AI（大语言模型）来审视这些黑盒。AI 很聪明；它能读懂机器的“乱码”代码，并尝试猜测裂缝在哪里。

然而，论文指出，AI 就像一位只拥有模糊照片的侦探。AI 能看到轮廓，但无法确定一条线是连接到管道还是电线。因为“照片”（二进制代码）缺失了关键细节，AI 经常：

漏掉真实的裂缝（假阴性）。
把安全区域误认为是裂缝（假阳性）。

解决方案：Veritas（“求真者”）

作者构建了一个名为Veritas的新系统。Veritas 不像以前那样让 AI 自由猜测，而是像一个三步调查团队，迫使 AI 严格遵循事实。

可以将 Veritas 想象为三位协同工作的专家：

第一步：制图师（切片器）

在 AI 查看任何内容之前，一个专用工具（切片器）会扫描黑盒。它不使用 AI，而是利用严格的数学来绘制精确地图。

类比：想象这台机器是一座巨大的城市。切片器忽略了 99% 的城市（安全部分），只画出一条细线，连接“入口”（数据进入处）和“危险区”（数据被使用处）。
结果：它给 AI 提供了一条微小且专注的路径供其调查，而不是整个混乱的城市。这条路径有“证人”（证明数据确实沿此路径传输的证据）作为支撑。

第二步：侦探（双视图检测器）

现在，AI（侦探）查看制图师画出的路径。但这里有个窍门：AI 通过两副不同的眼镜来观察这条路径。

眼镜 A（反汇编代码）：这看起来像可读的英文句子。它帮助 AI 理解正在发生的“故事”。
眼镜 B（LLVM IR）：这看起来像原始的、技术性的蓝图。它帮助 AI 看清确切的“数学”逻辑和内存地址。
类比：如果 AI 对某个路标感到困惑，它会切换到技术蓝图，以确切看清道路通向何方。这防止了 AI 编造与数学逻辑不符的故事。

第三步：法医测试员（验证器）

AI 可能会说：“我认为这里有个裂缝！”但 Veritas 不会只听其一面之词。第三位代理人（验证器）会走出去，对机器进行物理测试。

类比：AI 是法庭上作证说“我看见了一道裂缝”的证人。验证器则是法官，他说：“拿证据来。”验证器使用特殊工具（调试器）运行机器，看机器是否真的会在 AI 声称会出现问题的地方崩溃。
结果：如果机器没有崩溃，该“裂缝”将被驳回。如果机器确实崩溃了，漏洞即被确认。

为何重要（结果）

作者在已剥离标签的真实世界软件上测试了 Veritas。

成功率：Veritas 发现了**90%**的真实漏洞。
准确性：它几乎没有误报。当它声称存在漏洞时，几乎总是真的。
现实胜利：在另一项测试中，Veritas 在苹果公司的软件中发现了一个全新的、未知的漏洞（"0-day"），此前无人知晓。他们上报了该漏洞，苹果确认了它并为其分配了安全 ID（CVE）。

核心结论

论文认为，不能仅靠聪明的 AI 来发现复杂、精简软件中的漏洞。AI 需要落地（Grounding）。

没有落地：AI 就像一个梦想家，想象着可能并不存在的东西。
有了 Veritas：AI 变成了一位科学家。它被提供了一条特定的检查路径（由制图师提供），它用两种不同的工具检查细节（由侦探执行），并通过物理测试证明其发现（由验证器执行）。

通过结合严格的数学、智能 AI 和现实世界测试，Veritas 使得发现危险软件漏洞变得更加可靠和准确。

技术摘要：Veritas

问题陈述

在剥离符号的二进制文件中检测内存破坏漏洞（MCVs）构成了一个根本性的语义重构挑战。与源代码分析不同，二进制分析必须从因编译和剥离而丢失了高层结构、对象边界及显式控制流的产物中，恢复内存对象如何在函数间被分配、传播、约束和访问。

近期基于大语言模型（LLM）的方法虽然提升了代码理解能力，但在二进制 MCV 检测方面仍面临三大主要挑战：

共享状态追踪：漏洞通常源于跨离散函数的共享内存区域假设不一致，而这些函数之间缺乏直接的调用链边。标准的调用图扩展无法捕捉这些依赖关系。
语义丢失：恢复后的表示是碎片化的。提升后的 LLVM IR 保留了底层内存访问模式，但被编译器产物（SSA 变量、类型转换）所遮蔽；而反编译的 C 代码虽然提供了高层结构，却将内存操作坍缩为通用的偏移表达式，抹去了对象身份。
约束验证：静态分析往往无法确定可疑访问是否在可行的路径条件下可达。缺乏可执行证据时，LLM 依赖语法代理而非攻击者控制数据如何传播至内存敏感操作的证明，导致推理脆弱且误报率高。

现有的专为源代码设计的智能体框架（依赖摘要或调用图扩展）无法解决剥离二进制文件所提出的语义恢复问题，因为在这些文件中，所需的语义结构在构建时即已部分缺失。

方法论

Veritas 是一个混合的、基于语义的智能体框架，旨在将 LLM 的推理约束于可验证的程序语义和可执行行为之上。它将分析组织为三个阶段，并对应两个基础层：静态基础（恢复的程序事实）和运行时基础（具体执行证据）。

1. 语义驱动的上下文切片器（静态基础）

切片器在不使用 LLM 的情况下，从提升后的 LLVM IR 中提取紧凑的、有证据支持的源点到汇点流。

过程间传播图：它利用 RetDec 将二进制文件提升为 LLVM IR，并构建一个类型化的过程间传播图（ $G_P$ ），编码调用、返回及全局依赖关系。该图追踪与污点相关的值（指针、偏移量、长度）如何在函数间传播。
基于证据的流提取：切片器并非将所有可达的源点 - 汇点对视为有意义，而是验证有界的过程间证据。它追踪从输入源（如 fread）到内存风险汇点（如危险 API 参数）的污点令牌，并在每个函数边界利用定义 - 使用链和元数据验证传播过程。
流对象构建：被接受的证据被转换为紧凑的流对象，其中包含有序函数、污点相关令牌以及“锚点线索”（来源类别和端点注释）。这用一个小而语义完整的上下文替代了整个二进制文件，供下游分析使用。

2. 双视图漏洞检测器（受控 LLM 推理）

检测器利用双视图输入表示来克服语义丢失，对证据支持的流进行逐步推理。

双视图表示：对于源点和汇点函数，LLM 同时接收反编译的 C 代码（用于控制流推理）和提升后的 LLVM IR（用于消除内存操作和汇点语义的歧义）。对于中间函数，它主要使用由锚点线索引导的反编译代码。
逐步推理：LLM 一次分析一个函数的流，维护一个累积的推理状态（传播值、别名和边界的清单）。它根据赋值和控制流决策更新此状态，避免了同时处理整个流所带来的上下文限制。
基于 Trie 的记忆化：为了减少冗余，系统对共享流前缀的推理状态进行记忆化，仅在流的唯一后缀部分调用 LLM。
一致性检查：在报告候选项之前，检测器执行最终的路径敏感验证，以确保污点值保持与漏洞相关，并且汇点访问在可行条件下违反了内存安全。

3. 自动漏洞验证器（运行时基础）

验证器将检测器的假设转化为可执行检查，以确认或反驳候选项。

产物准备：它利用 Radare2 将检测器假设映射到可执行坐标（RVA、符号），弥合反编译器视图与运行时调试之间的差距。
多智能体协作：三个智能体协调验证过程：
- 策略制定者：规划验证，选择插桩目标、断点和触发模式（文件、网络、命令行）。
- 验证者：执行计划，生成概念验证（PoC），并在调试器（Radare2）或内存检查器（Valgrind）下运行二进制文件，以观察崩溃或无效访问。
- 探索者：如果初始证据不足，则探测替代状态或相关函数以寻找支持性证据。
确认：仅当具体的运行时证据（如段错误、Valgrind 错误或特定内存状态）证实了报告的汇点、访问模式和根本原因时，漏洞才被确认。

主要贡献

Veritas 框架：一个基于语义的智能体框架，统一了静态程序分析和运行时验证，以检测剥离二进制文件中的内存破坏漏洞。
三阶段架构：
- 一个切片器，在不使用 LLM 的情况下从提升后的 IR 中提取有证据支持的流。
- 一个双视图检测器，利用选择性 IR 支持对流进行推理，以解决语义歧义。
- 一个验证器，利用调试器可见的产物和具体执行来确认假设。
细粒度基准：一个包含 20 个真实世界二进制内存破坏案例的精选数据集，具有追踪级真值，旨在评估基于基础的二进制检测。
性能：评估显示，Veritas 在基准测试中实现了90% 的召回率，显著优于静态分析器（0% 召回率）、模糊测试（10% 召回率）和智能体基线（25–35% 召回率）。在对 623 个候选项的全面验证中，它产生了零误报，在更大规模的抽样审计中仅产生 2 个误报。
真实世界发现：Veritas 发现了 Apple 通用场景描述库（libusd_ms.dylib）中一个此前未知的零日越界读取漏洞，该漏洞已得到确认并被分配了 CVE。

结果与意义

该论文指出，基于 LLM 的漏洞发现的有效性不仅取决于模型本身的内在能力，还取决于周围基础设施恢复推理所需语义结构的能力。

语义基础作为设计原则：结果支持将语义基础作为操作设计原则。通过将 LLM 推理约束于显式的内存相关事实（静态基础），并根据可执行行为验证结论（运行时基础），Veritas 避免了无约束模型推测的脆弱性。
优于基线：传统工具因缺乏跨函数的语义基础而失败。智能体基线失败是因为缺乏内存对象生命周期的显式模型，并依赖无引导的探索或语法模式。Veritas 通过使用确定性分析预计算传播、利用 LLM 解释复杂语义，随后进行严格的运行时确认，从而弥合了这一差距。
成本 - 精度权衡：虽然运行时验证是主要的成本瓶颈（需要生成 PoC 和调试），但该框架表明，只有通过可执行证据才能在剥离二进制分析中实现高精度。该系统优先考虑检测可靠性而非吞吐量，这是安全关键型二进制分析的必要权衡。

该论文得出结论：对于实用的二进制漏洞检测，推理必须植根于恢复的程序语义和可执行证据之中，Veritas 通过其模块化混合架构实现了这一原则。