谷歌DeepMind用AI完成Signal协议安全验证

驱动中国11月10日消息，谷歌DeepMind团队利用人工智能对Signal加密协议开展形式化验证，以数学方法检验这一端到端加密协议的安全性。Signal加密协议长期被视为端到端加密消息传递的黄金标准，除Signal应用外，也被WhatsApp和Google Messages采用。

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

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

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

此次验证针对Signal加密协议本身，而非Signal整个应用程序的全面安全审查。同时，研究人员还使用该方法测试了包含已知安全漏洞的旧版Signal协议实现，AI识别出相关问题，并判定这些版本未通过形式化验证。

谷歌此次研究并非完全从零开始，团队利用了此前已完成的部分形式化验证成果，其中一些工作并未借助人工智能。整个分析过程耗时约四周，谷歌尚未公布完成这项工作所需的具体计算资源规模，因此外界暂时还不能期待大量其他加密协议在短时间内陆续完成类似验证。

这一进展显示，AI除帮助开发人员编写和检查代码外，还有望通过严格数学证明验证软件安全机制是否可靠。