DeepMind让AI证明Signal安全

Google DeepMind 在 11 月 10 日公布 AlphaProof Code，并宣布用这套多智能体系统完成了对 Signal 核心加密代码的形式化验证。研究团队没有让 AI 再找几个漏洞、补几段测试，而是要求它证明：Signal 的实际机器代码，在给定安全模型和假设下，确实满足前向保密、身份认证和入侵后恢复等关键承诺。

这项工作的分量不在于“AI 检查了 Signal”，而在于验证对象已经从协议设计图推进到编译后的 AArch64 机器代码。DeepMind 称，这是 AI 首次以这种深度验证被广泛部署的密码协议实现，也是一次把大模型、密码学和定理证明器真正接到生产代码上的实验。(deepmind.google)

形式化验证，不是更高级的单元测试

形式化验证是一种把软件需求写成数学命题，再用机器可检查的证明确认程序满足这些命题的方法。

普通测试回答的是“我们尝试的这些输入有没有出错”，模糊测试回答的是“随机、畸形或边界输入能不能撞出漏洞”，而形式化验证要回答的是“在模型覆盖的全部情况下，某类错误是否被数学上排除”。

区别可以类比为检查一座桥。测试是在桥上开过不同重量的车辆，静态分析是检查钢筋和焊点是否存在常见缺陷；形式化验证则是建立桥梁、载荷和材料的数学模型，再证明在设定范围内结构不会失效。

| 方法 | 核心问题 | 能否证明不存在某类漏洞 | 主要局限 | |---|---|---:|---| | 单元测试 | 给定输入是否得到预期结果 | 否 | 输入覆盖有限 | | 模糊测试 | 异常输入能否触发崩溃或错误 | 否 | 找到漏洞有效，没找到不代表安全 | | 静态分析 | 代码是否匹配已知危险模式 | 通常不能 | 误报、漏报依赖规则和分析深度 | | 传统形式化验证 | 实现是否满足数学规格 | 可以 | 专家成本高、周期往往以年计算 | | AlphaProof Code | AI能否生成机器可检查的软件证明 | 可以，但限于规格与模型范围 | 算力、规格质量和可信边界仍是瓶颈 |

因此，形式化验证的价值不是把漏洞扫描准确率从 90% 提高到 95%，而是改变安全结论的性质。测试只能说“暂时没有发现问题”，证明则可以说“任何违反已证明性质的执行路径，都无法在当前模型中成立”。

AI究竟证明了什么

AlphaProof Code 是一个由人类定义目标、多个大模型智能体生成证明、Lean 内核负责最终验收的形式化验证框架。

整个流程大致分为三层：首先，人类专家与模型共同把 Signal 的安全目标翻译成 Lean 规格；其次，AI 智能体分析编译后的程序并搜索证明；最后，Lean 内核逐步检查证明是否合法。AI 可以犯错、编造推理甚至走进死胡同，但错误证明无法通过 Lean 的内核检查。

这点很关键：DeepMind 并没有要求外界“相信 Gemini 的推理”，而是要求 Gemini 提交一份可以被独立验证的证明对象。它更像一个工作速度极快但不完全可信的证明工程师，Lean 则是拒绝通融的数学审计员。

研究覆盖的是 libsignal 的正式 Rust 实现经过编译后得到的 AArch64 机器代码。官方开源仓库显示，验证材料包含 libsignal v0.105.4、spqr v1.6.0、AArch64 指令语义、符号安全模型和计算安全模型；研究团队还提供了从论文结论映射到具体 Lean 定理的索引。(github.com)

DeepMind 披露的核心数字包括：

• 整个验证项目耗时约 4 周，而同等规模的人工工作通常需要数年；
• AI 生成了约 650 万行 Lean 证明代码；
• 证明建立在约 2.6 万行可信规格与 AArch64 语义之上；
• 自动审计后，需要人类重点复查的部分约占证明工程的 1%；
• 研究覆盖两套相互独立的证明路线：符号模型与计算模型。(deepmind.google)

