近日，谷歌DeepMind团队利用具备自主执行能力的AI智能体，对Signal加密协议进行了形式化验证，相关成果被描述为一项具有里程碑意义的进展。Signal加密协议长期被视为端到端加密消息传递的黄金标准，除Signal应用本身外，该协议也被WhatsApp和谷歌信息采用。

形式化验证是指通过数学方法严格证明或证伪加密算法或协议是否满足其安全性承诺，旨在证明协议在所有符合既定模型的条件下都能满足安全要求，而非仅通过测试寻找已知漏洞。研究人员还使用该方法测试了包含已知安全漏洞的旧版Signal协议实现，AI成功识别出相关问题并判定这些版本未能通过形式化验证。此次验证针对的是Signal加密协议本身，并非对Signal整个应用程序进行全面安全审查。

谷歌此次研究并非完全从零开始，研究团队利用了此前已完成的部分形式化验证成果，其中一些工作并未借助人工智能，整个分析过程耗时约四周。谷歌向媒体表示，目前还无法确定这项技术在更大范围内推广应用的实际可行性，尚未公布完成这项工作所需的具体计算资源规模。DeepMind研究科学家斯瓦拉特·乔杜里表示，对这一结果感到非常兴奋，但要将这项技术扩展到全世界所有软件还有很长的路要走。