Google DeepMind 用 AI 形式化验证 Signal 协议关键部分

核心事实

据 Ars Technica 转载 WIRED 的报道，Google DeepMind 研究人员使用智能体 AI 框架 AlphaProof Code，对 Signal 协议的多项关键密码学保证进行了数学证明，即“形式化验证”。该项目以概念验证形式在四周内完成。DeepMind 研究科学家 Swarat Chaudhuri 表示，团队对这一结果感到兴奋，但要把这种方法扩展到“世界上所有软件”仍有很长的路要走。

背景与影响

Signal 协议为 Signal 应用、Google Messages 和 WhatsApp 等平台的大量通信提供加密保护，此次工作被视为对该密码学的又一次独立验证。报道称，分析未在受检部分发现新漏洞；当研究人员把 AlphaProof Code 用于包含已知且早已修复漏洞的旧版 Signal 时，工具正确识别出这些漏洞，并显示该协议无法通过形式化验证。研究团队公开了为此次分析编写的规范与证明，以供其他形式化验证工作参考。Signal 首席技术官 Ehren Kret 在声明中称，此前的形式化验证聚焦较小代码范围，而 DeepMind 的方法实现了显著扩展。Google Cloud 首席科学家、DeepMind 研究副总裁 Pushmeet Kohli 则提到，银行等依赖安全保证的机构或可借此证明自身属性。

限制与来源

报道指出，此次分析范围有限，并未对整个 Signal 移动应用做形式化验证，DeepMind 研究人员称其只是更大进程中的一个里程碑。AI 自动化的形式化验证能否真正规模化、成本是否可承受，仍是整个科技行业的未解问题。DeepMind 以研究项目形式免费完成该分析，Google 拒绝披露成本，也未就是否推出商业化形式化验证产品或服务置评。本文信息来自 Ars Technica 对 WIRED 报道的转载，相关细节以原始报道及各方官方信息为准。