符号模型把密码算法视为理想化的黑箱，例如没有密钥就无法解密；计算模型则进一步用概率和计算复杂度描述攻击者，讨论攻击成功概率是否可以忽略。两套模型同时给出结论，比只在单一抽象层上验证更有说服力，也能减少“模型本身过度理想化”带来的风险。

Signal最关键的安全承诺被覆盖

Signal 协议是一套面向异步通信的端到端加密协议族，用于在服务器不可信、设备可能短暂失陷的情况下保护消息内容和会话身份。

此次证明重点覆盖了 PQXDH 握手和 Triple Ratchet 等机制，并验证了四类关键性质：

1. 前向保密：即使当前密钥泄露，攻击者也不能反推出过去的消息。
2. 身份认证：攻击者不能轻易冒充通信对象建立合法会话。
3. 入侵后安全性：设备短暂失陷后，只要攻击者失去控制，会话能够通过密钥更新重新恢复安全。
4. 握手机密性：建立会话时产生的关键秘密不会暴露给不具备相应密钥的攻击者。

这几项性质正是现代安全通信与传统“拿一个长期密钥加密所有内容”的根本区别。传统方案一旦长期密钥泄露，历史消息和未来消息可能一起失守；Signal 的棘轮机制会持续更新密钥，把一次设备入侵造成的损失限制在较小时间窗口内。

更重要的是，研究没有停留在“协议论文中的算法是安全的”。团队把协议安全目标连接到了实际编译产物，尝试填上密码工程里最危险的一道缝：设计正确，不代表实现正确；源代码正确，也不必然代表编译后的程序行为完全符合预期。

AI还识别了两个真实旧漏洞

反向验证是指把已知错误重新放入系统，检查证明工具能否拒绝错误实现。

为了确认 AlphaProof Code 不是只会为正确版本寻找一条看起来合理的证明，研究人员把两个已经修复的真实漏洞重新引入隔离版本。系统没有强行“证明成功”，而是生成了可由机器检查的结论，证明这些错误版本不满足目标安全性质。(deepmind.google)

这一实验比单纯宣布“正确版本验证通过”更重要，因为大模型在数学任务上的典型风险不是完全不会做，而是会在缺失条件时继续给出貌似完整的答案。错误版本被明确判定为不安全，说明最终结果并不依赖模型的语言自信程度，而取决于证明能否通过形式系统。

但这不等于“Signal绝对安全”

形式化证明只能覆盖已经写入规格、语义模型和可信边界的安全性质。

此次工作验证的是 Signal 核心密码协议实现，而不是 Signal 应用从界面到操作系统的完整安全审计。消息通知泄露、设备被植入恶意软件、备份配置错误、随机数源失效、供应链攻击和用户被钓鱼等问题，并不会因为核心协议获得证明而自动消失。

开源仓库也明确显示，验证运行在 CLI harness 中，并对部分密码学原语使用了 hook 模型。这意味着底层原语的正确性和模型对应关系仍属于可信计算基础的一部分。严格来说，结论应当表述为：在指定规格、密码假设、指令语义与可信组件成立时，被覆盖的机器代码满足相应安全性质。(github.com)

| 常见说法 | 是否准确 | 更严谨的表述 | |---|---:|---| | Signal已经被证明没有任何漏洞 | 否 | 核心密码代码的若干关键安全性质获得证明 | | AI独立完成了全部验证 | 否 | 人类定义和审核规格，AI生成证明，Lean内核检查 | | 证明覆盖整个Signal应用 | 否 | 重点覆盖libsignal及相关协议路径 | | 证明结果依赖相信大模型 | 否 | 最终证明可由Lean内核重新检查 | | 任何软件现在都能四周完成验证 | 否 | 生成证明所需资源和通用扩展性仍未明确 |

形式化验证最难的部分也不只是“把证明写出来”，而是确定“究竟应该证明什么”。如果规格遗漏了攻击路径，证明器可能完美证明一个不完整的目标。AlphaProof Code 可以显著降低证明搜索与工程实现成本，但安全规格仍然需要密码学家、系统工程师和形式化方法专家共同把关。

四周很快，算力账仍然没公布

