AREX Feed Article
Google 宣布用 Gemini 4 Carbon 把 Signal 协议代码验证到机器码层：逾 600 万行 Lean 证明，数年人工验证压缩到数周
北京时间 11 月 11 日凌晨，Google 与 Alphabet CEO Sundar Pichai 在 宣布：Google 团队把 Gemini 4 Carbon 用于一项安全挑战——对 Signal 协议的底层代码做数学证明。借助 Google DeepMind 同日发布的 框架，研究者引导 agent（自动执行任务的 AI 智能体）把协议验证到编译后的设备代码（compiled device code），用 Pichai 的话说，是「弥合真实漏洞藏身的缺口」。按公告口径，AI 生成了逾 600 万行经机器检验的 Lean 证明（Lean 是一种数学证明语言，每条证明都由其内核程序自动检验），把原本需要专家团队数年的人工验证压缩到数周，代码库仅约 1% 需要人工复核，其余由 Lean 自动检验；结果将向安全社区开源。
与帖子同期发布的一份给出更细的口径：agent 生成约 650 万行机器检验的 Lean 证明，建立在约 2.6 万行受信规格与 AArch64（ARM 64 位指令集架构）语义之上；验证对象是 libsignal——Signal 协议的参考实现——经原版 Rust 编译器编译出的 AArch64 Linux 机器码。论文称，这是首次有证明把协议级安全保证与一个被广泛部署、未经修改的密码协议实现连接起来。以上数字均为 Google 单方公告口径；由于全部规格与证明已经公开，任何人可以用 Lean 内核重新检验这些证明。Signal 协议是端到端加密通讯的事实标准，论文写道，除 Signal 应用本身，WhatsApp、Meta 的 Messenger 与 Google Messages 也部署了该协议的变体，保护着全球数十亿人的通讯。
图：AlphaProof Code 的工作流程——用户与 agent 起草并批准 Lean 规格（左上）；未经修改的 Rust 代码由标准编译器编译为 AArch64 可执行文件，在 Lean 的形式语义上运行（左下）；证明团队的产出必须通过 Lean 内核与 comparator 的守门检查（右侧）。橙色标出读者必须信任的部分，agent 输出一律视为不受信。（图源：Google DeepMind 论文）
流程拆解：人审规格，agent 团队写证明，Lean 内核做裁判
AlphaProof Code 是一个多 agent 框架，论文把工作拆成四步，分工方式类似一支研究团队：人与 AI 先共同决定「证明什么」，再由一组 agent 负责「怎么证」。第一步是规格撰写。博客称，研究者与多个模型协作，把 Signal 的安全目标翻译成形式化的数学规格，每一条都经人类专家评审；论文补充了细节：一个规格撰写 agent 在用户指导下，把文献中已有的 Signal 安全模型改写成 Lean 定理陈述，一批评审 agent 负责挑错，用户批准后，规格的 git commit 成为后续核对的基线。
规格在框架里是「受信」的：最终结果是否成立取决于规格是否写对，它无法被自动检验，一旦写弱，安全保证随之变弱。Signal 旧的形式化模型把初始握手与棘轮分开分析，而且早于 Signal 的后量子棘轮，不能直接使用；在人的引导下，agent 用几轮起草与评审把这些模型组合、扩展到实际部署的协议。论文同时承认，即便是大规模代码，人工评审也无法指望查出全部问题，因此框架还配有自动化测试：评审 agent 以怀疑立场出具审查意见，证明 agent 则构造额外定理做「空洞检测」，例如验证定理的前提确实可以同时成立。
第二步是把代码装进证明器。研究者为用户态 AArch64 Linux 写了一套形式语义：给定一个 ELF（Linux 可执行文件格式）二进制的字节，它描述程序所有可能的运行，覆盖 467 条指令和 31 个系统调用，共 7,578 行 Lean。受信的语义经过大规模测试，指令执行与两个独立参照——源自 QEMU 的 Unicorn 模拟器，以及由 Arm 官方规范衍生的 Sail 模型——逐条对跑。
第三步才是批量生成证明。博客称证明由 Gemini Carbon 驱动的 agent 完成；论文描述了队伍的构成：一支典型队伍有 40～80 个 agent，在一台机器上连续运行 24～72 小时。编排者分派任务但不亲自编辑文件，各队负责人汇总进度，architect 设计证明的分解方式，integrator 是唯一能向仓库提交代码的角色。agent 会在开工前先尝试反驳一个目标，避免在证不出来的子目标上浪费算力；它们不能修改规格，只能向一个从不接触证明过程的 critic agent 提交修订案，修订须有机器检验的反证或反例支撑、不得削弱安全性、且改动极小，触及受信假设的修订须由用户批准并记录理由。
第四步是守门。一个 gatekeeper agent 调用标准核对工具 comparator，只有当被证明的陈述及其依赖的全部定义与基线完全一致、证明只使用 Lean 标准公理、且 Lean 内核接受证明时，结果才算完成。论文说得很直白：证明本身不受信任，任何逻辑错误都会被 Lean 内核拒绝，因此结果的可靠性不依赖于写证明的 agent 是否可靠。人工所在的位置由此收窄：agent 会审计证明并标出需要人再看一眼的部分——论文称约占代码库的 1%；其余交由 Lean 自动检验，专家的判断因此集中在最要紧处。
为什么这一步以前做不到：seL4 花了 20 个人年
形式验证（formal verification）是安全保证的最高标准：先写下系统必须满足的性质，再数学地证明代码满足它们，一旦证成，凡违反该性质的 bug 与攻击一律被排除。博客称，密码协议支撑着从网银到网页浏览的几乎所有数字通讯，一个漏洞就能同时暴露数百万人，这也是专家花几十年对协议做形式化分析的原因。
但它出了名的贵。论文列举：被验证的 seL4 微内核花了 20 个人年，CompCert 验证 C 编译器花了 6 个人年，而且这些系统当初就是照着可验证性写的。对已经存在的工业级代码——比如经优化编译器产出的生产库——验证更难，因为证明者不能修改代码来迁就证明。更关键的是，博客指出大多数协议验证止步于设计层，而真实世界的漏洞往往藏在设计与实现之间的缺口里；跨越这道缺口会让证明的复杂度大幅上升。Pichai 在帖子里给出的判断是，这类能力「为从根本上把优势转向防御者打下基础」。
验证对象与边界：未改一行的 libsignal，编译到 AArch64
团队没有直接验证 Signal 手机应用，而是把未修改的 libsignal v0.105.4 与 spqr v1.6.0 crate 包进一个小的命令行工具 libsignal-cli，用原版 rustc 1.98.1 编译、以 musl（轻量级 C 标准库）静态链接成单个 AArch64 Linux 可执行文件。定理覆盖 init、send、recv 三种运行，从可执行文件的入口点一直跟到最后的 exit_group 系统调用，逐条指令地推理 musl 的 mallocng 内存分配器、protobuf（一种常用的数据序列化格式）序列化、MAC 校验，以及 PQXDH（Signal 的后量子握手）、Triple Ratchet（三棘轮）、SPQR（稀疏后量子棘轮）的状态机。keygen 不在验证范围内，各方密钥作为前提给定。另有 37 个挂钩例程以合约形式替代，其中包括 SHA-256 与 SHA-512 压缩、AES-256-CBC、X25519、Kyber1024、ML-KEM-768、libcrux 的 HMAC 等低层密码原语——这些原语的安全性无法在证明中给出，作为假设进入结果。
图：论文中的 Signal 会话示意。Bob 把 prekey bundle 上传到服务器，Alice 取回后独自完成 PQXDH 握手，把握手值连同第一条加密消息一起发出；此后双方进入 Triple Ratchet，每条消息都换用新密钥。（图源：Google DeepMind 论文）
证明分两条独立路线。符号模型（Dolev–Yao 模型，把密码原语当作理想化黑盒）下有十个定理：消息密钥的前向保密（当前状态被窃也不暴露更早的消息）与后攻陷安全（密钥被窃后，一次新鲜的密钥交换可恢复安全），握手认证与 KCI（利用泄露密钥冒充他人）抵抗力，以及即便量子攻击者日后破解 DH（Diffie–Hellman 密钥交换）仍然成立的握手保密性，并且任何一次运行都不会故障或发散。计算模型（用底层假设的难度限制现实攻击者的成功概率）下则证明了消息的机密性与真实性——连同前向保密与后攻陷安全——针对 PQXDH 与 Triple Ratchet 的组合，以攻击者优势的具体上界表述。边界同样明确：符号模型未覆盖计算保密性与 SPQR 的后量子自愈；计算模型未覆盖量子攻击者、多设备状态，以及多会话长期运行的场景——那种情况下安全界会退化为空话。
被验证的还有 libsignal 里那些容易藏 bug 的机制：大量可变会话状态、为乱序消息保存的密钥、被拆进普通消息分片的 ML-KEM 数据、protobuf 序列化，以及为延迟消息保留的归档会话。定理的对象是编译后的代码，这些机制因此都在覆盖范围内。与手机用户的关联是间接的：论文称 Signal 的 Android 与 iOS 应用运行同一份 libsignal Rust 代码，几乎所有 Android 手机与全部 iPhone 都用 AArch64，定理可以延续到这些环境——前提是相信它们保持了 libsignal-cli 二进制所演练的协议行为。语义本身不建模线程、信号、vDSO（Linux 的一种内核加速机制）与动态链接，依赖这些机制的程序无法用这套方法验证；libsignal-cli 恰好是单线程、静态链接的。群聊（两方以上会话）被论文列为未来工作。
反向检验：把两个已修复的漏洞放回代码
一份证明的价值取决于规格能否抓住真实错误。团队把两个此前已修复的 libsignal 真实漏洞重新引入一个隔离版本的代码，两种情形下系统都给出了机器检验的证明，表明带漏洞的二进制违反安全定理。论文举出其中之一的细节：一条只能在归档会话下解密成功的 prekey 消息，曾让 libsignal 照样存下新会话的状态，包括签名 prekey 密钥的一份拷贝；重新引入该漏洞后，产出的二进制被证明违反符号安全定理。
规格测试还借用了软件工程的变异测试思路：agent 往代码里加入自然形态的 bug，比如让 Signal 跳过密文的 MAC 校验，然后证明安全定理在变异后的二进制上为假。博客称，这项检验是为了确认 AlphaProof Code 分得清正确代码与带漏洞的代码。
Signal CTO 与论文作者的回应
Signal 首席技术官 Ehren Kret 在 DeepMind 博客中说：「此前的形式验证工作必然只能覆盖更小的范围，而新方法使验证规模得以显著扩展。过去，验证生产代码是否严格符合其密码学设计需要大量人工，因此用 AI agent 把真实代码自动翻译成有效的 Lean 定理是一项重大突破。随着 AI 驱动的安全威胁增长，对核心 Signal 协议实现做严格验证，让我们对代码兑现隐私承诺更有信心。」博客的致谢部分提到，Signal 的 Rolfe Schmidt、Michael Rosenberg 与 Ehren Kret 对方法论提供了反馈。
论文一作、Google DeepMind 研究科学家 Swarat Chaudhuri（兼任 UT Austin 教授）在北京时间 11 月 10 日晚间回顾：他 20 多年前读研究生时入行，被 Dijkstra 等先驱说服，相信编程应当有数学定理背书；那时只能在两个选项之间取舍——要么用能扩展但只能证明浅层性质的自动分析算法，要么做耗时数十年的专家级人工深度验证。「得益于数学推理 AI 的进展，我们不必再做这种选择了。」他写道，2026 年 10 月的四个多星期里，AlphaProof Code agent 生成逾 600 万行机器检验的 Lean 证明，把 Signal 协议核心的计算与符号安全性质一路证到 ARM 机器码层。
他也说明了这项工作的边界：「当然这只是第一步，因为我们的目标不折不扣是验证世界的软件基础设施。」「证明如今大部分已自动化，但人类专家需要决定借助 AI 证明什么。」他说团队已放出全部 Lean 规格与证明，计划与开源社区一起改进，并邀请在写关键软件的人找他们聊聊。
开源仓库已上线：复核路径与收窄后的信任边界
开源承诺当日兑现。 仓库 11 月 10 日已可访问，包含全部规格、证明与构建脚本；Google 代码按 Apache 2.0 许可发布，第三方的 libsignal 保留其 AGPL-3.0-only 许可，仓库同时注明「这不是 Google 官方产品」。
复核路径是具体的。装好钉死版本的 Lean 4.34.0 工具链与 Rust 1.98.1，拉取预编译 Mathlib（Lean 的社区数学库）缓存后执行 lake build，README 提示需要数小时、峰值内存约 15～34 GiB。要独立核对头条定理，可以再跑 comparator：它检查定理陈述及其全部传递依赖的定义与预先留存的规格副本完全一致，只承认 propext、Quot.sound、Classical.choice 三条标准公理，并从 lean4export 的输出在全新 Lean 内核里重放证明。
Google 在博客里给出了这项工作的延伸方向：让企业、政府与关键基础设施的软件也能获得「精英级安全保证」，并称验证 Signal 核心密码学为保护医疗设备固件、电网软件等其他关键系统打下基础；把形式验证与 CodeMender 这类自动防御 agent 搭配，可以跟上现代网络威胁的速度与规模。博客同时承认，扩展这些技术需要持续的研究。
按论文口径，需要人类读与信任的，收敛到约 1.8 万行规格与定理陈述、约 8 千行 AArch64 语义与符号名，加上 Lean 内核本身与密码原语的理想化假设，合计约 2.6 万行受信代码；需要人工过目的，则是 agent 从数百万行证明里标出的那 1%。