DeepMind 用 AI 验证 Signal 协议安全属性

AI 能不能检查加密协议，正在从「帮忙找漏洞」走向「参与数学证明」。据 IT之家 11 月 10 日报道，Google DeepMind 利用 AI 完成了针对 Signal 加密协议的形式化验证，还识别出了旧版实现中的已知安全问题。

但这项成果不能直接读成「Signal 应用已被证明绝对安全」。验证依赖既定模型，也借助了已有研究，整个分析过程耗时约四周，具体算力规模没有公布。值得读懂的，是它验证了什么，以及这条技术路线离日常开发还有多远。

形式化验证比测试多回答了什么

Signal 协议除了用于 Signal，也被 WhatsApp 和 Google Messages 采用。研究关注的是这套协议的安全承诺能否成立。

传统测试通过构造输入、执行程序、观察结果来发现问题。测试通过，只能说明这些测试没有暴露问题，不能覆盖所有可能情况。

形式化验证（Formal Verification）则先把协议行为、安全要求和相关假设写成数学模型，再证明或证伪模型中的安全性质。大白话理解：测试是在挑选案例检查，形式化验证是在明确规则后，推导符合规则的情况是否都满足要求。

证明成立的范围，由模型和假设共同决定。

因此，「在所有符合既定模型的条件下成立」中的限定不能省略。报道没有交代具体证明了哪些安全性质、采用什么威胁模型，以及使用了哪些验证工具，读者无法仅凭这篇报道判断证明覆盖得有多完整。

AI 做出了什么，哪些成本还没公开

此次工作的一个看点，是研究人员使用具备自主执行能力的 AI 智能体参与形式化验证。它的任务已经超出了生成代码或提供审查意见，而是进入需要严格推导的验证过程。

报道给出了一个具体结果：研究人员用同样的方法测试了包含已知安全漏洞的旧版 Signal 协议实现，AI 成功识别相关问题，并判定这些版本未通过形式化验证。

这比单独报告一次验证成功更有说服力，因为它展示了该方法能够拒绝有问题的版本。不过，报道没有列出漏洞数量、具体类型，也没有说明它能否发现未知漏洞，不能据此推断其一般性的漏洞发现能力。

另外，两项前提会影响我们对成果的理解：

• 研究团队利用了此前已经完成的部分形式化验证成果，其中一些工作没有借助 AI。此次工作有既有研究作为基础。
• 整个分析过程耗时约四周，需要消耗大量计算资源，但 Google 尚未公布具体算力规模。四周的工期无法直接换算成一般团队可承担的成本。

Google 向 Wired 表示，目前还无法确定这项技术大范围推广的实际可行性。DeepMind 研究科学家 Swarat Chaudhuri 也把它定位为研究进程中的一个里程碑，距离扩展到全世界所有软件仍有很长的路。

我的判断

我认可这项工作的方向：涉及安全承诺时，可检查的数学证明，比 AI 给出一句「代码看起来没有问题」更有价值。旧版缺陷能够被识别，也为方法有效性提供了一项具体证据。

但这里有两层边界。

第一，验证对象是 Signal 加密协议，并非 Signal 整个应用。应用中的其他代码、依赖与运行环境是否安全，不能由协议验证代为回答。

第二，这篇报道没有提供与人工形式化验证、其他自动化方法的对照数据。AI 到底节省了多少人力、提高了多少效率，目前无法判断。对于「显著降低验证门槛」这样的进一步结论，还缺少证据。

这是一项有具体结果的研究进展，还不足以成为普通团队立即采用的工程方案。

对日常开发而言，测试和代码审查仍然有直接价值。形式化验证回答的是特定模型中的性质是否成立；实际应用的行为是否符合需求，还需要其他检查共同支撑。

能拿来做什么

• 在前端或 Node 项目里接入端到端加密方案时，把「协议安全性」和「应用实现安全性」分开评估，不要把协议的研究成果当成整个产品的安全保证。
• 让 AI 审查安全相关代码时，要求它列出检查目标、成立前提和可复核依据，避免只接收「未发现问题」这样的结论。
• 评估 AI 形式化验证工具时，优先询问证明覆盖范围、已有证明依赖、缺陷案例表现和计算成本。这篇报道恰好说明，这几项信息决定了研究成果能否落地。