Google DeepMind 用 AlphaProof Code 对 Signal 协议机器码完成形式化安全验证

Rohan Paul· @rohanpaul_ai · X·2026-11-10 23:38· 1 小时前精选AI 评分79

AI 导读

Google DeepMind 发布 AlphaProof Code 多智能体形式化验证框架，并首次对广泛部署协议 Signal 的生产机器码完成形式化安全验证。

推荐理由

转发梳理了 DeepMind 用 AI 智能体形式化验证 Signal 机器码的细节，读者可以了解验证流程、规模和相对人工团队的成本变化。

Google DeepMind 取得重大成就，展示了一个 AI 系统能够以数学方式证明软件是安全的，而无需信任 AI 本身。

他们只是用 AI 智能体以数学方式证明了 Signal 实际运行的代码能保持消息机密。

Google 的 AI 智能体编写了 650 万行数学证明，证明 Signal 编译后的代码能保持聊天私密。

检查是在处理器实际执行的指令层面进行的。该实验室表示，此前从未有人对任何广泛使用的协议做到这一点。

常规测试会尝试许多输入，并希望命中那个坏输入。而证明则表明安全规则在所有情况下都成立，并且 Lean 证明检查器会拒绝 AI 写出的任何错误步骤。

真实缺陷往往在设计被转化为代码时潜入，因此检查处理器层面的代码填补了这一缺口。Rust 编译器也不被信任，因此编译器犯的错误也会被捕获。

这项工作耗时 4 周，而专家团队过去需要数年。由 40 到 80 个 Gemini Carbon 智能体组成的团队编写了约 650 万行 Lean，而人类设定安全目标并审查智能体标记出的 1%。

为了检查该系统不能随便批准任何代码，研究人员将 2 个旧的、已修复的 Signal 缺陷重新放回一个副本中。两次它都生成了机器检查的证明，表明该代码不安全。

更大的转变在于成本：既然 AI 能在数周内产出机器检查的证明，而不是耗时数年的项目，这类证明将成为设备固件、电网软件和其他关键代码的常规检查。

引用Pushmeet Kohli@pushmeet

宣布我的团队 @GoogleDeepMind 达成的一项重大里程碑：我们证明了 Signal 消息协议底层机器代码的关键安全属性。这是首次对广泛部署协议的实际生产代码进行如此深度的形式化验证——无论采用何种方法，无论是否借助 AI。
这不仅是研究突破，更是前沿 AI 如何成为力量倍增器、以对抗现代网络威胁的速度和规模的绝佳范例。
形式化验证提供了更高的安全标准；然而，它极其复杂且耗时，因此在许多情况下被认为不切实际。类似的工作可能需要团队数十年的合力才能完成。我们在一个月内就做到了。
借助 AlphaProof Code——Google DeepMind 新的形式化验证智能体框架，运行于包括 Gemini Carbon 在内的 LLM 之上——我们将 Signal 协议验证到了设备上实际运行的代码层面。这一里程碑为未来奠定了基础：从医疗设备固件到电网软件，关键系统在交付时都将附带其防护措施有效的数学证明。
要实现这一未来，需要我们社区持续的研究。本着这一精神，我们将开源我们的形式化规范和验证产物，以便他人能在此基础上继续构建。
就个人而言，这一刻对我意义深远。二十多年前，我作为一名实习生开始了自己的研究之旅，从事检查复杂软件系统一致性的工作。看到这一宏大挑战借助现代 AI 变得切实可行，实在非同寻常。
我为我的团队成员感到无比自豪：Swarat Chaudhuri、Andrew Ferraiuolo、Anton Kovsharov、Tej Chajed、Sam Schlesinger、Karn Seth、Jonathan Katz 和 Charles Sutton，他们接受了这一宏大挑战并交付了成果；也感谢 Signal 团队的合作。
deepmind.google/blog/formal-v…

原文

Announcing a major milestone achieved by my team @GoogleDeepMind: we have proven key security properties of the machine code underlying the Signal messaging protocol. This is the first time the actual production code of a widely deployed protocol has been formally verified – by any method, with or without AI – and at this depth.

More than a research breakthrough, it’s a prime example of how frontier AI can be a force multiplier to counter the speed and scale of modern cyber threats.

Formal verification offers a higher standard of security; however, it’s extremely complex and time consuming, which is why in many cases it’s considered to be impractical. Similar efforts could take teams decades of combined effort. We did it in a month’s time.

Using AlphaProof Code, Google DeepMind's new agentic framework for formal verification that runs on LLMs including Gemini Carbon, we verified the Signal protocol down to the actual code running on devices. This milestone lays the groundwork for a future in which vital systems, from medical device firmware to power grid software, ship with mathematical proof that their protections work.

Reaching that future will take continued research from our community. In that spirit, we're open-sourcing our formal specifications and verification artifacts so others can build on this work.

On a personal note, this moment is of deep significance to me. I started my own research journey more than two decades ago as an intern working on checking the consistency of complex software systems. Seeing this grand challenge made practical with modern AI is extraordinary.

I'm extremely proud of my team members: Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, and Charles Sutton for taking on this grand challenge and delivering, and grateful to the Signal team for their partnership.

deepmind.google/blog/formal-v…

在 X 查看被引用的帖子

来源：Rohan Paul · x.com