AlphaProof 代码

Google DeepMind 研究人员如何构建一个新的代理框架来正式验证 Signal 加密协议的代码——长期以来被认为是一项重大安全挑战。今天，我们将分享一个长期被认为是一项重大安全挑战的软件安全里程碑：Google DeepMind 研究人员指导 AI 代理以数学方式证明 Signal 协议底层实际代码的关键安全属性，该技术保护 Signal 和 Google Messages 等应用程序中的数十亿次私人对话。这一突破性的发现是使用 AlphaProof Code 实现的，这是一种新颖的代理框架，用于以前所未有的深度进行形式验证，将人类专业知识与人工智能代理相结合。形式验证——用数学方法证明代码正确运行且没有缺陷——是安全保证的最高标准；然而，这是很困难的，而且往往是劳动密集型的。我们的工作标志着人工智能首次被用于正式验证这种深度的广泛部署的加密协议。这也是第一次通过任何方法（无论是否有人工智能）对此类广泛部署的协议的实施进行正式验证。我们如何验证 Signal AlphaProof 代码是一个多 LLM 代理框架，它以研究团队的方式分割形式验证的工作：人类专家与 AI 一起决定要证明什么，然后由一组 AI 代理来完成。首先，我们的研究人员与多种模型合作，将 Signal 的安全目标转化为正式的数学规范，并由人类专家审查每一个模型。从那里，由 Gemini Carbon 支持的代理进行了证明，生成了超过 600 万行 Lean，这是一种从数学上证明代码准确性的计算机语言。接下来，代理审核了证据并突出显示了需要人工再次查看的区域 - 只需代码库的百分之一，节省了大量时间。由于精益会自动检查其余部分，因此我们的专家可以将审查重点放在人类判断最重要的地方。加密协议支撑着从网上银行到网页浏览的几乎所有数字通信，一个缺陷可能会同时暴露数百万人的安全。这就是为什么专家们花了几十年时间来正式分析它们。但大多数协议验证都停留在设计层面。我们的代理更进一步，证明编译的代码满足关键的安全属性——例如在设备暂时受到损害之前和之后保持消息受到保护——直到设备上运行的确切代码。由于现实世界中的漏洞通常隐藏在设计和实现之间的差距中，因此弥合这一差距会使这些证明变得更加复杂。即使在如此复杂的情况下，我们的验证过程也只花费了四个星期——这项任务历来需要专家团队花费数年时间——证明 Signal 的核心加密代码可以提供我们专家指定的安全保护。为了确认 AlphaProof 代码可以区分正确的代码和有错误的代码，我们将两个真实的、之前已修复的错误重新引入到 Signal 代码的独立版本中。在这两种情况下，系统都会生成经过机器检查的证据，证明有缺陷的版本不安全。虽然之前的正式验证工作必然集中在较小的范围上，但这种新方法可以实现显着的扩展。传统上，验证生产代码是否与其密码设计严格匹配需要大量的手动工作，这使得使用人工智能代理自动将实时代码转换为有效的精益定理成为一项重大突破。随着人工智能驱动的安全威胁的增长，通过自动定理证明对核心信号协议进行严格验证让我们更有信心我们的代码能够提供隐私保证。安全的未来解决这一长期存在的挑战表明人工智能如何为企业、政府和关键基础设施带来精英安全保证，帮助防御代理驱动的网络威胁。验证 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 对我们的方法提供的反馈。我们也