11月11日，据报道，谷歌 DeepMind 团队最近换了个思路：让 AI 智能体对 Signal 协议做形式化验证，用数学方法证明这套加密确实守得住。
Signal 协议的应用范围远不止 Signal 这款应用本身。WhatsApp、谷歌信息（Google Messages）的加密通信同样建立在它之上，因此这次验证被 DeepMind 形容为“一项具有里程碑意义的进展”。
所谓形式化验证，是指用数学方法严格证明或证伪某个加密算法、协议是否满足其安全性承诺。它和传统测试的逻辑完全不同：测试是拿着已知的攻击手法去试，没试出问题，并不等于没有问题；形式化验证则要求证明协议在所有符合既定模型的条件下都成立，把“可能存在未发现漏洞”这个口子尽量堵死。
让具备自主执行能力的 AI 智能体来完成这项工作，对密码学和人工智能两个领域都有意义。但代价也不小——整个过程消耗了大量算力。谷歌向《连线》表示，目前还无法确定这项技术在更大范围内推广时的实际可行性。
DeepMind 研究科学家斯瓦拉特·乔杜里（Swarat Chaudhuri）把这次成果定位为“研究进程中的一个里程碑”：“我们对结果感到非常兴奋，但要把这项技术扩展到全世界所有软件，还有很长的路要走，而这正是我们希望实现的目标。”
需要说明的是，此次验证的对象是 Signal 加密协议本身，而不是对 Signal 整个应用做全面安全审查。不过有个结果值得留意：研究团队还用同一套方法测试了包含已知漏洞的旧版 Signal 协议实现，AI 成功识别出问题，并判定这些版本未能通过形式化验证。
这项研究也不是从零起步。团队复用了此前已经完成的部分形式化验证成果，其中一些工作并没有借助 AI。整个分析过程耗时约四周，谷歌暂未公布具体投入的算力规模，因此短期内恐怕还看不到大批加密协议排着队完成同类验证。
但方向已经很清楚：AI 不再只是帮开发者写代码、查代码，它开始被用来做数学层面的“安全体检”，验证一套安全机制是不是真的可靠。
原创文章，作者：Google，如若转载，请注明出处：https://www.kejixun.co/article/767832.html
