DeepMind的AI智能体用四周时间从数学上验证了Signal加密代码

谷歌DeepMind发布了AlphaProof Code，这是一个用于形式化验证的多智能体AI框架——即从数学上证明软件确实按其规格运行。它的首个重大测试对象是libsignal，即Signal协议的参考实现，该协议保护着Signal、Google Messages等应用中的消息。

证明了什么

• 人类专家与AI模型合作，为Signal的安全目标编写形式化规格，并逐一审核。
• 随后，证明智能体（DeepMind称由Gemini Carbon驱动）生成了约650万行Lean证明代码，其基础是约2.6万行可信规格以及AArch64机器码的形式化模型。
• 证明覆盖后量子PQXDH握手和Triple Ratchet，确立了前向保密、身份认证、入侵后安全和握手保密——针对的是未经修改的libsignal v0.105.4的编译后机器码，而不仅是协议设计。
• 整个项目耗时四周。作为检验，团队在隔离副本中重新引入两个早已修复的真实漏洞，系统证明这些版本不安全。

局限

密码学原语和少数库函数被视为可信契约，未加验证。研究没有覆盖完整的Signal移动应用，也未发现新漏洞。《连线》指出，这种验证在大规模应用中是否实用、成本是否可承受尚不清楚；谷歌未披露成本。Lean证明已公开发布。