CVE-2026-72704 — Rocq 守卫检查器在传输后信任被破坏的递归树

通过守卫检查器不动点递归树破坏，从一致公理证明 0 = 1。

字段	值
缺陷报告	rocq-prover/rocq#22024
修复	PR #22027（开放中）
受影响	Rocq ≤ 9.2.0 / Coq 8.x（所有带守卫检查器的版本）
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-670（始终错误的控制流实现）
CVE	CVE-2026-72704

漏洞摘要

Rocq Prover 的守卫检查器（不动点的终止性检查器）在归纳类型参数通过传输（rew）被修改时，未能重新检查这些参数的递归树表示。一个不动点可以静默地破坏归纳类型类型参数的递归树，而调用第一个不动点的第二个不动点将信任被破坏的递归树而不进行验证，从而接受一个非终止定义作为结构递减。

该利用使用两个与 CIC 一致的公理——它们是 univalence 公理的直接推论（交换 0↔1 的双射在 Type 中给出路径 nat = nat，沿该路径传输将 0 送到 1）。健全的守卫检查器不得从一致公理推导出 False。

该利用：

仅使用两个一致公理（univalence 的推论）
Print Assumptions 仅报告这两个公理——没有 False，没有 sorry
没有插件、不安全特性或宇宙操作
守卫检查器是不健全性的唯一来源

用法

docker build -t rocq-cve-poc-22024 .
docker run --rm rocq-cve-poc-22024

在存在漏洞的 Rocq 版本上的预期输出：

[*] Compiling ZeroEqOne.v with rocq compile ...

zero_eq_one is defined
Axioms:
e : nat = nat
e1 : rew [fun T : Type => T] e in 0 = 1

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Axioms used: e (nat = nat), e1 (transport sends 0 to 1)
    These axioms are consistent (consequences of univalence).
    A sound guard checker must not derive False from them.

    Bug class:  Guard checker rectree corruption (CWE-670)
    Root cause: fixpoints can alter rectrees via transport; nested
                fixpoints trust the corrupted rectree without recheck
    Bug report: https://github.com/rocq-prover/rocq/issues/22024

影响

任何信任 Rocq 内核检查证明并且使用与 univalence 一致的公理的系统都会受到影响：

HoTT 开发：任何使用 univalence 公理（或命题外延性，它可能触发同一类缺陷）的 Rocq 项目，其经过 guard 检查的 fixpoint 可能会在非终止的情况下被静默接受。
形式化验证软件：CompCert、CertiKOS、Iris，以及任何添加了与 CIC 一致的自定义公理的项目，如果 guard 检查器是唯一的终止性保证，就会面临风险。
携带证明的代码：恶意依赖项可以引入这两个公理和被破坏的 fixpoint，然后在下游使用 False。

技术细节

Guard 检查器缺陷

Rocq 的 guard 检查器通过构建一棵 rectree 来验证 fixpoint 是否在结构上递减——rectree 是一棵树，用于跟踪在每次递归调用时递归参数的哪些子项是可用的。该缺陷是一个两步失败：

Rectree 损坏：weird 是作用于 Box A 的 fixpoint，它在 wrap 分支中对递归参数应用了 rew [Box] e（沿 e : A = A 进行 transport）。guard 检查器接受这一点，因为 transport 保持了归纳类型 Box，但参数 A 的 rectree 被静默改变了——经过 transport 之后，guard 检查器的内部模型不再准确跟踪流经 A 的值。
未检查的信任：loop 调用 weird loop e (wrap _ (box _ n))。guard 检查器验证了 loop 自身的递归调用，但信任了嵌套调用中 weird 的 rectree。由于 weird 的 rectree 已被 transport 破坏，guard 检查器错误地得出结论：loop 在结构上递减。

矛盾

在 guard 检查器被欺骗的情况下，loop 尽管是非终止的，却被接受了。随后该证明表明：

loop 1 = S (loop 1)

通过展开 loop 和 weird，并使用 e1 来表明 transport 将 box nat 0 发送到 box nat 1，而后者又反馈回 loop。由于 ∀ n, n ≠ S n 可通过归纳法证明，loop 1 = S (loop 1) 可推出 False，并由此得到 0 = 1。

为什么这些公理是一致的

这两条公理：

e  : nat = nat :> Type
e1 : rew [fun T => T] e in 0 = 1

是 univalence 公理的推论。在 univalence 下，任何双射 f : nat → nat 都会在 Type 中给出一个路径 nat = nat，而沿该路径的 transport 作用就如同 f。双射 swap01 将 0↦1、1↦0，且对 n≥2 有 n↦n，正是这样一个双射，其中 swap01 0 = 1 见证了 e1。

已知 univalence 与 CIC 相容（已由立方类型论模型验证）。因此这些公理不可能是矛盾的来源——守卫检查器才是。

与其他 PoC 的比较

方面	Rocq #22024（本 bug）	Rocq #22287	Lean #14484
Bug 类别	守卫检查器 rectree 损坏	宇宙检查状态失步	推断缓存污染
所需公理	2（与 univalence 相容）	无	无
利用复杂度	约 30 行	6 行	约 20 行
组件	守卫检查器（fixpoint）	模块系统（ugraph 标志）	类型检查器（不透明声明）
修复状态	PR #22027（开放）	开放	已修复（PR #14498）

致谢

Bug 发现：Yann Leray (@yannl35133)
PoC 打包：Jonathan Brossard (@endrazine)

rocq-cve-poc-22024

最受欢迎