谷歌DeepMind用AI形式化验证Signal协议，未发现新漏洞

据《连线》(Wired)报道，谷歌DeepMind的研究人员使用名为AlphaProof Code的智能体式AI框架，以数学方式证明了Signal协议的若干关键密码学保证。这项在四周内完成的概念验证工作属于形式化验证：它用数学来检验软件是否按预期运行，而不是只测试一部分案例。

Signal协议是Signal应用背后的加密方案，正如《连线》指出，它同样保护Google Messages和WhatsApp中的通信。因此，这项分析被视为对一套保护海量消息的密码学的又一次独立验证。《连线》称其对密码学和AI本身都是一个里程碑，同时强调其范围有限。

DeepMind究竟证明了什么？

团队证明的是协议的“若干”关键保证，而不是全部。《连线》明确指出，这次分析并未对整个Signal移动应用进行形式化验证，研究人员也把结果描述为更大进程中的一个节点。DeepMind研究科学家斯瓦拉特·乔杜里(Swarat Chaudhuri)对《连线》说：“我们对这一结果非常兴奋，但要把它推广到世界上所有软件还有很长的路要走，而我们想做到这一点。”

同一篇报道称，这次分析在所检查的协议部分中没有发现新漏洞。研究人员还把AlphaProof Code用于含有已知且早已修复漏洞的旧版Signal：工具正确识别了这些漏洞，并表明这些版本无法通过形式化验证。这一测试很重要，因为它说明该方法在存在缺陷时会失败，而不只是在没有缺陷时成功。

• 工具：AlphaProof Code，谷歌DeepMind的新型智能体式AI框架。
• 耗时：四周，属于概念验证项目。
• 结果：证明了关键密码学保证；在所分析的部分中未发现新漏洞。
• 旧版本：检测出已知且早已修复的缺陷，并表明协议无法通过验证。
• 公开：规范与证明将发布，以帮助其他形式化验证工作。
• 成本：未披露；作为研究项目免费完成。

AI与人类如何分工？

在AI时代之前，人们需要描述想要证明的性质，把这些描述转成公式，再构造证明。《连线》解释说，智能体式AI可以大幅缩短最后一步的时间，这使得四周内完成Signal评估成为可能。DeepMind的研究人员补充说，他们起步时占了一些先机，因为Signal基金会此前已对代码中较小的部分做过形式化验证。

Signal首席技术官埃伦·克雷特(Ehren Kret)在《连线》引述的声明中说：“此前的形式化验证只集中在代码的较小部分，而谷歌DeepMind的方法能够显著扩展范围。”他还说，随着由AI驱动的安全威胁增加，对实现进行严格验证，让Signal对其代码的隐私保证更有信心。

DeepMind认为自己的主要进展是一种“人机协作流程”：智能体几乎在每个阶段都有所贡献并自我纠错，而人类在关键节点进行审查。乔杜里说：“我们不想要一个由AI生成目标、又由AI生成证明的世界。”形式化证明只保证已写下的性质，因此人类对规范的审查仍然至关重要。

围绕Signal的另一项并行工作

DeepMind的工作并不是证明Signal密码学的唯一尝试。Beneficial AI Foundation与Signal的罗尔夫·施密特(Rolfe Schmidt)以及Lean FRO合作，发起了公开项目“Signal Shot”，计划用证明助手Lean验证该协议及其Rust实现。该项目打算用Aeneas工具把Signal的Rust代码翻译成Lean，并列出待验证的组件，包括后量子密钥交换PQXDH、Double Ratchet以及SPQR/Triple Ratchet。《连线》并未把这一倡议与DeepMind的工作联系起来，两者是各自独立的努力。

还有哪些不确定之处？

《连线》指出，悬而未决的问题是：由AI自动化的形式化验证能否以可行的成本扩大规模。谷歌拒绝透露Signal分析的成本，也拒绝说明是否计划推出形式化验证的商业产品或服务。谷歌云首席科学家、DeepMind研究副总裁普什米特·科利(Pushmeet Kohli)设想，担心程序错误的银行和其他公司将来可以说自己能证明软件的某些性质。这是一种设想，而不是已宣布的产品。

这对企业意味着什么？

对选择通讯工具或基于Signal协议开发产品的企业来说，这一结果是对协议设计的一个令人安心的信号，而不是对所有使用该协议的应用的认证：完整的Signal应用并未被验证，产品的部署方式、服务器和配置也都不在证明范围内。公开的规范与证明为安全团队提供了可研究和复用的材料。由于成本和商业化方案都未知，企业暂时还不能指望用这种方法对自家代码做形式化验证，但现在就可以向关键软件供应商询问，哪些性质已被明确规定并得到证明。