谷歌 DeepMind 的 AlphaProof Code 完成对 Signal 加密协议的形式化验证

谷歌 DeepMind 表示，其在软件安全领域取得了一项长期被视为重大挑战的里程碑：其研究人员引导 AI 智能体在数学层面证明了 Signal 协议底层实际代码的关键安全属性。Signal 协议是对消息进行端到端加密、使只有发送者和预期接收者能够阅读内容的技术，保护着 Signal 和 Google Messages 等应用中数十亿条私密对话。该公告由 Pushmeet Kohli 和 Swarat Chaudhuri 发布于 谷歌 DeepMind 博客。

这一成果由 AlphaProof Code 实现——这是一个前所未有的深度形式化验证的新型智能体框架，将人类专业知识与 AI 智能体相结合。形式化验证（即以数学方式证明代码无误地正确运行）是安全保障的最高标准，但其难度高且往往耗费大量人力。传统测试只能对程序行为进行抽样；而形式化证明可排除所有可能执行路径中的缺陷——这种级别的保障成本极高，因此很少应用于广泛部署的软件。

据该公司介绍，这项工作标志着 AI 首次在这一深度上对广泛部署的加密协议进行形式化验证，也是此类广泛部署协议的实现首次以任何方法（无论是否借助 AI）获得形式化验证。

谷歌 DeepMind 如何验证 Signal

AlphaProof Code 是一个多 LLM 智能体框架，它像研究团队那样划分形式化验证工作：由人类专家与 AI 共同决定需要证明的内容，再由一组 AI 智能体完成证明。

首先，谷歌 DeepMind 的研究人员与多种模型协作，将 Signal 的安全目标转化为正式的数学规范，并由人类专家逐一审查。随后，由 Gemini Carbon 驱动的智能体完成证明，生成了超过六百万行 Lean 代码——Lean 是一种以数学方式证明代码正确性的计算机语言。

接着，智能体对证明进行审计，并标出需要人类再次审视的部分——仅占代码库的百分之一，该公司称这大幅节省了时间。由于其余部分由 Lean 自动检查，专家得以将审查精力集中于最需要人类判断的环节。

将安全证明落实到运行代码层面

从网上银行到网页浏览，加密协议支撑着几乎所有的数字通信，而单一缺陷就可能使数百万人同时暴露于风险之中。这正是专家们数十年来一直对其开展形式化分析的原因，但大多数协议验证止步于设计层面。

谷歌 DeepMind 的智能体走得更远，证明了编译后的代码满足关键安全属性——例如在设备被临时入侵前后消息仍受到保护，即密码学家所称的前向保密性与受损后安全性——并一直落实到设备上运行的精确代码。现实世界的漏洞往往隐藏在设计实现与设计意图之间的鸿沟中，弥合这一鸿沟使这些证明的复杂度大幅提升。

即便在如此复杂度下，整个验证过程仅耗时四周——据该公司介绍，这类任务历来需要专家团队耗费数年——从而确证 Signal 的核心加密代码能够提供研究人员所规定的安全保护。

为确认 AlphaProof Code 能够区分正确代码与有缺陷代码，团队将两个此前已修复的真实漏洞重新引入 Signal 代码的隔离版本。在这两种情况下，系统均生成了经机器检查的证明，表明存在缺陷的版本并不安全——这一检验至关重要，因为无法识别缺陷代码的验证器只会提供虚假的安全保障。

在 AlphaProof Code 中，AI 智能体协助用户编写规范，随后自主证明实现满足该规范。每一条证明都由 Lean 检查，以核实智能体的工作。

Signal 的回应

"以往的形式化验证仅覆盖代码的较小部分，而谷歌 DeepMind 的方法使验证范围得以显著扩展，" Signal 首席技术官 Ehren Kret 表示。"利用 AI 智能体将实际代码转化为有效的 Lean 定理是一项重大突破。随着 AI 驱动的安全威胁不断增长，对 Signal 协议实现进行严格验证，使我们对代码的隐私保障更加充满信心。"

安全的未来

谷歌 DeepMind 认为，攻克这一长期挑战表明，AI 能够为企业、政府和关键基础设施带来顶尖的安全保障，帮助防御由智能体驱动的网络威胁。该公司表示，验证 Signal 的核心加密技术为保护其他关键系统奠定了基础，从医疗设备固件到电网软件。

扩展这些技术仍需持续研究。与 CodeMender 等自动化防御智能体相结合，形式化验证有助于应对现代网络威胁的速度与规模，打造以数学证明其防护有效性的软件。

谷歌 DeepMind 正在将其形式化验证工件开源供社区使用，托管于 google-deepmind.github.io/code-verification。完整技术论文可从 PDF 获取。对于安全研究社区而言，这一发布提供了直接审阅经机器检查的证明与方法论的途径——而这一深度的验证能在多大程度上从 Signal 扩展到该公司提及的医疗、工业和基础设施系统，是接下来值得关注的进展。

致谢

本研究由 Swarat Chaudhuri、Andrew Ferraiuolo、Anton Kovsharov、Tej Chajed、Sam Schlesinger、Karn Seth、Jonathan Katz、Charles Sutton 和 Pushmeet Kohli 完成。

团队感谢 Eric Wieser 在代码开源方面的协助、Owen Jones 在项目管理方面的支持，以及 Martín Abadi、Christopher Henson、Katerina Hristova、Henryk Michalewski、Jonathan Protzenko 和 George Tsoukalas 的有益讨论。研究人员还感谢 Signal 的 Rolfe Schmidt、Michael Rosenberg 和 Ehren Kret 对方法论的反馈，以及 Tulsee Doshi、Four Flynn、Kate Olszewska、Alicia Huang、Andy Liu、Benoit Schillings、Raluca Ada Popa、Melvin Johnson、Koray Kavukcuoglu、Demis Hassabis 和 Sundar Pichai 对该项目的支持。