DeepMind用AI验证Signal协议：端到端加密获数学证明

11 月 10 日消息，Signal 加密协议多年来被当作端到端加密消息传递的黄金标准。谷歌 DeepMind 团队如今借助人工智能，对这套协议的安全性做了正式验证（Formal Verification）。

据IT之家了解，采用这套加密协议的不只是 Signal 应用，WhatsApp 和谷歌信息（Google Messages）也在用。这项研究成果被形容为“一项具有里程碑意义的进展”。

形式化验证是什么？就是用数学方法严格证明或证伪某种加密算法、协议是否兑现了它的安全性承诺。它和传统测试的路子不同：目标是证明协议在所有符合既定模型的条件下都满足安全要求，而不是靠测试去翻找已知漏洞。传统测试即便没发现问题，也没法保证不存在其他尚未被发现的漏洞。

这回的形式化验证由具备自主执行能力的 AI 智能体完成，对

DeepMind 研究人员强调，这次成果只是整个研究进程中的一个里程碑。DeepMind 研究科学家斯瓦拉特 · 乔杜里（Swarat Chaudhuri）说：“我们对这一结果感到非常兴奋，但要将这项技术扩展到全世界所有软件，还有很长的路要走，而这正是我们希望实现的目标。”

有一点需要说明：此次验证的对象是 Signal 加密协议本身，并非对 Signal 整个应用做全面安全审查。不过有个结果值得关注——研究人员还用这套方法测了包含已知安全漏洞的旧版 Signal 协议实现，AI 找出了相关问题，并判定这些版本未能通过形式化验证。

谷歌这次的研究也不是完全从零起步。团队用上了此前已经完成的部分形式化验证成果，其中一些工作并没有借助人工智能。

整个分析过程耗时约四周。谷歌尚未公布完成这项工作所需的具体计算资源规模，所以外界暂时还不能指望大量其他加密协议在短时间内陆续完成类似验证。

即便如此，这仍是一项意义重大的进展：AI 不只能帮开发人员编写和检查代码，还有望通过严格的数学证明，验证软件安全机制是否真正可靠。