Trail of Bits复盘AI辅助审计

Trail of Bits 9月18日发布的复盘，把 AI 辅助安全审计的重心放在正式代码审查之前。文章给出一条具体生产路径：当目标生态缺少工具时，先用 agent 把语言服务、反编译、静态分析和形式化模型补起来。

本次新增的事实来自 9 月 18 日的 Trail of Bits 官方复盘。公司称，面对 Miden zkVM 这类新架构和自定义汇编语言 MASM，它们在审计前用了6个月，让 agent 构建 LSP、反编译器、静态分析引擎和 Lean VM 模型。实际审计中，这些工具发现了400多个可改进的类型验证位置、1个高危问题，并让 Lean 工作产出95个机器检查正确性证明。

这不代表 AI 已经可以独立完成高保障审计。原文里的角色分工很清楚：Claude 和 Codex 被用来规划、开发、代码审查、跑回归和生成证明脚手架；关键目标选择、工具边界、漏洞解释、证明陈述审计和最终判断仍由安全研究人员完成。更准确的说法是，agent 把原本“值得做但客户很难提前为其买单”的侧线工程变成了审计准备的一部分。

对安全团队和高保障系统开发者而言，这个案例的价值在于方法和产物。若目标语言缺 LSP、缺反编译器、缺类型验证、缺形式化语义，agent 的高杠杆位置可能是先把“代码能否被人和机器共同理解”这件事做扎实。

这次新增了什么

Trail of Bits 的新闻锚点是 9 月 18 日发布的长文《Auditing in the age of (good enough) AI》。文章开头把定位说得很直接：过去很多安全公司文章强调 agentic code review，也就是把 agent 指向代码库让它找漏洞；这次它们想讲的是代码审查之前的工作，agent 可以帮助构建自定义工具和形式化模型，从而提高安全审计的质量和深度。

审计对象是 Miden VM。Miden 文档把它定义为用 Rust 编写的 zero-knowledge virtual machine：程序在 Miden VM 上执行后，会自动生成基于 STARK 的执行证明，其他人可在不重新执行程序、甚至不知道程序内容的情况下验证执行正确性。Miden assembly，也就是 MASM，则是运行在这个 VM 上的低层语言。文档强调，MASM 位于原始 VM 指令集之上，很多指令直接映射到底层指令；它保留了对 VM 栈的直接访问，同时提供过程、控制流和宏指令等更稳定的外部接口。

这正是审计难点。Trail 写到，Miden core library 中有一组用 MASM 编写的密码学原语。MASM 面向栈机器，指令输入和输出经常隐含在栈上；Miden 又是新架构，审计开始时缺少 IDE 支持、LSP、linter 等成熟工具。传统审计在这种场景下会先消耗大量人工去恢复上下文：某个过程需要几个输入，调用后留下什么输出，分支和循环是否保持栈形状，advice 输入是否被约束。Trail 的做法是把这部分准备工作提前半年交给 agent 辅助推进。

关键事实可以压缩成这张审计链路表：

这里有两个事实边界。400多个指类型验证可改进位置，不应解读为400多个漏洞。Trail 的脚注说明，这些位置大多与 core library 中几乎所有 procedure 都是公共 API 有关，意味着第三方开发者可以在没有足够验证的情况下调用。95个指机器检查的正确性证明，且仓库 README 明确分布在 u64、u128、u256 和 word 组件里；它不应该被外推成 Miden VM 已被形式化验证。

工具链实际补了哪些缺口

第一层是 MASM LSP。masm-lsp README 显示，这个 language server 可用于支持 LSP 的 IDE，并由 VS Code MASM 扩展自动安装。它提供的功能包括 call target 和 constant 的 go-to-definition、find-references、hover 信息、语法错误和未定义符号诊断、指令说明或反编译结果的 inlay hints、procedure 或整个文件的反编译，以及指令栈效果 code lens。对于人工审计，这些能力的意义很朴素：先让审计者能在一个低层栈语言里可靠导航。

第二层是反编译器。masm-decompiler README 把它称为面向 Miden assembly 的 best-effort decompiler，用于给 MASM procedure 提供更高层表示。它同时列出 MASM 反编译困难：exec 调用没有稳定 ABI，很多 procedure 没有声明签名，while 循环不一定保持栈中性，条件分支也可能有不同栈效果。架构文档进一步说明，它只支持栈效果可静态确定的指令和结构，流程包括调用图生成、签名推断、提升到 SSA、优化、格式化，并旁路实现类型推断。

第三层是静态分析。Trail 原文写到，反编译器最大的收益来自内部分析框架和中间表示，后续可以复用于静态分析。基于这个 IR，团队构建了分析 pass，回答 prover-supplied advice values 是否经过验证、输入是否满足 32-bit integer 或 boolean 等类型约束、局部变量是否在所有路径初始化等问题。LSP README 也显示，诊断能力包含“因类型验证不足导致的潜在类型错误”和“无效 procedure 签名”。

第四层是 Lean 模型。masm-lean README 显示，这个项目用 Lean 4 对 Miden Assembly core library 做形式化验证：MASM 程序被 shallow embedding 翻译为 Lean 的 List Op 定义，正确性则相对于一个可执行的 Miden VM 语义来证明。仓库列出的组件包括 MidenLean/ VM 模型、MidenLean/Generated/ 生成的 MASM procedure 定义、MidenLean/Proofs/ 手写正确性证明，以及 masm-to-lean/ Rust 转译工具。

