Google DeepMind 研究人员如何构建了一个新的智能体框架，对 Signal 加密协议的代码进行了形式化验证——这长期以来被视为一项重大的安全挑战
今天，我们分享软件安全领域一个长期被视为重大挑战的里程碑：Google DeepMind 研究人员引导 AI 智能体，对 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 代码的隔离版本中。在这两种情况下，系统都生成了机器检查的证明，表明有缺陷的版本是不安全的。
“虽然之前的形式化验证侧重于代码的较小部分，但 Google DeepMind 的方法实现了显著扩展，”Signal 首席技术官 Ehren Kret 表示。“使用 AI 智能体将实时代码转化为有效的 Lean 定理是一项重大突破。随着 AI 驱动的安全威胁增长，严格验证 Signal 协议实现让我们对代码的隐私保证更有信心。”
Ehren Kret
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 对本项目的支持。