CVE-2020-37268 — Rocq/Coq 的 Print Assumptions 通过 Parameter Inline 遗漏了不安全的全域检查

通过模块函子内联绕过证明审计——自 2020 年起未修复。

漏洞摘要

当某个定义通过模块类型中的 Parameter Inline 到达调用方时，Print Assumptions 无法报告该定义是在禁用全域检查的情况下构建的。函子应用会内联参数的主体，并丢弃记录 Unset Universe Checking 上下文的元数据，因此生成的常量不会显示出任何不安全操作的迹象。

因此，模块可以利用全域不一致性来证明 False，而 Print Assumptions 会将依赖该证明的结论报告为在全局上下文中封闭——没有公理，也没有可见的不安全标志。

coqchk 确实会拒绝生成的已编译 .vo 文件，但进程内的假设审计（Print Assumptions）无法捕获该问题。

用法

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

在存在漏洞的版本上（Rocq 8.11 – 9.2.0，以及所有带模块系统的 Coq 8.x），输出会确认 0 = 1 的证明，且 Print Assumptions 将其报告为封闭。

影响

任何将 Print Assumptions 作为唯一完整性检查的工作流都可能受到影响：

• 形式化验证的编译器（CompCert）
• 经过验证的操作系统内核（CertiKOS）
• 分离逻辑框架（Iris）
• 数学库（MathComp）
• 携带证明的代码，其中依赖项中的恶意 .v 文件可能引入能通过假设审计的不健全声明
• 经过验证的智能合约（ConCert）
• 任何未对编译输出常规运行 coqchk 的项目

根本原因

当模块类型声明 Parameter Inline 时，函子应用会将参数的主体内联到调用上下文中。这种内联会丢弃记录原始定义是在 Unset Universe Checking 下生成的元数据。因此，全域图会接受来自内联主体的不一致全域约束，而 Print Assumptions 看不到任何不安全上下文的痕迹。

该缺陷自 2020 年起一直处于开放状态（Coq issue #12155），并记录在项目的 dev/doc/critical-bugs.md 中。截至 Rocq 9.2.0，尚未合并任何修复。

评分

字段	值
CVE	CVE-2020-37268
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1（高）
CVSS 4.0	AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N — 6.8（中）
CWE	CWE-778 — 日志记录不足

受影响版本

产品	受影响	已修复
Coq	8.11 – 8.20	未修复
Rocq Prover	8.20 – 9.2.0	未修复

缓解措施

• 在生产环境中信任证明之前，对所有已编译的 .vo 文件运行 coqchk。coqchk 能捕获 Print Assumptions 遗漏的全域不一致性。
• 审计模块依赖项——该攻击需要一个在 Unset Universe Checking 下编译的、带有 Parameter Inline 的模块类型。
• 截至 Rocq 9.2.0，尚无已修补版本可用。

参考资料

缺陷报告	rocq-prover/rocq#12155
严重缺陷文档	dev/doc/critical-bugs.md
VulnCheck 公告	vulncheck.com

时间线

日期	事件
2020	Jason Gross 报告该缺陷（coq/coq#12155）
2020–2026	缺陷保持开放，记录于 critical-bugs.md
2026-08-24	VulnCheck 发布 CVE-2020-37268
2026-08-24	发布可通过 Docker 复现的 PoC

致谢

• 缺陷发现：Jason Gross
• PoC 打包：Jonathan Brossard（@endrazine）— MOABI / PSIRT.com