Google DeepMind 证明了编译后 libsignal 的关键性质。这并不是无条件的安全保证

2026 年 11 月 10 日，Google DeepMind 宣布，在其研究人员的指导下，人工智能智能体已经从数学上证明了 Signal 协议背后编译代码的关键安全性质。由 Pushmeet Kohli 和 Swarat Chaudhuri 署名的博客，把此事写成：对一个广泛使用、且未经修改的密码学实现，一直做到机器码层面的形式化证明。这里的机器码，指的是编译后二进制文件里的实际处理器指令。论文《AlphaProof Code: Verifying Signal's Security at the Machine-Code Level》写得更精确。两处不一致时，我们以论文为准。可核对的主张，并不是 Signal、WhatsApp 或 Google Messages 从此无条件安全。它是：五人团队用四周时间，借助 AlphaProof Code，让 Gemini 4 Carbon 智能体写出约 650 万行 Lean 证明，只有通过 Lean 内核检查才会被接受，覆盖的是用原版 rustc 编译到 AArch64 的未经修改的 libsignal 的关键性质。

实际证明了什么

libsignal 是 Signal 协议的参考实现。Signal 协议是保护 Signal 应用中对话的端到端加密设计。论文写明，该协议的变体还部署在 WhatsApp、Meta 的 Messenger 和 Google Messages 中。DeepMind 并没有验证这些其他代码库。它把未经修改的 libsignal v0.105.4，连同 v1.6.0 的 SPQR 组件，链接进一个小型命令行程序 libsignal-cli，再用原版 rustc 编译到 AArch64 Linux。

PQXDH 是 Signal 当前的握手，也就是双方开始会话时的第一次密钥协商，其中包含一个抗量子步骤。Triple Ratchet 是 Signal 在消息发送过程中更新密钥的方法，它把较早的 Double Ratchet 与 Sparse Post-Quantum Ratchet（简称 SPQR）结合在一起。

团队在两种标准的协议安全模型中证明了这些组件的性质。在符号模型里，密码学运算被当成完美的黑箱。在计算模型里，高效攻击者的成功程度，受到底层数学问题难度的约束。论文称，这些证明在编译后的二进制上确立了前向保密、认证、失陷后安全和握手保密。前向保密的意思是，设备日后被攻破，先前的消息仍应受到保护。失陷后安全的意思是，失陷之后，一旦交换了新密钥，后续消息可以重新受到保护。在符号模型里，论文还主张，握手保密可以对未来的量子攻击者成立。

谁写了证明，以及仍须信任什么

人选定了范围，批准了每一条需信任的陈述，并审阅了修正。规格说明是在 Gemini 4 Carbon 和 Claude Opus 5.5 驱动的智能体协助下起草的，再由作者批准。证明本身完全由 Gemini 4 Carbon 驱动的智能体团队生成。作者本人没有写任何证明代码。

应当采用论文中的数字，而不是博客里较宽的"超过六百万行"。仓库里近 700 万行 Lean，含空行和注释。其中约 650 万行是证明：530 万行关于二进制，为两个安全证明所共用，计算证明约 86 万行，符号证明约 35 万行。另有 14 万行证明被重新引入的漏洞，7 万行验证内存分配器。被验证的 libsignal 代码约 560 KB，约 14 万条 AArch64 指令。

Lean 的内核检查这些证明。读者仍须信任的，是规格说明：仓库中约 18,000 行代码，含文档约 28,000 行，外加约 8,000 行 AArch64 语义。这些结果还依赖于 Lean 的内核、密码学原语的安全性，以及针对一些在二进制边界上被挂钩的底层密码学例程的合约，也就是被假定的行为。在计算证明中，假设大多是标准的，另外还有两条联合安全假设，因为同一把 Curve25519 密钥既用于 X25519 密钥协商，也用于 XEdDSA 签名。符号证明假定密码学是完美的。Rust 编译器本身不被信任：如果编译器缺陷，或 Rust 源码中的缺陷，破坏了已被形式化的性质，证明就会失败。博客称智能体标出了需要人类再看一眼的地方，"不过是代码库的百分之一"。这一数字未出现在论文里，我们不把它当作已证实的事实。

被重新放回去的漏洞

