Signal加密通过AI编写的650万行数学证明

Signal 的加密代码如今拥有一项几乎没有多少广泛使用的软件能够声称的成果：一份数学证明，证明它确实做到了自己承诺的事。一支 AI 智能体团队对运行 Signal 协议的 libsignal 库进行了分析，证明其中的一对一聊天能够保密、确认对话另一端的身份，并在密钥被盗后再次阻止攻击者入侵。他们没有发现新的漏洞。

这件事的意义远不止于 Signal 用户。Signal 协议是全球端到端加密消息服务的标准，其变体保护着 WhatsApp、Messenger 和 Google Messages 中的聊天内容。要把真实上线运行的代码检查到这种深度，过去耗时极长，几乎没人尝试：该领域最重要的成果之一——经过验证的操作系统内核——耗费了二十人年。这次工作只用了四周。

这款工具由 Google DeepMind 开发，名为 AlphaProof Code。人类专家和 AI 模型首先把 Signal 的安全目标转化为 Lean 中的形式化陈述。Lean 是一种专为数学证明设计的编程语言，每条陈述都经过人工审核。随后，由 40 至 80 个智能体组成的团队在 Gemini Carbon 的支持下编写证明，每次在一台机器上连续运行 24 至 72 小时。最终成果约有 650 万行 Lean 代码。

没人需要相信这数百万行代码。Lean 的内核会检查每一步，并丢弃任何不成立的证明，因此证明由哪个模型编写、过程中出错多少次，都无关紧要。人们真正需要信任的内容要少得多：约 2.6 万行规格说明，以及一个描述 ARM 处理器如何运行代码的模型。

这些证明涵盖了 Signal 中保护对话的关键部分：用于建立聊天会话的 PQXDH 握手协议，以及为每条消息更换密钥的 Triple Ratchet，其中还包括旨在抵御未来量子计算机的后量子层。实际而言，这意味着即便有人窃取了手机当前使用的密钥，也无法解锁更早的消息；而双方交换新密钥后，窃贼也会再次失去访问权限。

为了证明这套系统能够区分好代码和坏代码，研究人员重新引入了 libsignal 中两个早已修复的旧漏洞。其中一个会让该库保留一份本应丢弃的密钥副本。两种情况下，AlphaProof Code 都生成了经过机器检查的证明，证实存在漏洞的版本并不安全。

这项成果也有明确的局限。证明只涵盖一对一会话，DeepMind 将群组消息列为未来工作。它适用于 libsignal 0.105.4 版本：该版本使用标准 Rust 编译器，针对 ARM Linux 编译，并在一个小型测试程序中运行；它并不适用于 iPhone、Android 或桌面版 Signal 的完整应用。研究假定底层密码学构件是安全的，并未对其进行证明。经人工批准的规格说明一旦有误，就会削弱这项保证；而 WhatsApp 等其他应用运行的是各自的协议版本，因此这一结果不会自动适用于它们。Google 也拒绝向 Wired 透露这项分析的成本，或是否打算将其作为服务出售。

Signal 对这一成果表示欢迎。Signal 首席技术官埃伦·克雷特（Ehren Kret）在一份声明中说：“随着 AI 驱动的安全威胁不断增加，对 Signal 协议实现进行严格验证，让我们对代码所提供的隐私保障更有信心。”DeepMind 研究科学家斯瓦拉特·乔杜里（Swarat Chaudhuri）则更为谨慎。他告诉 Wired，要让这种方法扩展到“世界上的所有软件”，还“有很长的路要走”。

对 Signal 用户来说，无需安装任何东西，也不必更改设置。这份证明针对的是应用中已经存在的代码。

DeepMind 于 11 月 10 日发布了这项研究，同时公开了一篇技术论文，并在 GitHub 上以开源形式发布了规格说明和证明。该公司称 Signal 项目是朝着 4 月提出的一项形式化验证重大挑战迈出的里程碑，并表示接下来希望检查医疗设备固件和电网软件等系统。

乔杜里还谈到了机器应该承担多少工作。他告诉 Wired：“我们不希望进入这样一种氛围：由 AI 设定目标，再由 AI 生成证明。”人类仍然决定什么才算安全，AI 只负责证明这一点。

标签: 网络安全, Google DeepMind, AlphaProof Code, libsignal, Signal, 形式化验证