AI 帮安全审计补上工具，但“证明什么”仍要人检查

Coding Agent / 安全工程 · 8.5/10 · 建议深挖

Trail of Bits 公布了审计 Miden 虚拟机的经验：团队用 AI 辅助开发专用汇编语言的开发工具、反编译器和静态分析器，再把这些工具用于审计。这些原本需要投入大量工程时间的基础设施，开始变得更容易做。

工具发现了约400处可以加强类型校验的位置，但这不等于400个可利用漏洞。团队另行报告了一项严重的约束不足问题，可能导致签名伪造；这是潜在攻击后果，不是已经发生资金盗取的报道。

形式化验证部分生成了95个经过机器检查的证明，覆盖相关二进制算术组件。人仍需检查证明的命题是否符合系统真正的要求：一份证明可以完全正确，却只证明了一个不够有用的命题。审查过程中也暴露了额外假设和栈处理等边界问题。

这项经验最值得借鉴的，是先把难以阅读、难以验证的代码变成工具能够处理的形式。它不是整个虚拟机已经被证明安全，也不是让模型读一遍代码就交付审计；公开的三套工具，比“AI 找到了多少漏洞”的总数更有参考价值。