Google DeepMind 用 AI 对 Signal 协议关键部分完成数学验证

谷歌 DeepMind 研究人员使用 代理式 AI 从数学上证明，或称“形式验证”，了 Signal 协议 的若干关键密码学保证——这是广泛使用的密码学和 AI 自身的一个里程碑式发展。

这项工作历时仅四周，作为一项概念验证项目，具有两方面的重要意义。它进一步独立验证了保护全球大量通信的平台（如 Signal 应用、谷歌消息和 WhatsApp）所使用的密码学。同时，它展示了 Google DeepMind 使用名为 AlphaProof Code 的新 AI 框架进行形式验证的能力。

更广泛地说，AI辅助的形式验证正迎来一个高潮，但尚不清楚它将如何适用于广泛使用，以及它在大规模代码安全方面将有多有效。形式验证的支持者长期以来一直称其为软件安全领域的一种类似圣杯的东西，因为它使用数学来检查和验证软件是否按预期运行——换句话说，它是否没有关键漏洞。

在 AI 时代之前，人们描述他们想要证明的软件特性、将这些摘要转换为公式，然后开发证明，这个过程极其耗时。代理式 AI 可以显著缩短后一个项目的耗时，从而实现像 DeepMind 的 Signal 评估这样的分析。但即使这项分析在范围上也有局限性——例如，它没有对整个 Signal 移动应用进行形式验证——DeepMind 研究人员强调，他们的发现只是更大过程中的一个里程碑。

"我们对这一结果非常兴奋，但在我们能够将其扩展到全球所有软件之前，还有很长的路要走，我们希望做到这一点，" DeepMind 研究员 Swarat Chaudhuri 告诉 WIRED。

DeepMind 的分析在其分析的 Signal 协议部分没有发现任何新的漏洞，但当研究人员使用 AlphaProof Code 对包含已知且已长期修复的漏洞的 Signal 更旧版本进行分析时，它正确地识别了这些漏洞，并表明该协议不能进行形式验证。研究人员正在发布他们为 Signal 协议分析开发的规范和证明，以帮助其他形式验证工作。