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

IT之家 11 月 10 日消息，长期以来，Signal 加密协议一直被视为端到端加密消息传递的黄金标准。如今，谷歌 DeepMind 团队利用人工智能，对这一协议的安全性进行了正式验证（Formal Verification）。

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

所谓“形式化验证”，是指通过数学方法，严格证明或证伪某种加密算法或协议是否满足其安全性承诺。与传统测试不同，形式化验证旨在证明协议在所有符合既定模型的条件下都能满足安全要求，而不只是通过测试寻找已知漏洞。传统测试即使没有发现问题，也无法保证不存在其他尚未被发现的漏洞。

利用具备自主执行能力的 AI 智能体完成形式化验证，对密码学和人工智能领域都具有重要意义。不过，这一过程需要消耗大量计算资源。谷歌向《连线》（Wired）表示，目前还无法确定这项技术在更大范围内推广应用的实际可行性。

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

需要特别说明的是，此次验证针对的是 Signal 加密协议本身，而不是对 Signal 整个应用程序进行了全面安全审查。不过，有一个结果值得关注：研究人员还使用该方法测试了包含已知安全漏洞的旧版 Signal 协议实现，AI 成功识别出相关问题，并判定这些版本未能通过形式化验证。

此外，谷歌此次研究并非完全从零开始。研究团队利用了此前已经完成的部分形式化验证成果，其中一些工作并未借助人工智能。

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

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