谷歌用AI形式化验证Signal加密协议

时间：2026年11月10日 地点：美国加州山景城谷歌 DeepMind 总部，验证对象为美国开源加密通讯软件 Signal 的底层代码库 libsignal 人物：谷歌 DeepMind 研究员 Pushmeet Kohli、Swarat Chaudhuri，Signal 首席技术官 Ehren Kret，承担证明工作的 Gemini 系列智能体 事件详情：谷歌 DeepMind 于 11 月 10 日发布 AlphaProof Code，一套由多个大模型智能体协作的形式化验证框架。研究人员先与模型配合，把 Signal 的安全目标翻译成形式化数学规格，每一条规格都由人类专家复核；随后由基于 Gemini Carbon 的智能体完成证明，共产出超过 600 万行 Lean 证明代码。智能体随后自行审阅证明，并标出需要人工复看的区域，最终只有 1% 的代码库交由专家二次检查，其余部分由 Lean 自动校验。整个验证过程只用了四周，而同类任务历史上往往需要专家团队数年。这次验证深入到编译后的机器码层面，证明 Signal 协议的实际实现满足关键安全属性，包括设备被临时攻破前后消息仍能得到保护。为确认系统能区分正确代码与有缺陷代码，研究人员把两个此前已修复的真实漏洞重新植入隔离版本的 Signal 代码，两次都被系统给出机器可校验的"不安全"证明。谷歌表示将开源这套形式化验证框架，并与 CodeMender 等自动化防御智能体配合使用。 背景：形式化验证即用数学方法证明代码运行正确，是安全保证的最高标准，但长期费力费时。Signal 是端到端加密通讯工具，其协议也被 Google Messages、WhatsApp 等应用采用，保护着数十亿条私人对话。此前密码协议的形式化验证大多停留在设计层面，而现实中的漏洞常常藏在设计与实现之间的落差里。谷歌 DeepMind 称，这是第一次用 AI 对一个广泛部署的密码协议做这一深度的形式化验证，也是第一次有人工或非人工的任何方法，对这类协议的实现本身完成形式化验证。Signal 首席技术官 Ehren Kret 表示，此前形式化验证只能覆盖较小的代码部分，而新方法把活跃代码自动转成有效 Lean 定理的能力，是一次重大突破。 影响：对 Signal 用户而言，这次验证为其加密实现提供了独立于人工审计的数学保证；对行业而言，四周完成原本需要数年的任务，意味着 AI 智能体正从"写代码"走向"证明代码正确"。谷歌表示，这套方法可为医疗设备固件、电力系统软件等关键基础设施的防护打底，而这些系统正越来越多地暴露在智能体驱动的攻击之下。 总结：谷歌 DeepMind 用 AlphaProof Code 让 AI 智能体完成了 Signal 协议的机器码级形式化验证，600 万行 Lean 证明在四周内产出，人工只需复核 1% 的代码库。这是第一次用 AI 在这一深度验证广泛部署的密码协议实现，也是该协议实现首次被任何方法形式化验证。研究团队同时把两个真实漏洞重新植入代码，系统两次都给出"不安全"的机器可校验证明。谷歌计划开源这套框架，后续目标是把它用到医疗固件、电力软件等关键基础设施上。 参考来源： 谷歌 DeepMind 官方博客 Introducing AlphaProof Code https://deepmind.google/blog/introducing-alphaproof-code/ AlphaProof Code 项目页：机器码层级的 Signal 安全性验证 https://google-deepmind.github.io/code-verification/ 谷歌 DeepMind 技术论文 Formal Verification of Signal's Protocol with Gemini https://deepmind.google/documents/36/Formal_Verification_of_Signal_4.pdf WIRED：A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure https://www.wired.com/story/a-new-ai-tool-from-google-deepmind-formally-verified-the-signal-protocol/ ZDNET：谷歌新工具证明 Signal 加密真实有效 https://www.zdnet.com/tech/google-deepmind-researchers-prove-signal-whatsapp-encryption-works/ The Register：谷歌 DeepMind 用人与 AI 智能体复核 Signal 加密技术 https://www.theregister.com/ai-and-ml/2026/11/10/google-deepmind-melds-humans-and-ai-agents-to-vet-signals-secure-messaging-techniques/