当证明器学会说谎：Lean与Rocq同周曝出七个能推出0=1的内核洞

原创

赤霄攻防实验室
赤霄攻防实验室

赤霄攻防实验室

2026年10月29日 09:26
河北

去阅读

2026 年 10 月 26 日，安全研究员 Jonathan Brossard（圈名 endrazine）在 oss-security 邮件列表做了一次集中披露：七个 CVE，两个打 Lean 4 内核，五个打 Rocq（也就是改名后的 Coq）。这批洞最瘆人的地方不是数量，而是所有 PoC 跑完的输出都一模一样：zero\_eq\_one : 0 = 1，下面跟着一行 -- no axioms。零等于一，不带任何公理，还通过了最高强度（--trust=0）的内核检查。说白了，两台世界上最较真的数学机器，被同一类手法骗着给假定理盖了章。

先说人话：形式化验证是在干什么

你平时做的测试和代码审计，说到底是抽样：跑一亿个输入没崩，不代表第一亿零一个不崩。形式化验证走的是另一条路：把程序或协议的性质写成数学命题，再把「为什么成立」展开成证明，交给机器逐项检查每一步推理是否合规。检查证明的那一小块代码叫内核（kernel），它是整个体系里唯一需要信任的东西，行话叫 de Bruijn 准则：证明可以来自任何地方，哪怕是你完全不信任的 AI 或者陌生人，只要内核检查通过，定理就成立。这套逻辑漂亮得很，前提是内核自己不撒谎。这一次，它撒谎了。

站在信任链顶端的两台机器

Rocq 前身是法国 INRIA 的 Coq，2024 年改名。它最有名的产出是 CompCert，一个每一步都经过证明的 C 编译器，民航软件认证圈把它当标杆；Fiat Crypto 项目用 Rocq 生成椭圆曲线运算代码，这些代码进了 BoringSSL 和 OpenSSL，你手机里的 TLS 握手可能正跑在「被证明正确」的有限域运算上。Lean 4 是后起之秀，由 Lean FRO 维护，百万行级的 Mathlib 数学库是它的门面，Google DeepMind 的 AlphaProof 用 Lean 在 2024 年国际数学奥赛拿了银牌。补一句免得有人抬杠：seL4 微内核用的是 Isabelle，不属于这俩，但信任逻辑一模一样。在 Common Criteria、DO-178C 这类认证框架里，形式化验证工具本身就是信任链的根。根上有洞，上面的证书、编译产物、密码学实现全部连坐。

七个洞，每一种都能推出 False

按编号过一遍，每个我用几句人话讲清它打破了什么保证。

CVE-2026-72844（Lean）：内核不检查 projection 表达式里写的 structure 名和被投影值的类型是否匹配，嵌套归纳类型的参数检查也缺席。元程序注册一个类型错乱的嵌套归纳类型，构造子把投影用在无关类型上，类型混淆直接换来一个零公理的 False 证明，PoC 还顺手用哈希和深度碰撞打穿了内核缓存。v4.32.2 已修。

CVE-2026-72711（Lean）：add\_opaque 路径漏掉了定义和定理路径都有的闭包检查。攻击分两步：先让类型检查器的推理缓存记住一个类型为 False 的临时局部变量，再恢复上下文后提交引用这个已越界变量的 opaque 声明，缓存抢在上下文检查之前作答，False 混进环境。v4.32.2 已修。

CVE-2026-72703（Rocq）：guard checker 判断递归定义会不会终止时，只看自递归调用。嵌套互递归的 fixpoint 只要没人调用自己，参数全被判为 uniform，跨调用导致的参数增长没人管，不终止的定义被当作结构递归收下，于是一个自然数等于它自己的后继。Coq 8.20 引入，Rocq 9.2.0 修复。

CVE-2026-72704（Rocq）：沿类型等式做 transport 之后，guard checker 不复查递归树，第二个 fixpoint 无条件继承这份被改过的记录，非递减调用被放行。修复 PR 至今没合并，洞还开着。

CVE-2026-72705（Rocq）：guard checker 不追踪经参数传递的高阶递归调用。把递归函数自己当参数喂给另一个 fixpoint，后者把它应用到非子项上，于是一个类型在定义上等于自己的否定，自应用即爆。Rocq 9.2.0 修复。

CVE-2026-72714（Rocq）：在模块里关闭宇宙检查，模块收尾时全局标志恢复了，宇宙图自留的那份副本却还关着。命令查询说检查已开启，内核照收不一致的项，Hurkens 悖论把 False 递出来。截至目前没有任何修复。

CVE-2020-37268（Rocq/Coq）：Print Assumptions 是「这条定理到底靠没靠不安全操作」的标准审计命令，但定义经 Parameter Inline 内联后，它在关闭宇宙检查时构造的痕迹被抹掉，审计直接放行。独立检查器 coqchk 能拒收这种编译产物，项目自己把它记在 critical-bugs.md 的未修复清单里。

攻击者视角：这就是为供应链投毒定制的

注意这七个洞的共性：利用时全都不需要 sorry、unsafeCast、debug.skipKernelTC 这类「自首式」开关，全部走内核正常检查路径，全部能让 Print Assumptions 报告「不依赖任何公理」。两个 Lean 漏洞的利用条件只是在进程里跑元程序，构建一个项目、import 一个恶意 Lake 依赖就够了。攻击剧本我都能替人写好：往一个流行数学库风格的依赖里埋伪造定理，review 的人打开文件看到的是规规矩矩的证明项，内核点头，审计干净，下游把「已被证明安全」的代码打进编译器、密码学库。CVSS 给了 6.3（medium），理由是本地向量和需要用户交互，讲真，这个分数完全没算「下游完整性」这笔账。AI 时代还有个更阴的玩法：让大模型批量生成证明库，人类根本读不完，夹带私货的成本趋近于零。

修复状态，说白了：三个还开着

Lean 4.32.2 修掉了两个内核洞，别犹豫，直接升。Rocq 9.2.0 修了 72703 和 72705。剩下三个：72704 的修复躺在 PR 里等合并；72714 无修复；37268 被官方文档记录在案，唯一可靠的缓解是用独立检查器 coqchk 复核编译产物，这类检查器不与内核共享状态，适合直接进 CI。Lean 生态同理，nanoda 这类第三方检查器可以做交叉复核，这次披露里明说了独立检查器也要用最新版，因为旧版自己也有可被链式利用的洞。

为什么你该把这事记在心上

我们这行的隐秘共识正在成形：AI 写代码的速度会彻底压倒人类 review 的速度，最后能兜底的可能是形式化验证，先让机器证明代码合规，再决定要不要看代码本身。AWS 的自动推理团队在押注，AI for Math 的钱在涌入。可如果证明器自己能被骗，「最后一道防线」就成了心理安慰。我的建议很直白：把证明检查器当攻击面管理，对内核做 fuzz；把 coqchk、nanoda 这类独立复核器写进流水线；把验证工具链当成和密码学库同级的关键供应链资产来盘点。信任链的根也是软件，是软件就有洞。这一次它只证明了个 0 = 1，下一次未必这么好发现。