DeepMind 用 AI 智能体给 Signal 加密「验算」：4 周证完关键安全保证，没发现新漏洞

Google DeepMind 用一套叫 AlphaProof Code 的新智能体框架，给 Signal 协议的关键密码学保证做了数学证明。WIRED 在 11 月 10 日报道了这项研究：整个概念验证只花了四周，在检查的部分里没有发现新漏洞；研究团队还会公开这次用到的规范与证明。

形式化验证和常规代码审计不是一回事：审计是读代码、判断看起来对不对，形式化验证是把“系统应该怎样”写成数学命题，再由软件逐行检查证明是否成立。DeepMind 的智能体承担了其中最繁琐的一步——在人类于关键节点审核的前提下，自行提出证明并不断自我修正。研究负责人 Swarat Chaudhuri 对 WIRED 说，他们不想要一个“AI 自己出题、AI 自己答题”的世界，人的把关仍在回路里；他也坦言，离把这套方法扩展到“世界上所有软件”还很远。

这次验证的范围需要说清楚：它只覆盖 Signal 协议选定的几项密码学保证，不是整个 Signal 应用，更不等于 WhatsApp、Google Messages 这些同样用 Signal 协议的产品全无漏洞。作为对照，研究团队把 AlphaProof Code 用在含已知漏洞的旧版协议上，它正确识别了问题、并判定这些版本无法通过验证——这正是检查工具该有的表现。Signal 自身此前的形式化验证工作（包括与 Cryspen 合作的后量子棘轮）也给这次提速打了基础。Signal 首席技术官 Ehren Kret 在声明中说，DeepMind 的方法让验证范围比以往只覆盖小块代码的做法“显著扩大”。

值得注意的背景是，这不是 AI 第一次被派去啃密码学：DeepMind 的 AlphaProof 曾在 2024 年国际数学奥林匹克达到银牌水平；今年 5 月，AlphaProof Nexus 又以每个问题几百美元的成本解出了 9 个 Erdős 开放问题。区别在于，这次的证明对象是每天承载数十亿条消息的真实协议。DeepMind 免费做了这项研究，谷歌没有透露成本，也没有说明是否会把形式化验证做成商业产品。研究副总裁 Pushmeet Kohli 的说法是，如果能证明关键实现的正确性，银行这类最怕 Bug 的机构就能“睡个安稳觉”。

对中文读者来说，另一个参照是站内此前报道的两起 AI 啃硬骨头的案例：DeepMind 用 AI 智能体找出 1024 位 RSA 两处弱点，以及未公开的 Anthropic 模型 3 天证出 18 年量子猜想。前者是找漏洞，后者是证定理，这次则是给现成的加密协议做“无罪证明”——三种方向凑在一起，正好是 AI 安全研究今年的主线。

来源：WIRED（MadRobot 全文转述），原文