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

11月10日消息，Signal加密协议在端到端加密消息领域一直被当作黄金标准。谷歌DeepMind团队现在用人工智能对它做了一次正式验证（Formal Verification），从数学层面检验其安全性。

这套协议不只服务于Signal应用本身，WhatsApp和谷歌信息（Google Messages）也在使用。研究团队把这次成果称为“一项具有里程碑意义的进展”。

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

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

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

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

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

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

即便如此，这仍是一项分量很重的进展：AI不光能帮开发人员写代码、查代码，还有望通过严格的数学证明，去检验软件的安全机制是否真的可靠。