DeepMind用AI证明Signal协议核心加密安全性

Google DeepMind 研究团队利用全新 AI 框架 AlphaProof Code，在数学层面成功证明了 Signal 协议的数项核心加密安全保证。据《连线》（WIRED）报道，这项历时四周的概念验证项目未在所审查的协议模块中发现任何新漏洞。

这一成果的影响不仅限于 Signal 本身。Signal 协议同时为 Google Messages 和 WhatsApp 等通讯工具提供底层加密，直接保护着全球庞大的通讯流量。此次分析为这些关键加密通信提供了又一次独立的严格检验。这也表明，AI 智能体能够显著加速形式化验证这一传统上极其缓慢、通过数学逻辑严格证明软件行为符合预期的流程。

分析的核心发现

研究人员还在包含已知漏洞的 Signal 早期版本上测试了 AlphaProof Code。该工具准确识别出这些早已修复的缺陷，并证明这些旧版本无法通过形式化验证。DeepMind 目前正在公开其构建的形式化规范与证明过程，供其他验证项目参考使用。

不过，本次验证的覆盖范围依然有限。研究并未涵盖 Signal 移动端应用的全部代码，团队将其视为长期探索中的一个里程碑。DeepMind 研究科学家 Swarat Chaudhuri 表示：“我们对这一结果感到兴奋，但要将其扩展到全球所有软件，还有很长的路要走。”

Signal 首席技术官 Ehren Kret 在声明中表示，早期的形式化验证通常只针对代码的微小部分，而 Google DeepMind 的方法实现了大幅拓展。面对日益增加的 AI 安全威胁，这项验证让团队对协议安全性更具信心。

行业探索与成本未知数

除 DeepMind 外，其他机构也在进行类似探索。Signal、Beneficial AI 基金会与 Lean FRO 此前联合发起了开源项目 Signal Shot，计划使用 Lean 证明助手来形式化验证 Signal 协议及其 Rust 实现。DeepMind 的研究独立于该项目。

目前，利用 AI 进行自动化验证的成本与规模化可行性仍有待观察。DeepMind 此次作为纯研究项目免费实施了 Signal 验证，Google 尚未透露具体成本，也未表明未来是否会推出商业化验证产品。

Chaudhuri 强调，本次工作的关键突破在于建立了一套人机协作机制——AI 智能体负责生成证明并修正自身工作，人类专家则在关键节点进行审查。他指出，不应让 AI 既出题又答题、完全自闭环运行，人机协同的中间路线才是安全落地的关键。