AlphaProof Code 证明了 Signal 的什么：从二进制到信任边界
650 万行 Lean 证明覆盖的是指定构建的 libsignal 协议代码，不是整个 Signal App。逐层看证明对象、安全性质、可信定义和未覆盖场景。
Google DeepMind 11 月 10 日宣布用 AlphaProof Code 把 Signal 核心密码协议的部分安全性质证明到了指定构建的机器码。这不是「整个 Signal App 已被证明没有漏洞」：论文验证的是基于特定版本 libsignal 编出的 AArch64 Linux 命令行程序；结论还依赖人审核的规格、密码原语契约以及实验环境。650 万行是机器检查过的 Lean 证明代码，不是 Signal 应用源码的体量，也不是安全保证的计量单位。（发布公告；原始论文摘要与 §4）
这个限定并不削弱成果。恰恰相反，只有先说清它验证了哪一层，才能看到突破在哪里：过去常见的是证明协议在抽象模型中成立，这一次研究团队把协议性质与未为证明而改写的生产库代码所编译出的特定可执行文件连了起来。问题从「设计上应该安全」推进到了「这些机器指令在给定前提下符合该安全模型」。它离完整产品依然有距离，但这一段距离过去恰是很难跨过的部分。
从一条离线消息说起：PQXDH 与 Triple Ratchet 在保护什么
设想 Alice 要给暂时离线的 Bob 发第一条消息。Bob 事先把公开的身份密钥和预密钥材料交给服务器；Alice 取到材料后，不必等 Bob 上线，就能建立共享秘密并发出首条加密消息。这一步叫 PQXDH。Bob 收到后，两人的后续消息再由棘轮机制不断更新密钥。这里的 Alice 和 Bob 是协议规范与论文用来说明机制的角色，不是真实用户案例。（Signal PQXDH 规范 §1、§3；原始论文 §3、Figure 2）
两段机制要回答的威胁不同：握手须防止旁观网络的人获知会话秘密；消息链须让之后偷到当前状态的人不能顺藤摸瓜还原所有过去消息，并在双方完成某些新的密钥交换后限制继续窃听。术语分别是前向保密与泄露后安全性。Signal 的 Double Ratchet / Triple Ratchet 规范解释了每条消息换钥、跳过消息的密钥保存和后量子棘轮如何组合，但规范列出设计目标，不等于任何实现自动满足目标。真正麻烦的地方是落地：会话状态、序列化、乱序消息、历史会话与密钥销毁都必须和协议图上的箭头一致。
例如 Bob 收到一条先前延迟的消息时，代码需要在保存过的消息密钥里找对应项。若某个路径意外保存了本该消失的秘密，协议白板上正确的前向保密性质不会替实现补洞。论文特别提到，libsignal 还处理归档的旧会话和拆分传输的后量子棘轮材料；这些细节正是只验证漂亮的协议图容易遗漏的地方。问题因此具体起来：研究团队究竟证明了协议，还是证明了会在设备上执行的代码？
这次跨过了哪一层：从模型落到指定的机器码
论文给出了可核对的验证对象：libsignal-protocol v0.105.4、spqr v1.6.0 的未改动 Rust crate，被包装进研究用的小型 libsignal-cli；用标准 rustc 1.98.1 编译、以 musl 静态链接，得到 AArch64 Linux 可执行文件。命令行封装让每次执行完成一次 init（建会话）、send（加密）或 recv（解密）；证明覆盖这三种操作。生成初始密钥的 keygen 不在证明内，双方密钥作为场景的初始条件给出。（原始论文 §4 “Setup for Verification”）
为什么强调机器码？如果只证明 Rust 源码的一个抽象解释，还要额外相信编译器把这个解释忠实翻译了；如果只证明数学协议，还要额外相信源码把协议实现对了。研究团队把该可执行文件的字节与 AArch64 指令语义装入 Lean，目标是把程序执行和安全模型中的事件联系起来。论文明确说，这一验证不把 Rust 编译器放进可信基：只要某个编译错误让已经形式化的性质失效，针对编译产物的定理就不会成立。注意后半句——没有被形式化的性质，仍不在这句话覆盖的范围内。（原始论文 Figure 1、§4、§5.3）
这也不是把手机上的每条指令全部放进证明器。研究对象是一个单线程、静态链接的 CLI 程序，模拟固定时钟与一组文件状态；部分底层函数由可信契约替代。论文列出 39 个这类 hooked routines，包括密码学底层、少量内存与字符串例程、写文件和标准输出的函数。证明会跟踪 CLI 的文件读写、会话状态以及大量程序逻辑，但不会由此证明被替代的真实函数本身正确。把「机器码级」听成「每个外部函数和操作系统都验证了」，会把这项工作讲得比论文更大。
研究团队认为，相同 Rust 库也用于移动端，因此结果对 Android 和 iOS 有参考价值；他们随即给出条件：要把结论搬到不同编译选项、链接方式和操作系统接口的环境，还得相信这些差异不会改变论文所验证的协议行为。这是迁移论证所需的额外假设，不是「移动 App 二进制已经验证」。（原始论文 §4 末段）
650 万行证明对应哪些安全性质
论文的数字需要先拆开。约 650 万行指机器检查过的 Lean proof；仓库接近 700 万行，包含注释和空行。论文称被验证的 libsignal 机器码约为 560 KB，约 14 万条 AArch64 指令。把 650 万拿来和 App 的源码行数直接相比，既换了单位，也换了对象。（原始论文 §7 “Scale”）
证明结果也不是一句「Signal 安全」所能概括。研究团队并行使用两类密码协议分析模型：符号模型把密码操作当作理想黑箱，讨论给定攻击者能力下每条执行轨迹应满足什么；计算模型承认真实密码学以概率和计算难度刻画，给经典攻击者在指定游戏中成功的优势上界。两套模型回答互补但不同的问题，不能把第一套对某种量子场景的结论和第二套对经典攻击者的概率上界拼成一个「全面抗量子」总保证。（原始论文 Table 1、§5）
先用一句日常语言分清两者：符号模型看的是「假定密码工具可靠，程序可能走出的路径是否安全」；计算模型问的是「面对算力有限的攻击者，突破安全目标的概率能被约束到多低」。两者都需要前提，但前提和答案的表达方式不同。
| 研究视角 | 论文在限定场景中证明什么 | 特别不能据此推出什么 |
|---|---|---|
| 符号模型 | 消息密钥的前向保密、泄露后安全性，握手认证等性质；在特定未来量子攻击者情形下的握手保密 | 不给真实字节的计算保密概率；不证明 SPQR 带来的后量子「愈合」；不覆盖全部会话情形 |
| 计算模型 | PQXDH 与 Triple Ratchet 组合的消息保密及认证，并对经典攻击者优势给出条件化上界 | 不保证对量子攻击者成立；不覆盖多设备与若干首次消息场景；上界在论文所列较大规模下会变空洞 |
表格依据论文的 Table 1 与限制章节。关键区分是：握手的后量子保密，不等于消息棘轮的后量子泄露后恢复。 符号模型对棘轮只证明 Triple Ratchet 不弱于 Double Ratchet，没有证明 SPQR 所带来的后量子恢复；计算模型则面向经典攻击者。具体的密钥选择与攻击者设定见论文 §5.1.6、§5.2.5，不能跨模型借用结论。
这些限制不是研究成果的失败报告，而是定理的一部分。密码证明从来不是对一切想象得到的攻击者都成立；它说明的是，在一组明示条件下，某类攻击无法突破某个明示性质。可供工程团队借鉴的，正是把条件摆在桌面上的写法。反过来，一项性质没有出现在表中，也不等于它一定有漏洞；只是当前证明没有给出那项担保。
AI 写证明之后，人为什么还要审可信定义
最容易误解的工作分工是「AI 写了几百万行，Lean 验了，所以人可以退出」。Lean 内核检查的是一份形式命题有没有有效证明；它不会替团队判断这个命题是不是用户真正需要的安全目标，也不会自动知道环境契约是否忠实描述真实代码。论文说得很直接：人决定证明范围、挑选参考模型、审定定理陈述与定义，并裁决可信假设变更。研究团队报告，主要精力花在写规格，而非写证明。（原始论文 §2.1、§7）
想象给一个程序写出「如果输入永远为空，输出就安全」的定理。它或许可以被正确证明，却几乎无法保护真实工作负载；若前提互相矛盾，结论甚至可能空洞成立。这不是说 AlphaProof Code 的论文犯了这种错误——恰好相反，作者描述了对应防线：人审规格；让代理尝试证明前提可满足；针对变异代码和历史错误检查规格是否足够有力。由此也能明白，为什么证明的总行数并不是衡量保证强弱的捷径。（原始论文 §2.1 “Specification Writing”）
团队还防止证明代理在过程中偷偷换题。被批准的规格放在独立留存的基线；gatekeeper 的 comparator 会核对最终定理以及其传递依赖的定义是否仍与批准版本相同，再由 Lean kernel 检查证明。论文称证明产物不能靠代理自己宣布完成；更改可信假设须走审查与批准。这个门禁的意义不是「代理永远不会出错」，而是让代理写出的错误证明无法悄悄改写目标后通过。（原始论文 §2.4 “Gatekeeping”）
论文估计，真正需要读者审阅并信任的定义约 1.8 万行仓库代码 + 约 8000 行 AArch64 语义。这是约 2.6 万行的可信内容，不是「机器自动验证掉了所有信任」。其中包括符号模型、计算模型、安全游戏、事件层、机器语义、外部函数契约和密码原语假设；还要信任 Lean 的内核、可复现构建和抽取符号名等环节。编译器不在这份名单里，这很有价值；名单本身也不能消失。（原始论文 §5.3、§7 “Scale”）
把两处旧漏洞放回去，证明会怎样
一个容易让读者理解规格强度的问题是：若把过去已经修好的错误重新塞回程序，这套定义会不会仍宣称它安全？论文做了这一检验。研究者将两处历史上已修复的 libsignal 错误分别倒应用到所用版本，重编译变异二进制，随后给出由 Lean 检查的反证：变异版本不满足相关的符号安全定理。（原始论文 §6 “Finding Historical Bugs”）
一处涉及处理解密失败的预密钥消息时旧会话的试解密路径，可能把新的、未确认会话状态和秘密存下；另一处涉及发起方 X25519 临时公钥（base key）的有效性检查，重放并更改编码可使程序错误接受另一会话。论文给出对应的具体执行见证，并沿变异二进制的 AArch64 语义证明这些轨迹与其安全模型不相容。这比「跑一次测试出现异常」更有力：它检验了规格能否排除两种特定的现实错误路径。（原始论文 §6，两项历史错误说明）
但也要把结论止在这里。论文没有说今天的线上 Signal 被发现了两个新漏洞；错误早已修复，实验针对人工回退修复的隔离版本。反证针对的是符号定理，不等于为所有尚未知晓的漏洞建立了自动探测覆盖率，更不是攻击者永远找不到定理之外的缺陷。这种变异验证回答的是「规格有没有牙齿」，不是「所有牙缝都已检查」。
哪些东西还在证明边界之外
现在可以把「完整 App 无漏洞」拆成几个具体问题，而不是一句笼统的保留意见。
首先是执行对象。论文证明的是它构建的 libsignal-cli 可执行文件，不是移动端完整应用；应用 UI、消息同步、推送通知、设备间状态与各自的打包版本不因此自动获得同一个定理。研究用 CLI 的运行环境被固定为单线程、静态链接、当前目录文件、固定时钟和指定输入输出与内存条件；机器语义不建模线程、信号、动态链接等。研究者验证了这些场景中的大量机器指令，但换一个构建和运行环境，不能简单复用「已证」标签。（原始论文 §2.2、§4.1、§5.2.5）
其次是被替换的函数与密码假设。若底层密码例程未按契约工作，或随机性、身份密钥信任等前提不成立，Lean 检查过主程序证明这件事本身也不能挽救被破坏的前提。论文没有把所有密码原语从硬件到数学再证明一遍，也没有验证被 hook 的真实实现。符号模型将其理想化；计算模型写明若干计算难度和原语安全假设。这与软件里通过接口约定组合模块一样：接口使推理可扩展，也明确指出需要另行审计的模块。（原始论文 §4、§5.2.4、§5.3）
最后是威胁模型的边角。论文的符号证明要求双方预置对方身份密钥、限制预密钥和会话结构，不处理旁路泄漏与内存中其他秘密，且说明对某种精确重放的前向保密损失不作排除。计算证明不涵盖多设备状态，限制某些未晋升会话的首次消息和若干腐化时点；其上界在论文列出的较大规模场景会失去实质约束。两者对首次信任路径的处理也不同：不能把一套模型的假设悄悄换成另一套的结论。（原始论文 §5.1.6、§5.2.5）
这三层边界给出的工程判断相当朴素：证明成立的对象、性质和前提必须同时写在同一张纸上。单独说「机器码已验证」会漏掉哪些机器码；单独说「前向保密已证明」会漏掉哪种攻击者、哪个时间点和哪个会话范围。做安全采购或审计时，不能要求供应商贴一张这篇论文的链接便算过关。应要求其提供自己的证据，逐项回答：
- 验证了哪个构建？ 版本、二进制与目标设备是否明确，实际部署与被证明对象有哪些差异？
- 保证了什么？ 已证明的性质、攻击者能力和未覆盖场景，是否对应团队真正关心的风险？
- 还需要信任谁？ 外部函数契约、生产环境假设与独立审计证据，是否足以支撑这些保证？
不能提供这些材料，就不应把本篇研究当成该供应商或其产品的安全认证。
新的分工：证明可以扩张，规格和信任不能外包
这项研究没有给出通用验证服务的报价或交期，团队不能拿它的投入直接估算自己的项目预算。论文描述的投入是五位研究者并行工作四周，持续指导代理团队；典型证明团队有数十个代理，一次干活可能连续运行一到三天，干净构建证明可耗费数小时。作者称无人手写证明代码，但不等于无人审核、零计算成本或一键商业化可用。公告说开放形式化验证产物供社区使用；它没有给出面向普通团队的通用产品价格或立即可用的服务承诺。（原始论文 §7 “AlphaProof Code in Practice”；发布公告）
真正值得带走的是分工变化：过去证明的人工量可能使人连尝试都不敢；现在代理可以在被固定、可核查的目标之下写出大规模证明。于是最稀缺的工作前移了——选哪些性质、哪些环境假设值得信、怎样证明目标不空洞，以及如何检查实际部署没有越过证明边界。对 Signal 这项研究，结论是指定 libsignal 构建的核心协议行为获得了罕见的机器码级条件化保证。下次看到类似的「AI 证明软件安全」，先找其定理对象和可信基；那比数一数代理写了多少行更接近安全事实。