谷歌 DeepMind 用 AI 完成 Signal 协议形式化验证，数学证明其端到端加密可靠性
要点
- 龙腾代码 11 月 10 日消息，长期以来，Signal 加密协议一直被视为端到端加密消息传递的黄金标准。如今，谷歌 D
- 据龙腾代码了解，除了 Signal 应用本身，这套加密协议也被 WhatsApp 和谷歌内容（Google Messag
- 所谓“形式化验证”，是指通过数学路径，严格证明或证伪某种加密算法或协议是否满足其安全性承诺。与传统测试不同，形式化验证旨
龙腾代码 11 月 10 日消息，长期以来，Signal 加密协议一直被视为端到端加密消息传递的黄金标准。如今，谷歌 DeepMind 队伍利用人工智能，对这一协议的安全性进行了正式验证（Formal Verification）。
据龙腾代码了解，除了 Signal 应用本身，这套加密协议也被 WhatsApp 和谷歌消息（Google Messages）采用，这项探究成果被描述为“一项具有里程碑意义的进展”。
所谓“形式化验证”，是指通过数学路径，严格证明或证伪某种加密算法或协议是否满足其安全性承诺。与传统测试不同，形式化验证旨在证明协议在所有符合既定模型的条件下都能满足安全要求，而不只是通过测试寻找已知漏洞。传统测试即使没有发现问题，也无法保证不存在其他尚未被发现的漏洞。
利用具备自主执行能力的 AI 智能体完成形式化验证，对密码学和人工智能板块都具有枢纽意义。不过，这一过程需要消耗大量计算资源。谷歌向《连线》（Wired）表示，目前还无法确定这项技术力在更大范围内推广应用的实际可行性。
DeepMind 探究人员也强调，此次成果只是整个探究进程中的一个里程碑。DeepMind 探究科学家斯瓦拉特 · 乔杜里（Swarat Chaudhuri）表示：“我们对这一结果感到非常兴奋，但要将这项技术力扩展到全世界所有软件，还有很长的路要走，而这正是我们希望实现的目标。”
需要特别说明的是，此次验证针对的是 Signal 加密协议本身，而不是对 Signal 整个应用程序进行了全面安全审查。不过，有一个结果值得关注：探究人员还使用该路径测试了包含已知安全漏洞的旧版 Signal 协议实现，AI 成功识别出相关问题，并判定这些版本未能通过形式化验证。
此外，谷歌此次探究并非完全从零开始。探究队伍利用了此前已经完成的部分形式化验证成果，其中一些工作并未借助人工智能。
整个探究过程耗时约四周，谷歌尚未公布完成这项工作所需的具体计算资源规模。因此，外界暂时还不能期待大量其他加密协议在短时间内陆续完成类似验证。
尽管如此，这仍然是一项意义重大的进展：AI 不仅能够帮助开发人员编写和检查代码，还有望通过严格的数学证明，验证软件安全机制是否真正可靠。
“掌”握科技鲜闻 （微信搜索techsina或扫描左侧二维码关注）
新浪科技为你带来最新鲜的科技资讯
苹果汇为你带来最新鲜的苹果业务新闻
新酷业务第一时间免费试玩
带来最新的科学家新闻，精彩的震撼图片