AI 代码审查的可信度,取决于它的反驳者 🧪

Trail of Bits 上周那篇 Auditing in the age of (good enough) AI 开头先点了一句:安全公司已经发了一大堆博客,讲自己怎么把 agent 框架对准一个代码库、找出几十个 bug —— 他们自己也发过。接着他们说,agent 代码审查只是他们在安全审查里用 AI 的一个环节。他们想讲的是审查开始之前的事:让 agent 去造定制工具和形式化模型,让审查做得更好、更深。

我们同意。这一周我们自己的审查记录,正好从另一头说明了为什么。

他们的时间到底花在了哪

这次的审查对象是 Miden VM:一个新的零知识虚拟机,有自己的汇编语言 MASM,开发工具几乎为零。为了准备,他们花了六个月,让 agent 从零做出一个 LSP 服务器、一个反编译器、一个静态分析引擎,以及虚拟机执行器的 Lean 模型。审查期间,这些分析找出了 400 多处可以加强类型校验的位置,外加一个高危问题:mod_12289 里由证明者提供的余数从来没被校验,恶意证明者可以借此伪造 Falcon 签名,掏空任何由 Falcon 密钥对控制的 Miden 账户。Lean 这条线产出了 95 个经机器检查的正确性证明,还揪出两个现有单元测试没抓到的隐蔽 bug。

比这些数字更值得看的是方法。做反编译器时,每实现一个新功能,他们就让 agent 从核心库里随机挑一批过程去反编译,再和原始 MASM 比对,发现的问题一律变成回归测试。证明那边,证明本身交给 Lean 内核检查,人只需要审定理的陈述写得对不对。两处是同一个结构:agent 负责产出,另有一个独立的东西负责判断它站不站得住。

bug 数量衡量的是「找」的那一方

「我们的 agent 找到了 N 个 bug」,说明的是候选发现如今很便宜。它没算进去的,是读这份清单的成本:每一条都是一个主张,得有人去复现、排优先级,然后修掉或者驳回。一个每三次错一次的发现器,并不等于三分之二的价值。它交给你的是一条队列,而你没法分辨错的是哪三分之一。反过来,一条写明了输入和错误输出的发现,任何人都能照着跑一遍,看它到底成不成立。

一条发现变得可信,靠的是它被找到之后经历了什么:

1. 具体的失败场景: 一个输入,加上它产生的错误输出。
2. 一次独立的反驳尝试。
3. 一个不修就会失败的测试, 靠把 bug 放回去来证明。
4. 上线后对运行中系统的探测。

这套流程抓到了什么

这周我们把一批 SEO 和路由修复,从我们的一个站点移植到另一个用同一套代码库搭起来的站点。部署前先跑了一轮自动审查:几个审查 agent 各管一个视角 —— canonical/hreflang 注册表、中间件与重定向、robots 与内容、构建与部署。每条发现都必须写明一个输入、错误的输出和修法。然后每条发现交给两个互相独立的「质疑者」agent,任务是驳倒它;如果从实际代码里复现不出来,默认判为已驳倒。

结果是 12 条成立,0 条被驳倒。最要命的一条:博客索引页改成了「某个语言自己没有文章时,回退显示另一种语言的文章」,但卡片上的链接仍然按页面自身的语言拼出来。而文章页只在它自己的语言下预渲染,动态路由参数又是关着的,于是在 15 个语言里的 13 个,博客索引页上的每一张卡片都链到 404。

其余几条也不轻。同一次改动刚在站点地图里声明为自身 canonical 的中文法律页面,标题和描述还是英文。语言切换器仍把读者送到已经删掉的文档页。站内 AI 助手的提示词还在引导用户去一个已删除的 FAQ 页面。规范化用的 HTTPS 重定向保留了非标准端口,http://host:8080/ 会跳到 https://host:8080/,而 CDN 在这个端口上根本不提供 TLS。还有一个共享的开放重定向防护函数,被挪进了跨仓库漂移检查覆盖不到的文件,两份副本已经差出一行 —— 好在行为还一致。

第二个改动小一些:给大小写写错的语言前缀加一跳重定向(比如 /zh-hant 到 /zh-Hant),并让 tRPC 的 API 路径也经过中间件。这次先走设计阶段:一个 agent 设计每项改动,另一个独立的评审 agent 专门想办法把设计打破。设计阶段的排查还在两个生产站点上挖出一个真漏洞:只要路径匹配一个没加锚点的 .png/.jpg 正则,中间件就会在任何鉴权逻辑运行之前跳过全部检查。于是 /api/trpc/edge/forum.search,x.png?batch=1 没经过 API 的默认拒绝,就把数据返回了(HTTP 207)。修法是:静态资源的跳过规则,永远不适用于需要会话的路径。

差点漏过去的

评审 agent 在设计里没找到运行时缺陷,却在拟议的测试里找到了三个。一个清单测试列了 8 个文件,实际有 9 个。多加一个测试文件,会让 lint 错误数比发布门禁的棘轮上限多出 1 个,直接把发布卡住。还有一个检查源码先后顺序的测试,它搜索的字符串在三份文件副本里有两份根本不存在,所以这个测试永远不会失败。简化后的写法和修法如下:

// 空转:要找的字符串不存在时 indexOf 返回 -1,
// 任何位置都比它「大」,这条断言永远不会失败。
const canonical = src.indexOf("<不存在的锚点>");
const hop = src.indexOf("<存在的锚点>");
assert.ok(hop > canonical);
 
// 修正:两个锚点都找到了,比较先后才有意义。
assert.notEqual(canonical, -1, "canonical anchor not found");
assert.notEqual(hop, -1, "hop anchor not found");
assert.ok(hop > canonical);

更隐蔽的一次险情发生在后面。这个改动实现之后的审查用了 4 个视角,成立 0 条。但有 3 条低严重度的发现从头到尾没被验证过:负责验证的 agent 撞上了用量上限,直接死掉了。我们没有把这三条算作「已驳倒」,而是自己逐条读了一遍,其中 2 条是真的:漂移检查没覆盖一个共享的冒烟测试脚本;一个清单测试只认得导入路径的一种写法。两条都修了。「复现不出来就默认驳倒」这条规则,对一个认真试过的质疑者是对的;而一个根本没跑起来的质疑者,什么结论都没给出。

每个新测试都做了变异检验:把 bug 放回去(撤掉修复、删掉防护、把 308 改成 307、去掉解码那一步、放开一个循环),跑测试,确认它失败,再恢复原样。那次改动一共做了 9 个变异,全部被抓住。每次部署之后,我们都对生产环境跑实时检查:一个站点 44 项全过,另一个站点 29 项回归检查和 12 项网关检查也全部通过。

给团队的一张短清单

• 没有场景,就不算发现。 每条都要给出输入、错误输出和修法。
• 让另一个 agent 来反驳, 并且从真实代码里复现不出来就默认驳倒。
• 状态分三种:成立、驳倒、未验证。 未验证的交给人看,绝不归进驳倒那一堆。
• 每个新测试都做变异检验。 把 bug 放回去,亲眼看它失败。
• 查找落空必须报错。 测试依赖的任何 indexOf、正则或文件清单,找不到东西时要直接失败。
• 上线后用同一批场景探测生产环境。

Trail of Bits 说,如今一个失败的支线项目只花掉一些 token。发现也是一样便宜。真正贵的,是把一条没人核实过的发现当成真的,或者当成假的。所以力气该花在判断每条发现站不站得住的那套机制上。

来源: Trail of Bits