Google DeepMind 用 AI 数学证明 Signal 代码安全性

Google DeepMind 宣布用 AI 智能体对 Signal 的真实运行代码完成数学级安全证明，生成约 650 万行 Lean 证明代码，验证对象直达处理器实际执行的指令级别。该团队表示此前从未有人对任何广泛使用的协议做到这一点。 技术上，团队使用 40 到 80 个 Gemini Carbon 智能体撰写 Lean 证明，Lean 证明检查器会拒绝任何错误步骤，因此无需信任 AI 本身。人类负责设定安全目标并审查智能体标记的约 1% 内容。由于 Rust 编译器也不在信任范围内，编译器引入的错误同样会被证明捕捉，从而填补设计与代码之间的缝隙。 整个验证耗时 4 周，而过去专家团队通常需要数年。为排除系统只会通过任何代码的可能，研究者将 2 个已修复的旧 Signal 漏洞重新植入副本，两次都得到机器检查的证明指出代码不安全。随着成本大幅下降，这类机器验证证明有望成为固件、电网软件等关键代码的常规检查手段。