为检验规格说明能否抓住真实错误，作者把 Cheval、Jacomme 和 Richards 发现、且后来已修复的两个 libsignal 漏洞重新引入，方法是把上游修复提交反向应用到 v0.105.4 并重新编译。small-subgroup 漏洞是：PQXDH 的响应方没有检查发起方的 X25519 基点密钥是否无挠且在合法范围内，于是一次带有被篡改基点密钥的重放握手，就可能创建出共享密钥相同的第二个会话。weak-state 漏洞是：一条在新会话上解密失败的预密钥消息，会被拿到旧会话上试解密，一旦成功，新会话尚未确认的状态（其中含有签名预密钥的一份秘密副本）仍会被存下来。对这两个漏洞，Lean 证明都表明，符号安全定理在注入漏洞后的二进制上不成立。论文还记录了 Alwen、Coretti 和 Dodis 对 Double Ratchet 的一篇计算分析中的 15 处缺口或错误，以及 Cheval、Jacomme 和 Richards 已刊出的 ProVerif 查询中的错误，还有 Bhargavan 及其同事在 PQXDH 分析中的一处读法。

定理没有覆盖什么

汇编层面的符号定理，覆盖的情景比模型更窄。双方一开始就把对方的身份密钥固定好了，因此 libsignal 的首次使用即信任路径，也就是第一次见到联系人身份密钥就接受它的常见路径，并没有被跑到。测试程序给两个诚实的参与方，每个会话文件只安排一个会话。一次性 Kyber 预密钥，也就是预密钥包里可能出现的一次性抗量子密钥，不在覆盖范围内。侧信道，以及内存中的其他秘密，也不在范围内。结果针对的是这次构建的 libsignal-cli，而不是 Signal 自己的应用程序。工作也不覆盖群组消息、sealed sender，或服务器侧协议。

计算定理是经典的，因此不对量子对手给出保证。与 Cheval 等人一样，棘轮定理允许攻击者选择 SPQR 密钥，因而表明的是 Triple Ratchet 不弱于 Double Ratchet，而不是 SPQR 旨在增加的抗量子恢复能力。Signal 首席技术官 Ehren Kret 在博客中被引用说，这项工作带来"对我们代码的隐私保证更大的信心"。论文感谢 Signal 的 Rolfe Schmidt、Michael Rosenberg 和 Ehren Kret 对规格说明提供了反馈。对规格说明的反馈，并不是对证明的独立审计。

更公允的读法

更公允的读法，要从成本说起。论文回顾，seL4 微内核花了 20 人年才完成验证，CompCert C 编译器花了 6 人年，而且那些系统在编写时就考虑了验证。在这里，五个人用四周时间指导智能体，为一份广泛使用的密码学库生成了可机器检查的证明，并表明在把已知漏洞放回去之后，符号定理不再成立。

诚实的界限就在这项工作旁边，而不是藏在它下面。这些证明只约束被写进规格的那些性质，而且针对的是这个带测试程序的构建，以及这些假设。它们仍然信任 Lean 的内核、标准的密码学假设，以及一些被挂钩例程的合约。它们并没有把 Signal，或复用其协议变体的那些应用，变成无条件安全的软件。

谁该在意，接下来看什么

任何交付或依赖 libsignal 的人应当关心，那些会看到"Signal 已被证明安全"这类标题的读者也应当关心。产物已开放在 https://google-deepmind.github.io/code-verification。论文写明，作者希望用同一套流程，在新的 libsignal 版本发布前完成验证。未来六个月里，真正的检验是：独立读者是否审计那 18,000 行需信任的规格说明，并认为其强度与宣称相符；后续工作是否证明 SPQR 旨在提供的抗量子恢复能力，而不是继续让攻击者自由选择那些密钥；以及这套方法是否从一次针对 libsignal-cli 的行动，推进到用户实际使用的应用和功能，包括群组消息。

收束

一个小团队在一个月内，就他们选定要证明的那些性质，得到了关于编译后 libsignal 的、可机器检查的证明。这并不是一张证书，证明手机上的那些应用已经无条件安全，或证明棘轮中抗量子的那一部分完成了它被设计去完成的恢复。这些主张仍然开放，而且现在可以对照作者已经公布的产物来检查。