在'足够好'AI时代的安全审计

# “在（足够好用的）AI时代进行审计” 来源：https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/ 安全公司已发布大量博文，描述如何将他们的智能体框架应用于代码库并发现数十个漏洞（我们也是其中之一 (https://blog.trailofbits.com/tags/patch-the-planet/)）。然而，这些文章往往侧重于智能体代码审查，而这只是我们在安全审查中使用AI的一个方面。我们希望提供一个不同的视角：在代码审查开始之前，智能体现在让我们能够构建定制工具和形式化模型，从而提升审查的质量与深度。 我们最近审查了Miden虚拟机（一种拥有自定义汇编语言、几乎没有任何开发者工具链的新型零知识虚拟机）。为准备工作，我们花了六个月时间，让智能体从头开始构建了一个LSP服务器（https://github.com/trailofbits/masm-lsp）、一个反编译器（https://github.com/trailofbits/masm-decompiler）、一个静态分析引擎（https://github.com/trailofbits/masm-lsp/tree/main/crates/masm-analysis）以及一个关于VM执行器的Lean模型（https://github.com/trailofbits/masm-lean）。这些工具发现了真实的安全问题，例如一个未经验证的证明者输入，该输入可能允许恶意证明者伪造Falcon签名并窃取Miden账户持有者的资金。此外，Lean的工作产出了95个机器验证的正确性证明，涵盖了Miden核心库的大部分组件。 ## 审计Miden zkVM 2025年末，Miden团队找到我们，希望在其启动前审查他们的零知识虚拟机（https://docs.miden.xyz/reference/miden-vm/）的部分内容。审查范围的一部分覆盖了Miden核心库，该库包含一小套用称为Miden汇编（MASM）（https://docs.miden.xyz/reference/miden-vm/user_docs/assembly/）的自定义汇编语言编写的密码学原语。这让我们非常兴奋，因为这正对我们的胃口：一个使用我们从未见过的底层自定义汇编语言编写复杂密码学代码的高保证项目。同时，这也带来了一些独特的挑战。 “并排的两段代码列表：一段计算两个128位值异或的MASM过程，以及同一过程的32位x86汇编实现”图1：左图显示了一个计算两个128位值（表示为32位片段）异或的MASM过程。右图显示了使用32位x86汇编代码实现的同一过程。首先，Miden虚拟机实现了栈机架构（https://en.wikipedia.org/wiki/Stack_machine）。这意味着每条指令操作从栈中读取的值，然后将指令结果写回栈顶。虽然概念简单，但这使得用MASM编写的代码难以审查，因为指令的输入和输出都是从栈中读取的，并且始终是隐式的。此外，由于Miden虚拟机是一个全新的架构，几乎没有IDE支持、语言服务器协议（LSP）服务器和代码检查器等开发者工具。 我们知道有六个月的准备时间，因为实现尚未完成全部功能，所以我们问自己：*“我们应该如何分配时间和算力，以确保审查能尽可能多地在代码库中发现漏洞？”* 由于MASM缺乏开发者工具，我们首先思考的是：当项目开始时，我们希望拥有什么样的工具。我们通常使用VS Code进行代码审查，语法高亮和代码导航对于代码的可读性和在整个代码库中跟踪数据流至关重要。为此我们需要一个LSP服务器和相应的VS Code扩展，几天之内，我们就让Claude构建了一个可用的原型（https://github.com/trailofbits/masm-lsp），它提供了我们所需的大部分功能：如语法高亮、跳转到定义、查找代码引用以及在悬停时显示过程文档字符串。在这些基本功能的基础上，我们还决定添加更多特定于语言的功能，例如显示内联指令文档和单个指令的栈效应。 “展示带有内联栈效应和指令文档的代码标注的示意图，有助于避免为查找指令语义而进行的上下文切换”图2：在代码上标注内联栈效应和指令文档，有助于避免为在其他地方查找指令语义而进行的上下文切换。构建了LSP服务器后，我们开始思考如何提供高级语义信息，以支持人工和智能体驱动的审查。我们想看看是否能在VS Code界面中为MASM过程提供忠实的反编译，以帮助审查者快速理解他们所查看过程的高级控制流和数据流。对于MASM，这个问题比初看起来更难。栈机提升和反编译是一个研究得很好的问题，但反编译手写的MASM仍然由于多种原因而相当困难。 1. 核心库中的大多数过程没有声明签名，这意味着输入和输出的数量必须从上下文中推断。 2. MAS过程不遵循明确定义的调用约定，此类调用的净栈效应通常无法静态确定。这意味着所有分析失败都会沿调用链向上传播。 3. While循环不需要保持栈中性，这意味着while循环条件可能在每次迭代中占据不同的栈槽。这也使得无法将后续指令的输入映射到栈槽。 4. 条件语句中的不同分支可能具有不同的栈效应，这同样使得栈跟踪和签名推断变得具有挑战性。 这意味着，如果我们还希望反编译输出是正确的，就不能指望能反编译所有MASM过程。因此，我们专注于正确地反编译一个明确定义的MASM子集。在开发反编译器的过程中，我们在使用Claude进行规划和开发，以及使用Codex进行代码审查之间交替。每当我们实现一个新功能时，我们就会让智能体反编译核心库中的一个随机过程集，并将结果与原始MASM进行比较以查找回归问题。发现的任何问题都会作为回归测试添加，由模型修复。 “上方展示的eqz MASM过程及其反编译的伪代码”图3：`eqz`过程（测试一个256位整数（表示为八个32位片段）是否等于零）及其相应的反编译伪代码。反编译器（https://github.com/trailofbits/masm-decompiler）是本项目工具开发的最大努力成果，在数月内产生了超过100个AI生成的提交。这项工作的主要好处原来是反编译器的内部分析框架和中间表示，我们可以将其重用于静态分析，而不是完整的反编译流程。 反编译器就绪后，我们可以访问每个过程的中间表示，其中指令输入和输出被填充为表达式。这使我们能够将所有标准的静态分析机制（如数据流分析）应用于在MASM代码中发现漏洞的问题。我们利用这一点构建了许多分析过程（https://github.com/trailofbits/masm-lsp/tree/main/crates/masm-analysis）来处理中间表示，回答诸如以下的问题： 1. 证明者提供的建议值1 (https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/#fn:1)（如余数和模逆元）是否经过适当验证？ 2. 类型约束（例如，输入是32位整数还是布尔值）是否被强制执行？ 3. 局部变量是否在所有执行路径上都已初始化？ 探索这些问题的一种方法是抽象解释。这项技术背后的理念很简单。分析不是用真实数字运行程序，而是跟踪每一步栈上可能出现的值的类型，例如“一个32位整数”或“未知”。它反复遍历代码，直到找不到新信息为止。由于它总是跟踪每个可能的值（预留少量额外空间），因此它永远不会错过真实情况。所以，如果检查在分析中通过，那么在实际的程序运行中也保证成立。 我们使用Claude和Codex构建了一个通用的抽象解释引擎，然后在此基础上实现了多个具体的分析过程，让智能体在开发和代码审查之间切换，如上所述。我们还决定让智能体为反编译器和一个新的MASM代码检查器设计并构建命令行接口，使这些新工具也能用于智能体驱动的代码审查工作流。 ## 发现所有漏洞！ 在实际审查过程中，这些分析识别出了400多个可改进类型验证的独特位置2 (https://blog.trailofbits.com/2026/09/18/auditing-in-the-age-of-good-enough-ai/#fn:2)（所有位置都可从库的公共API访问），以及一个高危漏洞。 “展示从建议栈中读取余数，但未验证其是否为有效64位整数的示意图”图4：余数是从建议栈中读取的，但未验证其是否为有效的64位整数。高危问题源于`mod_12289`过程中的一个约束不足的建议值，该过程将一个64位值对`12289`取模，商和余数作为建议值由证明者提供。商经过检查以确保其为有效64位值（表示为两个32位片段），但余数在传递给32位指令`u32overflowing_sub`之前从未得到验证。通过仔细调整商和余数以确保它们仍满足减法施加的约束，我们发现可能使`mod_12289`返回的值不是正确的余数。恶意证明者可以利用这一点伪造Falcon签名，并盗取任何由Falcon密钥对控制的Miden账户资金。 ## 但如果不存在漏洞呢？ 所有这些工作意味着，在审计开始时，我们拥有一套全面的工具来支持人工和智能体驱动的代码审查。然而，我们花了很长时间思考其他支持人工审查流程的方法，并且我们还有更多想法想要测试。例如，如果核心库中的过程都正确实现且没有漏洞，那么是否可以使用像Lean (https://lean-lang.org/) 这样的证明助手来证明这一点？ 事实证明，Miden虚拟机非常适合形式化建模，因为指令集很小，且大多数指令没有副作用。为了形式化建模MASM，我们首先在Lean (https://github.com/trailofbits/masm-lean)中实现了一个最小的Miden VM执行器，并让Claude构建了一个从MASM过程到Lean的自动转换器。在审查期间，我们让多个智能体并行工作，以证明库中尽可能多的过程的正确性。由于Lean内核可以验证生成的证明是否正确，我们只需要人工审核定理陈述，以确保每个定理都证明了相应过程的正确属性。为了确保定理易于审查，我们为域元素和核心库中实现的整数类型引入了Lean类型。这意味着从高层次上看，大多数正确性属性可以表达为以下形式： > 如果栈由`[x1, x2, x3, ..., xn, ...]`给出，我们执行过程`P`，那么`P`终止且栈变为`[P(x1, x2, x3, ..., xn), ...]`。 图5：带有`n`个参数的过程`P`的高级正确性陈述。我们智能体驱动的形式化建模工作产出了95个正确性证明，覆盖了核心库的所有二进制算术组件。这项工作还发现了两个现有单元测试套件未能捕获的细微错误。第一个是64位右旋转`rotr`的一个边界情况：当旋转位移是32的倍数时，如果输入值大于Goldilocks素数，则行为不正确。第二个是256位乘法`wrapping_mul`中的一个问题，它在返回之前会从栈中丢弃调用者拥有的值。 “展示人工审查结果的示意图”图6：人工审查发现64位`rotr`过程的正确性证明需要一个额外的假设（`shift mod 32 ≠ 0`）才能成立。## 为什么两年前我们做不到 我们在此次合作之前开发的工具，以及在审查过程中生成的Lean库和证明，都是我们一两年前无法投入时间或资源的副业项目。这类项目通常具有高度探索性，最终结果和潜在回报难以预测。实际上，这意味着很难提前向客户推销这些项目。然而，在过去的一年里，智能体已经变得足够好，只需少量监督就能完成此类非核心项目，这彻底改变了哪些项目值得追求的经济性。如今，一个失败的副业项目只消耗算力。 对于Miden来说，所有这些准备工作的益处是显而易见的。LSP服务器和静态分析引擎提高了我们人工审查的覆盖率，加强了智能体驱动的审查，并在代码库中发现了可能导致数百万美元损失的真实安全问题。AI生成的Lean正确性证明也提高了库中一个大型基础组件的保证级别，使团队能够放心地继续在此基础上构建。团队已经采纳了为本次审查开发的静态分析引擎，这意味着我们的副业项目现在也将有助于保护Miden核心库未来的更新。 就个人而言，这是我多年来在Trail of Bits工作过的更有趣的项目之一。如果你对这类工作感兴趣，或者你正在构建类似的东西，请联系我们 (https://trailofbits.com/contact/)。我们很想听听！