Google DeepMind 新 AI 工具证明 Signal 协议安全

Google DeepMind 研究人员利用代理式 AI，在短短四周内通过数学方法对 Signal 协议的关键加密保障进行了形式化验证。这一里程碑式的成果不仅为 WhatsApp、Google Messages 等广泛使用的平台提供了独立的安全背书，也展示了其新 AI 框架 AlphaProof Code 的强大能力。分析未发现新的漏洞，且能准确识别已知旧版本中的缺陷，但需注意的是，此次验证并未覆盖整个 Signal 移动应用的全部代码。

形式化验证被视为软件安全的“圣杯”，旨在用数学证明软件无关键漏洞。此前该过程耗时极长，而 Agentic AI 大幅缩短了构建证明的时间。DeepMind 强调这仅是更大进程中的一步，并非最终结论。为了推动行业进步，研究团队已公开相关的规范与证明细节。Signal 首席技术官表示，虽然前期工作侧重于较小部分代码，但 Google DeepMind 的方法实现了显著扩展，进一步增强了对其隐私保证的信心。

尽管前景广阔，AI 辅助形式化验证能否规模化及成本控制仍是业界难题。DeepMind 将此作为免费研究项目，未透露具体成本，也未回应是否计划推出商业产品。研究人员指出，关键进展在于建立“人机协作流程”，让 AI 在几乎每个阶段贡献并自我纠正，同时在关键环节寻求人类审查。他们明确表示，不希望出现 AI 完全自主生成目标和证明的封闭循环，而是要保持中间地带的协作平衡。