一份 zkVM 审计，最危险的漏洞不是靠模型读一遍代码找出来的。

Trail of Bits 在审计 Miden 之前，让 Agent 花了六个月，从零补出 MASM 的 LSP、反编译器、静态分析引擎，以及一份 Lean 的 VM 执行器模型。最后，它们不仅抓到一个可能让恶意 prover 伪造 Falcon 签名、进而盗取资金的高危漏洞，还定位了 400 多处类型验证缺陷，产出了 95 个机器验证的正确性证明，并找到了两个原有单元测试没有覆盖到的细微 bug。

很多人看到这类新闻，第一反应会是，Agent 已经能做安全审计了。

我觉得这个结论太快了。

更有价值的信号恰恰相反。这个案例说明，面对陌生语言、复杂虚拟机和高价值资产，Agent 的第一份工作不该是找漏洞。它得先把系统变成一个可以被检查、被提问、被反证的对象。

审计不是模型能力的展示场。审计是证据生产。

代码能跑，不等于它能被可靠地审

传统代码审计很依赖两件事，专家经验和已有工具。前者知道哪里容易出事，后者把肉眼不该重复做的检查机械化。

问题是，很多新系统偏偏两样都不充足。

Miden 使用 MASM 这类专用汇编语言。对外部审计团队而言，公开生态里的 parser、语言服务、反编译器、静态检查器都未必齐全。一个资深安全研究员当然可以逐文件阅读，可这会马上碰到三个实际问题。

第一，阅读无法自然扩展。代码量增长后，审计结论很容易变成一些局部印象，知道某个函数看起来不对，却很难说明所有类似位置是否已被检查。

第二，手工推理很难复现。今天发现一条栈平衡错误，明天要怎么确保新的改动没有再引入一条？靠审计报告提醒，还是靠某位研究员记得？

第三，复杂系统真正棘手的 bug 往往不是某行代码明显写错，而是两套语义在边界处没有对齐。类型检查、序列化、寄存器约束、异常路径、证明系统的假设，单独看都合理，组合起来却留了缝。

这也是为什么我对「把代码喂给模型，再问它有没有漏洞」一直很谨慎。它可以给出线索，也能帮你快速熟悉仓库。但如果没有结构化证据、没有独立的执行模型、没有可以持续运行的检查，模型的好答案很难变成可交付的审计结论。

安全团队真正需要的，不是一段漂亮的解释。

是下一次还能跑出来的证据。

Trail of Bits 先造的不是 Agent，是审计仪器

从已披露的信息看，这个项目的路径很克制。Trail of Bits 没有让 Agent 直接接管审计结论，而是持续让它完善四类基础能力。

LSP 解决的是理解问题。它把符号跳转、引用关系、类型信息带到编辑器和分析流程里。对一门专用语言来说，能准确回答「这个操作数来自哪里」「哪个过程会调用这里」「这个声明有哪些使用点」，本身就能砍掉大量无效浏览。

反编译器解决的是可读性问题。汇编和 VM 指令对人类审计者不友好，尤其当控制流、栈操作和隐含状态混在一起时。反编译并不会自动得到真相，可它能生成更适合审阅和比对的中间视图，让研究员不必把所有注意力耗在逐条翻译指令上。

静态分析引擎解决的是覆盖问题。它把「我怀疑这里存在类型验证问题」转换成「让规则扫描全仓库，告诉我类似模式到底出现过多少次」。最终定位到 400 多处类型验证缺陷，价值不只是发现很多 issue，更是把漏洞类别从一个偶然发现变成了可枚举、可处理的工作清单。

Lean 执行器模型解决的是语义问题。它不只是再写一个模拟器，而是把 VM 的关键执行规则放进可被机器检验的形式化系统。95 个正确性证明听着很学术，工程上它的意思很朴素，至少有 95 条关于行为的断言，不再只依赖某个人「看起来没问题」的判断。

你会发现，Agent 在这里的角色和很多演示视频很不一样。

它不是万能审计员，更像一个极其耐心的工具链工程师。它能快速补 parser、补 language server、补分析规则、补模型和测试，但每一层产物都要能被独立验证，也要让人类专家能接着用。

这才是人机协作里比较踏实的一种形态。

高危漏洞为什么需要两套视角互相咬住

这次公开的高危漏洞涉及 Falcon 签名。按照 Trail of Bits 的描述，恶意 prover 可以借此伪造签名并盗取资金。即使暂时不展开具体攻击路径，这个结果也说明了一件重要的事。