验证生成成本是决定 AlphaProof Code 能否进入日常软件工程的关键变量。

DeepMind 尚未披露四周研究使用了多少加速器、模型调用和并行智能体资源，因此目前无法计算一次同类验证的真实成本。四周这个数字很惊艳，但如果背后需要大规模集群持续运行，它更接近科研项目，而不是普通团队可以加入 CI 的工程工具。

开源仓库给出的本地复核要求相对具体：完整构建和检查证明需要数小时，峰值内存约 15GB 至 34GB，并建议按照每约 4GB 可用内存配置一个 Lean 线程。这只是复核已有证明的资源，不等于从零生成 650 万行证明所需的算力。(github.com)

这个区别类似于验证一道数学题答案和首次解出这道题：前者可以快速检查每一步，后者可能需要长时间搜索。形式化证明之所以适合与大模型结合，正是因为生成过程可以昂贵且不稳定，验证过程却必须相对确定、便宜和可重复。

AI正在从程序员变成证明工程师

证明工程师是负责把软件行为建模为数学规格，并构建机器可检查证明的软件与数学交叉角色。

过去两年，大模型进入软件开发的主线是写代码、补测试、做代码审查和寻找漏洞。AlphaProof Code 展示了下一阶段：AI 不只生产更多代码，也生产关于代码为什么正确的证据。

这会改变 AI 编程工具的竞争指标。今天的产品主要比较代码接受率、任务完成率和修复漏洞数量；未来更有价值的指标可能是：一个智能体提交功能时，能否同时提交安全不变量、边界条件和可由证明器检查的正确性证书。

Signal 并不是孤立项目。2026 年 4 月启动的 Signal Shot 计划，已经联合 Signal、Lean FRO、Google、微软以及多所高校，推动用 Lean 验证 Signal 协议和应用。该计划同时推进功能正确性与协议安全两条路线，目标还包括让验证随软件版本持续更新。DeepMind 此次成果可以视为这条路线上的一次激进加速，而不是从零开始的魔法演示。(github.com)

真正的价值是缩短“代码到证明”的距离

AlphaProof Code 的突破不是消灭形式化验证专家，而是把专家时间从机械证明转向安全定义和高风险判断。

650 万行证明代码几乎不可能由人逐行审查，也没有必要。Lean 内核负责检查形式正确性，人类重点审核规格、可信组件和少量高风险区域。这与现代编译器的分工类似：工程师不手工检查每条机器指令，而是信任一条经过严格控制的工具链。

我的判断是，这项成果足以称为里程碑，但还称不上形式化验证的“ChatGPT 时刻”。它证明了大模型能够把过去需要多年专家劳动的项目压缩到以周计算，却没有证明成本已经低到可以覆盖普通应用，也没有解决规格遗漏和可信边界问题。

短期内，AlphaProof Code 最适合密码库、操作系统内核、支付系统、医疗设备和基础设施控制软件。这些系统一旦出错，损失足以覆盖高昂的验证成本。普通 Web 应用不会因为这项研究立刻开始编写数百万行 Lean，但高风险软件采购可能逐渐出现新要求：不仅提交测试报告和安全审计，还要提交可重复检查的形式化证明。

更长远的变化是，软件行业可能从“发布后找漏洞”转向“发布时携带证明”。当攻击者也能用智能体批量寻找漏洞时，只靠更快的补丁速度并不占优势；让关键代码附带数学可验证的安全声明，才可能真正改变攻防的不对称关系。

DeepMind 这次没有证明所有软件都会变得安全，但它至少证明了一件事：大模型已经不满足于替开发者敲代码，它开始进入计算机科学最严苛的区域之一——为真实世界的软件写下可以被机器逐步核验的数学证明。

参考来源

• Google DeepMind：Signal形式化验证开源仓库——包含Lean证明、AArch64语义、验证范围、构建要求与论文到代码的映射。
• Signal Shot项目仓库——介绍Signal协议和应用的长期形式化验证计划、参与机构与技术路线。
• IT之家：谷歌DeepMind用AI完成Signal协议形式化验证——中文事件报道，整理验证耗时、适用范围及研究团队表态。