DeepMind 用智能体形式化验证 Signal 加密代码

2026年11月10日 研究

推出 AlphaProof Code：深度验证复杂软件的重大突破

Pushmeet Kohli 与 Swarat Chaudhuri

阅读技术论文

Google DeepMind 研究人员如何构建一个全新的智能体框架，对 Signal 加密协议的代码进行形式化验证——这一直被视为一项重大的安全挑战

今天，我们分享软件安全领域的一项里程碑成果，这一领域长期被视为一项重大的安全挑战：Google DeepMind 研究人员引导 AI 智能体，用数学方法证明了 Signal 协议底层实际代码的关键安全属性。Signal 协议是保护 Signal 和 Google Messages 等应用中数十亿次私密对话的技术。

这一突破性发现借助 AlphaProof Code 实现，这是一个全新的智能体框架，能够以前所未有的深度进行形式化验证，将人类专业知识与 AI 智能体相结合。 形式化验证——用数学方法证明代码运行正确、没有缺陷——是最高标准的安全保障；然而，它难度大，且往往耗费大量人力。

我们的工作标志着 AI 首次被用于以如此深度对广泛部署的加密协议进行形式化验证。这也是首次通过任何方法（无论是否借助 AI）对这类广泛部署协议的实现进行形式化验证。

我们如何验证 Signal

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

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

接下来，智能体对证明进行了审计，并标出了需要人工复核的部分——仅占代码库的百分之一，大幅节省了时间。由于 Lean 会自动检查其余部分，我们的专家可以将审查重点放在最需要人类判断的地方。

密码学协议是几乎所有数字通信的基础，从网上银行到网页浏览，一个漏洞就可能同时暴露数百万人的信息。正因如此，专家们数十年来一直致力于对它们进行形式化分析。

但大多数协议验证都止步于设计层面。我们的智能体更进一步，证明了编译后的代码满足关键安全属性——例如在设备暂时被攻破前后都能保持消息受保护——并且一直验证到设备上运行的确切代码。由于现实世界的漏洞往往隐藏在设计与其实现之间的差距中，弥合这一差距会使这些证明的复杂度大幅提升。

即便复杂度如此之高，我们的验证过程也仅用了四周——而这项任务历来需要专家团队花费数年时间——这证明了 Signal 的核心密码学代码提供了我们专家所指定的安全保护。

为了确认 AlphaProof Code 能够区分正确代码和有缺陷的代码，我们在 Signal 代码的一个隔离版本中重新引入了两个真实的、此前已修复的漏洞。在这两种情况下，系统都生成了经过机器校验的证明，表明有缺陷的版本是不安全的。

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

虽然以往的形式化验证主要聚焦于代码中较小的部分，但 Google DeepMind 的方法实现了显著的扩展，”Signal 首席技术官 Ehren Kret 表示。“利用 AI 智能体将实际运行代码转化为有效的 Lean 定理是一项重大突破。随着 AI 驱动的安全威胁不断增长，对 Signal 协议实现进行严格验证，让我们对代码的隐私保障更有信心。

Signal 首席技术官

以往的形式化验证工作必然聚焦于较小的范围，而这种新方法实现了显著的扩展。传统上，要验证生产代码严格符合其密码学设计，需要大量人工投入，因此利用 AI 智能体自动将实际运行代码转化为有效的 Lean 定理是一项重大突破。随着 AI 驱动的安全威胁不断增长，通过自动定理证明对 Signal 核心协议进行严格验证，让我们更加确信我们的代码能够兑现其隐私保障。

安全的未来

攻克这一长期挑战表明，AI 能够为企业、政府和关键基础设施带来顶尖的安全保障，帮助抵御由智能体驱动的网络威胁。

验证 Signal 的核心密码学为保护其他关键系统奠定了基础，从医疗设备固件到电网软件。

推广这些技术需要持续研究。配合 CodeMender 等自动化防御智能体，形式化验证可以帮助应对现代网络威胁的速度和规模，从而打造出带有数学证明、可证实其防护有效的软件。

我们正在开源我们的形式化验证产物供社区使用。请阅读下方的技术论文。

阅读技术论文

致谢

本研究由 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 对本项目的支持。

相关文章

推出 CodeMender：一款用于代码安全的 AI agent

2025 年 10 月责任与安全了解更多