密码学、虚拟机和资产结算交汇的地方，最怕单点信任。

如果只做静态规则扫描，能抓到大量局部模式，却可能看不懂某条指令序列在完整执行过程里如何组合成攻击。反过来，如果只靠形式化模型证明某些规则成立，也可能因为模型范围不完整，错过真实实现中绕开的路径。

所以工具链不应该是一条从代码到结论的单行流水线，而应当形成互相校验的网。

可以把它理解为四种问题互相传递。LSP 和反编译器帮助人和 Agent 建立正确的代码地图。静态分析把怀疑扩展成全局搜索。形式化模型检查关键语义是否自洽。单元测试、回归测试和真实 exploit 验证，再负责检验工具对现实代码的判断没有飘在空中。

其中任何一层都可能出错。

但它们出错的方式不一样，这件事很重要。一个 parser 的解析错误、一个静态规则的误报、一个形式化模型遗漏的状态、一个测试恰好没走到的分支，通常不会以完全相同的方式遮住同一个漏洞。让不同方法彼此挑错，比堆更多同类型的 Agent 更可靠。

这和 Java 服务里的测试分层是同一个道理。只跑 unit test 不够，只做接口联调也不够。你需要把关键不变量落到不同层次，领域规则有单测，跨服务契约有 contract test，主链路有 E2E，线上还有可观察的指标和审计日志。

工具多，不自动带来可信度。

独立的证据路径，才会。

400 多处缺陷不是战果表，它是一份架构诊断

「发现 400 多处类型验证缺陷」很容易被当成一个夸张数字。可从工程视角看，它更像一张架构 CT 图。

如果同一类问题在数百个位置出现，通常有两种可能。要么规则在语言、编译器或 VM 的某个边界没有被统一表达，要么团队缺少一个能持续执行的验证机制，于是每个模块都在各自写一份差不多的检查。

前一种情况该回到抽象层。比如类型系统的约束是否能在更早的编译阶段表达，是否能让不合法的程序根本无法生成。后一种情况则该回到工程治理层，把静态规则变成 CI 的强制门槛，而不是把问题清单分给开发者后就结束。

这点对 Agent 写代码尤其关键。

Agent 很适合在仓库中复刻已有模式。一个边界检查缺失的模式如果已经散落在几十个文件里，它也很可能以更快速度把这个缺口扩散到新代码中。代码生成规模上来后，人工 Review 不会跟着等比例增长，问题会变得更隐蔽。

所以，团队不应该只问「Agent 这次给我写得对不对」。还要问「如果它重复写错一百次，我的系统哪一层能先拦住」。

这两个问题，难度完全不同。

前者依赖当次 Review 的运气和精力。后者逼着团队建设可复用的检查能力。

形式化验证没有魔法，它是在缩小可以撒谎的范围

一提 Lean、Coq 或形式化验证，很多工程团队会退一步，觉得那是密码学论文或航天软件才需要的东西。

这可以理解。完整形式化一个业务系统，成本很高，建模本身也可能带 bug。更现实的路线不是给所有代码套上证明，而是挑那些错一次就代价很高、同时语义又相对稳定的边界。

比如 VM 的栈操作不变量、字节码解释器的状态转换、签名校验前后的约束、金额不会凭空增加、权限不会在错误路径升级。这些东西一旦说清楚，往往就很适合转换成可检查的性质。

Trail of Bits 的 95 个机器验证证明并不代表 Miden 的一切都被证明安全。把它理解成「已经绝对安全」会犯一个危险的推断错误。证明只覆盖模型写进去了的范围，模型和真实实现的对应关系还要靠测试、Review 和持续比对保证。

但它仍然很有价值。

因为它把一部分原本依赖口头共识的规则，钉成了机器不能随意放宽的边界。未来无论人类还是 Agent 修改实现，都得面对同一条规则。

对于 Spring 和 LangGraph 团队，未必需要从 Lean 起步。你可以先把关键性质写成 property-based test，把状态机用表驱动测试覆盖，把工作流中的审批、幂等和补偿路径明确下来。等这些规则足够稳定，再考虑用 TLA+、Alloy 或更强的形式化工具检查并发和状态空间。

关键不是工具名字。

关键是把「正确」从一句模糊的话，变成一组无法轻易绕开的约束。

