Google DeepMind 正式验证 Signal 协议的关键安全保证

发生了什么

Google DeepMind 的研究人员使用智能体式 AI 和名为 AlphaProof Code 的框架，对 Signal 协议中选定的密码学安全保证进行了形式化验证。这项为期四周的概念验证未在所检查的部分发现新的漏洞；研究人员表示，AlphaProof Code 识别出了旧版 Signal 中已知且早已修复的漏洞。他们将发布相关规范和证明，以支持进一步开展形式化验证工作。

接下来读什么

• 今日还有哪些重要变化Google DeepMind 推出 Gemini 4 Hydrogen，加速智能体工作流

5 家信源报道

这件事到目前为止

Google DeepMind 使用 AlphaProof Code，对 Signal 协议底层编译代码中的部分密码学保证进行了形式化验证。这项为期四周的概念验证生成了超过 600 万行 Lean 证明，均由 Lean 自动检查；人类专家审查了每项规范，并检查了约占代码库 1% 的、被标记为需要再次审查的代码。检查的部分未发现新的漏洞。 使用两个此前已修复的漏洞进行的测试，生成了机器检查的证明，表明较早的含漏洞版本并不安全。DeepMind 正在发布其规范和证明，以支持进一步的形式化验证工作。