DeepMind AI完成Signal加密形式化验证

时间：2026年11月10日，Google DeepMind 正式发布 AlphaProof Code 框架，宣布研究团队利用 AI 代理成功完成对加密通讯软件 Signal 核心加密协议的数学验证。 地点：美国（Google DeepMind 总部） 人物：Google DeepMind 研究团队，包括 Pushmeet Kohli、Swarat Chaudhuri 等 事件详情：DeepMind 开发的 AlphaProof Code 结合人类专家审核与 AI 代理（基于 Gemini 4 Carbon 模型），在仅 5 人团队、4 周时间内生成 650 万行形式化证明代码，完成了对 Signal 协议中后量子 PQXDH 握手协议与 Triple Ratchet 算法的验证。验证覆盖前向保密、身份验证、入侵后安全及握手保密性四大安全属性。团队还将这套方法用于测试已知存在漏洞的旧版 Signal 程序，AI 成功识别出缺陷并判定该版本无法通过验证。 背景：形式化验证是软件安全领域的「圣杯」，传统方法往往需要数年时间、数十人团队才能完成一次。过去，安全研究人员只能通过代码审计和渗透测试发现漏洞，无法在数学层面证明加密协议「没有漏洞」。Signal 作为全球数亿用户使用的加密通讯工具，其协议安全性一直备受关注。 影响：这是首次有 AI 系统在真实世界广泛使用的加密协议上完成机器码级别（machine code level）的形式化验证。研究团队将验证周期从数年压缩到 4 周，成本与人力大幅下降。该方法未来可扩展至更多关键软件与安全场景，有望改变网络安全验证的工业流程，让高强度的数学验证不再是少数专家的专利。 总结：DeepMind 的 AlphaProof Code 展示了 AI 在形式化验证领域的巨大潜力。通过人机协作模式，研究团队不仅证明了 Signal 协议的安全性，也为未来更大规模的软件验证提供了可复用的框架。这一突破意味着 AI 辅助安全验证正在从理论研究走向实际部署，为全球加密通讯的安全保障提供了新的技术路径。 常见问题： 问：AlphaProof Code 是什么？ 答：Google DeepMind 开发的 AI 框架，结合人类专家审核与 AI 代理，用于对复杂软件进行形式化验证。 问：这次验证了 Signal 的哪些部分？ 答：主要验证了 Signal 的后量子 PQXDH 握手协议与 Triple Ratchet 算法，覆盖前向保密、身份验证、入侵后安全及握手保密性四大安全属性。 参考来源： DeepMind 官方博客 https://deepmind.google/blog/introducing-alphaproof-code/ TechNews 科技新报 https://technews.tw/2026/11/11/deepmind-ai-successfully-completes-formal-verification-signals-core-encryption/ ArsTechnica https://arstechnica.com/ai/2026/11/signals-encryption-just-passed-an-ai-powered-mathematical-checkup/ ZDNET https://www.zdnet.com/tech/google-deepmind-researchers-prove-signal-whatsapp-encryption-works/ Wired https://www.wired.com/story/a-new-ai-tool-from-google-deepmind-formally-verified-the-signal-protocol/ The Register https://www.theregister.com/2026/11/10/20266/ Axios https://www.axios.com/2026/11/10/google-code-verification-signal