谷歌 DeepMind 团队近日利用 AI 智能体完成了对 Signal 加密协议的形式化验证，通过数学方法证明了该协议满足其端到端加密的安全承诺。Signal 协议被广泛应用于 Signal 应用、WhatsApp 和谷歌信息（Google Messages），长期被视为端到端加密消息传递的行业基准。这项研究成果被描述为“一项具有里程碑意义的进展”。
形式化验证与传统的安全测试存在本质差异。传统测试通过构造攻击场景寻找已知漏洞，即便未发现问题，也无法排除其他尚未被发现的缺陷。形式化验证则借助数学方法，在既定模型下严格证明或证伪协议是否满足安全要求，覆盖所有符合模型条件的运行情形。此次验证的对象是 Signal 加密协议本身，而非对 Signal 整个应用进行全面的安全审查。
值得关注的是，研究人员还使用同一方法测试了包含已知安全漏洞的旧版 Signal 协议实现，AI 成功识别出相关问题，并判定这些版本未能通过形式化验证。这表明该方法在检测真实缺陷方面具备实际能力。此外，本次研究并非从零开始，团队复用了此前已完成的部分形式化验证成果，其中一些工作并未借助人工智能。整个分析过程耗时约四周，谷歌尚未披露所消耗的具体计算资源规模。
利用具备自主执行能力的 AI 智能体完成形式化验证，对密码学和人工智能两个领域均具有重要意义。但该过程需要消耗大量计算资源，谷歌向《连线》表示，目前尚无法确定这项技术在更大范围推广应用的可行性。DeepMind 研究科学家 Swarat Chaudhuri 表示，团队对结果感到兴奋，但要将该技术扩展到全世界所有软件仍有很长的路要走，而这正是其希望实现的目标。
从行业影响看，这一成果展示了 AI 在软件安全验证领域的潜在价值：AI 不仅能辅助开发者编写和检查代码，还有望通过严格的数学证明来验证安全机制是否真正可靠。不过，由于计算成本高企且方法尚处早期阶段，短期内不宜期待大量加密协议陆续完成类似验证。此次成果更宜被视为研究进程中的一个里程碑，而非可立即规模化落地的工程方案。
该文观点仅代表作者本人，企服科学平台仅提供信息存储空间服务。
