谷歌 DeepMind 用 AI 完成 Signal 协议形式化验证，数学证明其端到端加密可靠性

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

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

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

让具备自主执行能力的 AI 智能体来做形式化验证，对密码学和人工智能两个领域都有分量。问题是这个过程很吃算力。谷歌对《连线》（Wired）说，这项技术能不能在更大范围内推广，实际可行性目前还说不准。

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

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

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

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

即便有这些保留，进展本身仍有分量：AI 不只能帮开发人员写代码、查代码，还有望通过严格的数学证明，去验证软件的安全机制是否真的可靠。