# DeepMind用AI验证Signal加密代码

> AlphaProof Code用四周时间，检查了Signal编译后代码中的关键安全属性。证明仅涵盖特定安全保证，并非Signal的所有部分。

Oossa · 2026-11-11 · https://oossa.com/zh/deepmind-used-ai-to-verify-signal-s-cryptographic-code

Google DeepMind表示，该公司使用AlphaProof Code，对Signal消息协议参考实现libsignal中的关键安全属性进行了数学验证。这项工作耗时四周。DeepMind称，过去类似的验证工作通常需要专家团队花费数年。

这套系统由研究人员与AI代理协同完成。研究人员和AI将Signal的安全目标转化为数学规范，并由人类审核。随后，由Gemini Carbon驱动的代理生成了约650万行Lean证明代码。Lean是一种编程语言，其检查器能够验证数学证明是否符合规则。代理还标出了代码库中约1%的内容，供人工审核。

## 证明涵盖了哪些内容？

研究人员检查了libsignal中后量子PQXDH握手协议和Triple Ratchet的编译后机器码。他们证明了前向保密、身份验证以及设备遭入侵后的保护等特定属性。研究论文称，代码由未修改的Rust代码通过标准编译器编译而成，随后以AArch64机器码进行检查。

这项工作不再局限于证明抽象设计安全，而是将明确规定的安全保证与编译后的代码联系起来。DeepMind称，这是首次以如此深入的程度，对一种广泛部署的加密协议实现进行形式化验证。团队还将两个此前已修复的漏洞重新引入隔离版本的代码；系统生成的证明显示，存在漏洞的版本不符合所述安全属性。

## 这项证明有其局限

这并不意味着Signal的所有部分，或所有使用该协议的应用，都获得了不存在安全问题的数学保证。证明涵盖的是libsignal的部分选定属性，而非整个应用。它也依赖经过批准的规范、Lean检查器，以及针对底层加密例程的契约。The Register指出，这项成果并未证明实际消息字节在计算意义上的保密性；DeepMind的论文则称，证明同时采用了符号模型和计算模型，并依赖关于底层加密原语的假设。

DeepMind表示，将向其他人开放验证材料供其使用。该公司希望把这一方法应用于医疗设备固件、电网软件等领域，但也表示，要扩大这种方法的适用范围，还需要更多研究。这项工作只是朝着验证更多现实世界代码迈出的一步，并不代表那些其他系统已经通过验证。

## 事实

- Google DeepMind于2026年11月10日宣布推出AlphaProof Code。
- 该系统在针对libsignal的工作中生成了约650万行Lean证明代码。
- 验证涵盖了以编译后AArch64机器码呈现的PQXDH握手协议和Triple Ratchet。
- 研究人员重新引入了两个此前已修复的漏洞，系统证明受影响的版本不符合规定的安全属性。

## 为什么重要

对Signal用户而言，这项工作为其核心协议实现中的特定安全属性增添了机器检查证明。但它不能证明整个应用没有漏洞，而且证明依赖于对加密组件的假设。

## 来源与参考

1. [Google Deepmind's AlphaProof Code verified Signal's cryptographic core in four weeks instead of years](https://the-decoder.com/google-deepminds-alphaproof-code-verified-signals-cryptographic-core-in-four-weeks-instead-of-years/) – The Decoder, 2026-11-11
2. [Introducing AlphaProof Code: a breakthrough in verifying complex software at depth](https://deepmind.google/blog/introducing-alphaproof-code/) – Google DeepMind, 2026-11-10
3. [Google DeepMind](https://google-deepmind.github.io/code-verification/) – Google DeepMind
4. [The Register](https://www.theregister.com/ai-and-ml/2026/11/10/google-deepmind-melds-humans-and-ai-agents-to-vet-signals-secure-messaging-techniques/5308625) – The Register

最后更新: 2026-11-11