CVE-2026-72714 — Rocq 宇宙检查在模块关闭后状态失同步

通过模块作用域内的宇宙检查标志失同步，在无公理的情况下证明 0 = 1。

字段	值
缺陷报告	rocq-prover/rocq#22287
修复	无（截至 2026-08-16 该 issue 仍处于开放状态）
受影响	Rocq ≤ 9.2.0 / Coq 8.x（所有在 stdlib 中包含 Hurkens 的版本）
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-488（数据元素暴露给错误的会话）、CWE-20（输入验证不当）
CVE	CVE-2026-72714

漏洞摘要

Rocq Prover 的模块系统未能正确限定 Local Unset Universe Checking 标志的作用域。当在模块内使用该标志时，模块关闭后应将其恢复为之前的状态。然而，宇宙图（ugraph）维护着该标志自身的一份副本，在模块关闭时会与全局状态失去同步。

失同步之后：

Test Universe Checking 报告为开启（全局标志已恢复）
ugraph 仍将宇宙检查保持为关闭（其副本未被恢复）
因此内核会在不报错的情况下接受宇宙不一致的项

在宇宙检查实际被禁用的情况下，Hurkens 悖论便适用： TypeNeqSmallType.paradox 利用了当宇宙约束未被强制执行时， Type@{u} 与 Type@{v}（其中 u < v）可能被混淆这一事实，从而直接给出 False 的证明。

该利用：

不使用任何公理、插件或不安全特性
Print Assumptions 报告“Closed under the global context”
仅需要 Stdlib.Logic.Hurkens（标准库的一部分）
证明代码仅 6 行

用法

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

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

[*] Compiling ZeroEqOne.v ...
Universe Checking is on.
bad is defined
Closed under the global context
zero_eq_one is defined
Closed under the global context

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms (closed under the global context)

    Bug class:  Universe checking state desync (CWE-488)
    Root cause: ugraph retains stale Local Unset Universe Checking flag
    Bug report: https://github.com/rocq-prover/rocq/issues/22287

影响

任何信任 Rocq 内核校验证明的系统都会受到影响：

形式化验证软件：CompCert（经过验证的 C 编译器）、CertiKOS （经过验证的操作系统内核）、Iris（并发分离逻辑框架）、 MathComp——任何基于 Rocq 证明构建的安全论证，如果证明环境存在此标志不同步问题，都会失效。
携带证明的代码：依赖项中的恶意 .v 文件可能静默引入下游证明所依赖的不健全声明。
智能合约：使用 Rocq 进行经过验证的智能合约开发的项目（例如 ConCert）其安全保障可能被作废。

技术细节

根本原因

内核中的宇宙图（ugraph）包含其自己的 Universe Checking 标志副本。当模块使用 Local Unset Universe Checking 时，该标志会在全局状态和 ugraph 中同时被修改。当模块关闭时，全局状态会从模块保存的状态中恢复，但 ugraph 的副本未同步，导致宇宙检查实际上被禁用。

攻击流程

┌─────────────────────────────────────────────────────┐
│ 1. Universes u v.  Constraint u < v.                │
│    → Declare universes with strict ordering          │
├─────────────────────────────────────────────────────┤
│ 2. Module Off.                                       │
│      Local Unset Universe Checking.                  │
│    End Off.                                          │
│    → ugraph flag stays OFF after module closes        │
├─────────────────────────────────────────────────────┤
│ 3. Test Universe Checking.  → reports "on" (LIE)     │
├─────────────────────────────────────────────────────┤
│ 4. eapply TypeNeqSmallType.paradox; reflexivity.     │
│    → Kernel accepts universe-inconsistent proof       │
│    → False proved with no axioms                     │
├─────────────────────────────────────────────────────┤
│ 5. zero_eq_one : 0 = 1                              │
│    → Derived via exfalso                             │
└─────────────────────────────────────────────────────┘

与 Lean 4 内核缺陷的比较

方面	Rocq #22287（本缺陷）	Lean #14484	Lean #14576
证明助手	Rocq (Coq)	Lean 4	Lean 4
缺陷类别	模块系统中的状态不同步	推理缓存污染	通过投影导致的类型混淆
利用复杂度	6 行	约 20 行	约 50 行
宇宙/类型系统	宇宙检查被绕过	不透明 FVar 被接受	幻影参数逃逸
修复状态	未修复	已修复（PR #14498）	已修复（PR #14577）

致谢

缺陷发现：Gaëtan Gilbert（@SkySkimmer）
PoC 打包：Jonathan Brossard（@endrazine）

rocq-cve-poc-22287

最受欢迎