AI审计前先造了半年工具,然后挖出能掏空账户的漏洞

一家安全公司接到审计合同，没有马上扑到代码上。

审计还没开始，他们先让智能体花了六个月，从零造了四件工具。

工具造完，人才开始看代码。最后挖出一个能让账户资金被整个搬走的高危问题。

这是 Trail of Bits 在本月发的一篇复盘里讲的事。我读完最想抄的部分，在前面那半年。

那段等着的时间，他们没拿来等

事情是这样开头的。

2025 年底，一个做零知识虚拟机的团队找上门，想在上线前把其中一块审一遍。范围里的东西叫 Miden 核心库，里面是一小撮密码学原语，用一门他们自己写的汇编语言 MASM 写的。

接活的公司挺兴奋，这种高安全要求的项目正对胃口。麻烦也跟着来了。

这台虚拟机是栈式架构。每条指令读什么、写什么，全在栈上，而且是隐式的。代码读起来，你得自己在脑子里维护一个栈。

更要命的是，这门语言几乎没有配套工具。编辑器支持没有，语言服务器没有，代码检查工具也没有。

对方的代码还没写完，所以他们知道手上有一段准备期，半年左右。于是问了自己一个问题：这半年的时间和 token 花在什么上，才能让这次审查把问题挖得最干净？

他们给出的答案是：先造工具，再看代码。

四件工具，四层抽象

先是语言服务器。这个几天就有了能用的版本：语法高亮、跳转定义、查引用、鼠标停上去能看到说明。后来又加了指令文档和每条指令的栈效应。

接着是反编译器。把底层代码还原成人看得懂的样子，解决的是看不见。

这活比想起来难。核心库里大多数过程压根没声明签名，输入输出有几个得靠上下文猜；调用约定也不统一，一次调用到底吃掉几个、吐出几个，静态根本算不出来。一处算不出来，就会沿着调用链一路往上传递。

然后是静态分析引擎。在还原出来的中间表示上做类型推导和数据流追踪，解决的是看不全。

第四件走的不是同一条路。他们用 Lean 这个定理证明器，给虚拟机的执行器建了个形式化模型。前面几件说的是“这里可能有问题”，这一件说的是“在这组前提下，它一定成立或者一定不成立”。

四件叠在一起，做的事其实是同一件： 把人的注意力从机械劳动里抢出来，留给判断。

挖出来的东西

结果挺实在。

静态分析标出了四百多个类型验证可以改进的位置，而且这些位置都能从库的公开接口走到。

这里我把话说准一点。原文用的词是可以改进，指的是校验还能收紧，不是已经出事了。差一个字意思差很远，读者一对照原文就能看出来。

真正的高危问题是另一条。有个过程做取模运算，商和余数由证明方提供。商被检查过，余数没有，直接就传给了下一条指令。把这两个值凑一凑，可以让它算出来的余数不是真正的余数，于是证明方就能伪造签名，把账户里的钱转走。

Lean 那边的产出是九十五个机器验证过的正确性证明，覆盖了核心库里一大块基础组件。顺带还抓出两个单元测试没逮住的细微毛病。

一句话，把算账的方式改了

文章最后那段才是我觉得最值得存的。

作者说，这些工具、还有那些 Lean 库和证明，搁在一两年前都属于副项目，团队根本匀不出人力和资源去做。因为这类探索性的东西，结果和回报都很难预测，你也没法提前拿它去跟客户谈价钱。

过去一年情况变了。智能体已经好到能在很轻的监督下把这类非核心项目扛下来，这把“哪些项目值得做”这笔账整个改写了。

现在，一个失败的副项目只花掉一些 token。

这句话我读了两遍。

过去我们判断一件事做不做，算的是投入产出比。探索性的事回报不确定，投入又是实打实的人天，所以这类事长期排在队尾，谁都知道该做，谁都不做。

当失败的代价塌到只剩 token，投入这一头轻了一大截，哪些事值得做，跟着就换了名单。

还有个尾巴值得说：那套静态分析引擎，对方团队留下了。以后核心库再更新，它还接着用。

产品经理、项目经理能抄的三条

一、手上有等待期的时候，别只当等待期用。他们那半年是因为对方没写完才有的，多数团队会把它排成“先等着”。他们拿去造工具了。等项目排期里出现空档，先问一句这段能提前备什么，比干等划算。

二、把耐力活派给智能体，把判断活留给人。造语言服务器、写反编译器这类事，规则清楚、重复度高、需要穷举，恰恰是人不愿意干也干不长的。找漏洞靠的是判断力，这部分他们没交出去。

三、把那些想做又迟迟没动的事重新过一遍。以前算不过来的账，现在算得过来了。先挑一件失败也不心疼的，扔给智能体跑一轮看看。

这半年值得抄的三句 ① 代码还没写完的那段空档，是造工具最好的时候。 ② 耐力活交给智能体，判断活留给自己。 ③ 探索性的活失败一次只花点 token，这笔账该重算了。一句话记住：先问手上的工具够不够，再问活干不干得完。

带项目的人大概都有过这种体会：活干不完，常常是人手够、家伙不趁手。

过去造家伙太贵，只能凑合。现在这笔成本降下来了，凑合的理由也就少了一个。

你手上有那种一直想做、但排不上人手的活吗？如果失败只花一点 token，你会先拿哪件开刀？下一期希望我讲什么？欢迎评论区互动哟~