Google DeepMind 借助 AI 智能体验证 Signal 核心机器代码

Google DeepMind于 2026 年 11 月 10 日推出了 AlphaProof Code，利用 AI 智能体团队为 Signal 编译后的 libsignal 代码中指定的安全属性生成可由机器验证的 Lean 证明。五人研究团队在四周内完成了证明工作，并公开了相关规范和验证材料，供外部审查。

这项工作不再局限于 Signal 协议设计的抽象模型，而是进一步验证了其编译后的实现。研究人员将未经修改的 libsignal v0.105.4 和 SPQR v1.6.0 crate 封装在一个小型命令行工具中，随后使用标准版 rustc 构建了一个静态链接的 AArch64 Linux 可执行文件。这篇技术论文称，这是首次针对广泛部署的密码协议实现的未经修改代码，给出协议层面的安全证明。

AlphaProof Code 如何分工

五名研究人员用四周时间完成证明工作，在工作站上持续运行智能体，同时并行开展符号证明和计算证明。论文称，智能体生成了约 650 万行经机器验证的 Lean 证明代码，其基础是约 2.6 万行可信规范和 AArch64 语义。

人类研究人员选定要验证的属性，厘清歧义和安全权衡，审查规范，并保留最终批准权。由 Gemini 4 Carbon 和 Claude Opus 5.5 驱动的智能体起草并审查这些规范，审查工作还包括由不同模型系列的模型进行复核。随后，Gemini 4 Carbon 智能体团队生成了全部证明代码；作者中没有任何人编写证明代码。典型任务会在一台机器上使用 40 至 80 个智能体，持续 24 至 72 小时；协调器和团队负责人负责协调证明工作者，架构师和集成者则维护共享的证明基础。

只有在 Lean 内核完成检查，且比较器确认证明与留存的、经人类批准的规范相符（包括所有传递依赖的定义），并且仅使用 Lean 标准公理后，守门程序才会接受该证明。当证明暴露出规范问题时，智能体可以提出小幅修改；但对可信假设的任何更改，都必须获得人类批准或遵循用户设定的策略，并记录修改理由。这项控制措施针对的是已有记录的智能体生成证明风险：规范可能通过其中某个定义被间接弱化。

安全覆盖范围与历史漏洞测试

验证对象是一对一会话代码，涵盖 PQXDH 握手和 Triple Ratchet 消息传递。研究人员报告了两种相互独立的论证：一种是在理想化密码学假设下的十条符号定理；另一种是计算证明，通过密码学假设和统计项对攻击者的优势设定上界。所涵盖的属性包括前向保密（即当前状态被窃取后仍能保护此前的消息）、身份认证、后泄露安全（即泄露事件发生后能否恢复安全）以及握手机密性。此外，符号论证还涵盖了 Diffie–Hellman 日后遭破解时的握手机密性。

为检验这些规范能否发现真实漏洞，团队反向应用了两个此前已修复的 libsignal 漏洞的修复补丁，这两个漏洞称为弱状态和小子群，并重新编译了修改后的二进制文件。在这两种情况下，团队都生成了 Lean 证明，表明符号安全定理不成立。公开的验证代码库将计算证明、符号证明、共享二进制文件和 AArch64 语义材料分门别类，并说明如何重新构建和独立检查这些证明。

Signal 首席技术官 Ehren Kret 表示，这项工作“让我们对代码的隐私保障更有信心”。

局限与后续计划

这些保障远不足以证明 Signal 的完整应用程序安全。研究结果针对的是研究人员构建的 libsignal-cli 在全新进程中运行的情形；密钥生成未经验证，群组消息传递留待未来研究，侧信道和多设备状态也不在考察范围内。底层密码学原语以及选定的输出例程和库例程均由可信契约表示，因此，研究结果也取决于这些契约、获批的规范、Lean 内核、AArch64 语义以及关于密码学原语的假设。

论文指出，这两种论证都没有证明 SPQR 旨在提供的后量子安全恢复能力：计算定理涵盖的是经典攻击者，而符号棘轮定理允许攻击者选择 SPQR 密钥。计算模型还限制了攻击者的若干行为，并且当消息和会话规模足够大时会变得无效。这些边界界定了外部审查者在将机器验证的证明视为特定部署的安全保障之前必须信任的内容。

研究人员提出的后续计划包括强化定理、通过验证更多挂接例程并将密码学契约与经验证的实现相连接来缩小可信基础，以及将覆盖范围扩展到群组消息传递、密封发送者和服务器端协议。他们希望在发布前验证新版 libsignal；这仍是研究目标，而非已经宣布的部署计划。

这一成果的直接意义在于展现了分工方式：智能体负责构建证明，而可信保障仍依赖经过人工审查的规范和明确的假设。公开这些证明和检查程序，让外部审查者能够检验这一基础；与此同时，研究人员也在努力将这套工作流程应用于 libsignal 的持续开发。