谷歌DeepMind借助AI完成Signal协议形式化验证，确立加密可靠性
谷歌DeepMind团队利用AI智能体对Signal加密协议完成形式化验证，这是里程碑式进展。研究证实该协议满足安全承诺，且能识别旧版漏洞。虽耗时四周且资源消耗大，但为软件安全验证提供了新路径，未来有望扩展至更多领域。
谷歌DeepMind团队近日宣布，利用人工智能技术成功对Signal加密协议进行了形式化验证。这项被形容为里程碑式的成果，通过数学方法严格证明了该协议在既定模型下满足安全性承诺。作为端到端加密消息传递的标杆，Signal协议此前已广泛应用于WhatsApp和谷歌信息等平台。
形式化验证区别于传统测试，它旨在证明协议在所有条件下均安全可靠，而非仅寻找已知漏洞。DeepMind利用具备自主执行能力的AI智能体完成了这一复杂过程，这对密码学与AI领域意义重大。然而，研究团队向《连线》表示，目前尚无法确定该技术在更广泛范围内推广的可行性，且整个分析过程耗时约四周，具体计算资源规模未公布。
值得注意的是，此次验证仅针对Signal协议本身，而非整个应用程序的全面安全审查。研究团队还测试了包含已知漏洞的旧版Signal实现，AI成功识别出问题并判定其未通过验证。此外，谷歌并未从零开始，而是利用了此前部分非AI完成的形式化验证成果作为基础。
DeepMind研究科学家斯瓦拉特·乔杜里强调，当前成果仅是长远的阶段性突破。他表示：“我们对这一结果感到非常兴奋，但要将这项技术扩展到全世界所有软件，还有很长的路要走。”这表明尽管AI在编写和检查代码方面展现出潜力，但通过数学证明验证所有软件安全机制仍需大量时间与资源投入，短期内难以大规模应用。
