Security auditing in the age of (good enough) AI
3 hours ago
- 安全公司使用AI代理不仅进行代码审查，还构建自定义工具和形式化模型，以提升审查深度。
- 为审计Miden zkVM，代理从零构建了LSP服务器、反编译器、静态分析引擎以及VM执行器的Lean模型。
- 静态分析识别了超过400处需要类型验证的位置，以及一个允许Falcon签名伪造的高严重性漏洞。
- AI生成的Lean证明产出了95个机器校验的正确性定理，揭示了单元测试遗漏的两个细微缺陷。
- 由于AI成本改善，这些准备性的辅助项目变得经济可行，从而能够在没有客户前期承诺的情况下进行更深入的审计。