这张表说明，AI 的贡献由一组互相支撑的工程产物组成。LSP降低人工理解成本，反编译器产生更高层 IR，静态分析在 IR 上跑规则，Lean 模型则用另一种方式检查 procedure 的语义陈述。每一层都不完美，但叠加后能把审计从一次性人力阅读扩展成可复用工具链。

漏洞发现来自哪里

静态分析最直接的成果，是发现超过400个类型验证可改进位置。Trail 原文强调，这些位置都可从 library 的 public API 触达。对一般应用来说，“类型验证可改进”听起来不像高危漏洞；但在零知识 VM 和加密原语里，外部提供的 witness、advice 或 stack value 一旦未被约束，可能让证明系统验证了一个不符合预期的计算。

高危发现出现在 mod_12289 procedure。这个过程把一个 64 位值对 12289 取模，quotient 和 remainder 由 prover 作为 advice values 提供。Trail 写到，quotient 会被检查为有效的 64-bit value，也就是两个 32-bit limbs；但 remainder 在传给 32-bit 指令 u32overflowing_sub 之前没有被验证。研究者通过调整 quotient 和 remainder，让它们仍满足 subtraction 施加的约束，却能让 mod_12289 返回不正确的 remainder。

这个漏洞为什么严重，和 Falcon 签名相关。Trail 的结论是，恶意 prover 可以利用该问题伪造 Falcon signatures，并从由 Falcon key pair 控制的 Miden 账户中转走资金。这里的表述需要保持“could exploit”的条件语义：原文说的是可以被恶意 prover 利用，造成伪造签名和资金被盗的风险；它不是在说已经发生了链上盗窃事件。

Lean 工作发现的两个 bug 则展示了另一类价值。第一个是 64-bit right-rotation rotr 的边界问题：当输入大于 Goldilocks prime 且 rotation shift 是 32 的倍数时，行为不正确。第二个是 256-bit multiplication wrapping_mul 的栈行为问题：返回前会丢掉 caller-owned values。它们被称为 subtle bugs，说明其价值不在“危害巨大”，而在单元测试没有覆盖、但形式化证明迫使团队把语义条件写到足够精确。

为什么这个案例比泛泛宣传更硬

很多“AI 审计”材料的问题，是只展示最终命中的 bug，缺少对模型失败约束方式的说明。Trail 这篇的可信度更高，原因有三点。公开仓库包括 masm-lsp、masm-decompiler 和 masm-lean，读者可以检查工具目标与实现范围。反编译器明确聚焦可正确反编译的子集，没有承诺覆盖全部 MASM。Lean 证明还需要 kernel 检查，agent 生成的证明若不能通过类型检查就不会成立。

同时，也不能把这个案例泛化过度。Miden 的特征非常适合这套打法：MASM 是小而低层的语言，core library 有大量可复用的整数和 word procedure，VM 指令集相对适合形式化建模，且审计前刚好有6个月准备窗口。换成一个庞大、动态、依赖复杂、业务状态散落在外部服务里的 Web 应用，agent 未必能用同样投入换来 LSP、反编译器和可执行语义模型。

另一个限制是维护成本。Trail 原文说，Miden team 已经采用了这次审计开发的静态分析引擎，这让工具有机会继续保护后续 core library 更新。但 LSP、反编译器和 Lean 模型都不是一次性报告里的截图；只要 MASM 语义、库结构或 VM 指令发生变化，它们就需要跟着更新。agent 可以降低开发成本，不会自动消除维护责任。

对读者的直接影响

对安全审计团队，最可复制的动作是先识别“审计前缺什么工具”。如果目标系统有自定义 DSL、IR、字节码或链上语言，先做 LSP、索引、调用图、签名推断和简单 lint，往往比立刻要求模型找漏洞更有效。工具越接近语言语义，agent 后续审查越少依赖上下文猜测。

对 zkVM 和密码学库团队，Miden 案例提醒的是 public API 边界。Trail 提到的400多个验证改进位置，不等于每个点都能直接变成盗币漏洞；它说明在低层库里“调用者会按预期给入参”这个假设很危险。只要 procedure 可以被第三方调用，类型约束、advice 约束和栈形状约束都应尽量在代码或工具里显式化。

对采用 AI 工具的企业买方，这篇文章提供了一个更好的验收问题：供应商是否只交付 bug 列表，还是同时交付可持续使用的分析工具、测试和证明材料。后者更难包装，但更接近长期安全收益。Trail 的复盘之所以值得看，正是因为它把 agent 产物从一次性输出变成了 Miden 后续维护可以继续使用的工程资产。

后续应当看什么

先看 Miden 是否把这套静态分析引擎放进常规开发流程。若它进入 CI 或发布前检查，说明审计工具真正变成项目治理的一部分；若只停留在审计期间，价值就更接近一次性加速。

masm-lean 的覆盖范围也会决定这条路线的上限。当前 README 列出95个手写正确性证明，其中 u64 31 个、u128 36 个、u256 17 个、word 11 个。这已经覆盖 core library 的大型算术组件，但还没有证明整个 VM、全部库或所有宿主交互。后续如果能覆盖更多 advice、memory、host 和 control-flow 语义，形式化工作才会从局部证明走向系统级保障。

安全行业还要回答商业化问题。Trail 这次有半年的准备窗口，不是每个项目都有。若客户只愿意为最终报告付费，agent 只能压缩报告生成成本；若客户愿意为可维护工具链付费，AI 辅助审计才有机会从演示走向标准工作流。