Agent 会让审计变便宜，也会让错误规模化

这件事有一个不太舒服的两面性。

一边是好消息。过去搭一套语言工具链，可能需要一个专家团队长期投入。现在 Agent 可以显著压缩实现、测试、文档梳理和规则迭代的时间。对于小众语言或遗留系统，这会让原本不经济的审计工作变得值得做。

另一边是坏消息。工具链的生产速度上去后，错误工具链也会生产得更快。一个 Agent 写出的 parser 如果误解了一条指令语义，后面的反编译器、静态规则和测试生成器都可能建立在同一处错误上。看起来工具齐全，实际上只是在重复验证同一个误解。

所以我不赞成把「Agent 搭了工具」直接当作可信证明。

要盯住三个更硬的信号。

工具的语义从哪里来

每个规则、模型和解析行为，都应该能追溯到语言规范、参考实现、已有测试或人工确认的假设。没有来源的自动生成规则，最多是探索线索，不能直接成为风险结论。

谁能推翻工具的结果

如果同一个 Agent 既写 parser，又写规则，又生成通过规则的测试，风险非常高。至少要用独立实现、差分测试、真实样本和人工抽检，给它制造反证机会。

结果能否进入持续流程

一次审计报告只能解决当下。真正有价值的是把已发现的 bug 类别、最小复现、关键不变量和回归规则放进 CI。否则下一个版本又会从头开始猜。

Trail of Bits 这次最值得借的不是某一个 Prompt，而是这种交付物思维。审计结束后留下的，应该是更会说话的工具、更严格的基线和更短的下一轮验证路径。

如果你要在自己的系统里试，别从全自动审计开始

很多团队已经有 Copilot、Claude Code 或内部 Agent，下一步很自然会问，能不能让它帮忙做安全审计。

可以，但我会建议从一块狭窄且可验证的区域开始。

先选一个边界清楚的模块。例如 JWT 校验封装、文件上传链路、Webhook 签名验证、订单状态转换，或者 LangGraph 里会调用外部工具的节点。不要选整个微服务，更不要把生产凭据直接接给第一个实验。

再让 Agent 产出三类东西。第一类是可读性资产，例如调用图、数据流说明、关键入口清单。第二类是可执行检查，例如 Semgrep、CodeQL 规则、架构测试或 property-based test。第三类是反例资产，例如最小复现、恶意输入样本和回归测试。

最后，给这些产物定所有者。规则由谁 Review，基线由谁批准，豁免谁能开，发现问题后怎么进 backlog，哪些检查必须阻断合并。没有这些，Agent 审计只是一次很热闹的代码阅读会。

这块需要注意一下，安全工具的权限要比编码 Agent 更小。读代码、跑本地测试、在隔离环境构造样本，已经能完成很多工作。让它默认拥有生产数据库、云账号、部署密钥或联网攻击权限，得到的不是更好的审计，而是新的攻击面。

安全能力不能用口号外包。

它得被做成一套边界清楚、可回归、能被人质疑的工程系统。

结尾不是 Agent 替代专家，而是专家终于有了更好的杠杆

Trail of Bits 这个案例最让我在意的，不是 Agent 六个月写出了多少代码，而是审计团队没有把速度误认成可靠性。

他们让 Agent 做了它擅长的重活，补工具、枚举模式、构建模型、反复验证。与此同时，最终能支撑安全结论的不是 Agent 的自信语气，而是可复现的缺陷、可运行的分析器、可机器检验的证明，以及不同证据路径之间的互相约束。

对开发者而言，这比「AI 会不会取代安全工程师」更现实。

未来安全工程师也许会少花很多时间在机械浏览上，但会更花时间定义不变量、审视模型假设、设计独立验证路径，以及决定哪些系统边界永远不能交给自动化自证。

Agent 能把造仪器的速度提起来。

而审计的底线，始终是仪器能不能经得起反证。

资料与边界

本文基于 Trail of Bits 关于 Miden zkVM 审计的公开复盘整理。六个月工具链建设、Falcon 签名相关高危风险、400 多处类型验证缺陷、95 个机器验证证明，以及两个单元测试未覆盖 bug 等事实，均来自该复盘的摘要信息。未公开的攻击细节、工具实现范围和审计覆盖边界不在本文推断范围内，因此不应把本文视为对 Miden 整体安全性的结论。

来源 https://aihot.news/items/cmu6w30lt0dnhrowkh7qwiped