谷歌 DeepMind 用 AI 完成 Signal 协议形式化验证
谷歌 DeepMind 用 AI 完成 Signal 协议形式化验证，数学证明其端到端加密可靠性
DeepMind 让 AI 智能体给 Signal 协议写数学证明，WhatsApp 和 Google Messages 都在用这套协议。旧版有漏洞的实现还被它揪出来了。做密码学或安全工程的值得看看 AI 形式化验证这条路走到了哪一步。
谷歌 DeepMind 团队利用具备自主执行能力的 AI 智能体，对 Signal 加密协议完成了形式化验证，通过数学方法严格证明其满足端到端加密的安全承诺。这套协议除 Signal 应用外，还被 WhatsApp 和谷歌信息（Google Messages）采用，研究成果被描述为里程碑式进展。与传统测试只能寻找已知漏洞不同，形式化验证能证明协议在所有符合既定模型的条件下都满足安全要求。
验证过程耗时约四周，谷歌尚未公布具体计算资源规模。研究人员还用该方法测试了包含已知安全漏洞的旧版 Signal 协议实现，AI 成功识别出问题并判定这些版本未通过验证。不过这项工作并非从零开始，团队利用了此前已部分完成、部分未借助 AI 的形式化验证成果。
DeepMind 研究科学家 Swarat Chaudhuri 表示，要将该技术扩展到全球所有软件还有很长的路要走。谷歌也向《连线》（Wired）承认，目前无法确定该技术在更大范围内推广应用的实际可行性。此次验证针对的是 Signal 协议本身，并非对整个应用程序的全面安全审查。
谷歌 DeepMind 用 AI 完成 Signal 协议形式化验证，数学证明其端到端加密可靠性
IT之家 11 月 10 日消息，长期以来，Signal 加密协议一直被视为端到端加密消息传递的黄金标准。如今，谷歌 DeepMind 团队利用人工智能，对这一协议的安全性进行了正式验证（Formal Verification）。 据IT之家了解，除了 Signal 应用本身，这套加密协议也被 WhatsApp 和谷歌信息（Google Messages）采用，这项研究成果被描述为“一项具有里程碑意义的进展”。 所谓“形式化验证”，是指通过数学方法，严格证明或证伪某种加密算法或协议是否满足其安全性承诺。与传统测试不同，形式化验证旨在证明协议在所有符合既定模型的条件下都能满足安全要求，而不只是通过测试寻找已知漏洞。传统测试即使没有发现问题，也无法保证不存在其他尚未被发现的漏洞。 利用具备自主执行能力的 AI 智能体完成形式化验证，对密码学和人工智能领域都具有重要意义。不过，这一过程需要消耗大量计算资源。谷歌向《连线》（Wired）表示，目前还无法确定这项技术在更大范围内推广应用的实际可行性。 DeepMind 研究人员也强调，此次成果只是整个研究进程中的一个里程碑。DeepMind 研究科学家斯瓦拉特 · 乔杜里（Swarat Chaudhuri）表示：“我们对这一结果感到非常兴奋，但要将这项技术扩展到全世界所有软件，还有很长的路要走，而这正是我们希望实现的目标。” 需要特别说明的是，此次验证针对的是 Signal 加密协议本身，而不是对 Signal 整个应用程序进行了全面安全审查。不过，有一个结果值得关注：研究人员还使用该方法测试了包含已知安全漏洞的旧版 Signal 协议实现，AI 成功识别出相关问题，并判定这些版本未能通过形式化验证。 此外，谷歌此次研究并非完全从零开始。研究团队利用了此前已经完成的部分形式化验证成果，其中一些工作并未借助人工智能。 整个分析过程耗时约四周，谷歌尚未公布完成这项工作所需的具体计算资源规模。因此，外界暂时还不能期待大量其他加密协议在短时间内陆续完成类似验证。 尽管如此，这仍然是一项意义重大的进展：AI 不仅能够帮助开发人员编写和检查代码，还有望通过严格的数学证明，验证软件安全机制是否真正可靠。
This report is categorized under AITOP's "Models" desk, focusing on US frontier AI labs and Silicon Valley technology leaders. Within our cross-regional analytical framework, it directly maps to AI developer toolchains, coding agents, and engineering workflows and US-China foundation model benchmarks and commercialization comparison. Key entities and technical topics under continuous tracking include Google DeepMind, Signal, 形式化验证, 端到端加密.
Source attribution: curated from IT之家.
