谷歌 DeepMind 用 AI 证明 Signal 加密协议安全，整个分析耗时四周

Signal 加密协议长期被视为端到端加密的黄金标准，WhatsApp 和谷歌信息也在用它。谷歌 DeepMind 团队最近用 AI 完成了对这套协议的形式化验证，研究成果被形容为“具有里程碑意义”。

形式化验证和传统测试不是一回事。测试是去找已知漏洞，即使什么都没发现，也不能保证不存在别的问题；形式化验证则是用数学方法，证明在既定模型下协议始终满足安全承诺，或者干脆证伪它。

难点在于算力。让具备自主执行能力的 AI 智能体跑完整个验证过程，消耗的计算资源相当可观。谷歌对媒体表示，暂时还无法判断这项技术在更大范围内推广的实际可行性。

研究人员的态度也保持克制。DeepMind 科学家 Swarat Chaudhuri 说，对结果非常兴奋，但要扩展到全世界所有软件还有很长的路要走，而那正是他们想实现的目标。

几个需要说清的边界：这次验证针对的是协议本身，不是对 Signal 整个应用做全面安全审查；研究也不是从零开始，团队利用了此前部分已完成的形式化验证成果，其中一些并没有借助 AI；整个分析耗时约四周，具体用了多少算力没有公布。

不过有个结果值得注意：研究人员拿包含已知漏洞的旧版协议实现做了测试，AI 成功找出了问题，并判定这些版本未能通过验证。这说明 AI 不只是能帮着写代码和查代码，也有望用严格的数学证明，去确认安全机制是不是真的可靠。