CVE-2020-37268 — Rocq/Coq Print Assumptions Omits Unsafe Universe Checking via Parameter Inline

Bypassing the proof audit via module functor inlining — unfixed since 2020.

Vulnerability Summary

Print Assumptions fails to report that a definition was built with universe checking disabled when that definition reaches the caller through Parameter Inline in a module type. Functor application inlines the parameter's body and drops the record of the Unset Universe Checking context, so the resulting constant shows no sign of the unsafe operation.

A module can therefore use a universe inconsistency to prove False, and Print Assumptions reports the dependent proof as closed under the global context — no axioms, no unsafe flags visible.

coqchk does reject the resulting compiled .vo file, but the in-process assumption audit (Print Assumptions) does not catch the issue.

Usage

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

On a vulnerable version (Rocq 8.11 – 9.2.0, and all Coq 8.x with the module system), the output confirms the proof of 0 = 1 with Print Assumptions reporting it as closed.

Impact

Any workflow that relies on Print Assumptions as the sole integrity check may be affected:

• Formally verified compilers (CompCert)
• Verified OS kernels (CertiKOS)
• Separation logic frameworks (Iris)
• Mathematical libraries (MathComp)
• Proof-carrying code where a malicious .v file in a dependency could introduce unsound declarations that pass assumption auditing
• Verified smart contracts (ConCert)
• Any project not routinely running coqchk on compiled output

Root Cause

When a module type declares Parameter Inline, functor application inlines the parameter's body into the calling context. This inlining discards the metadata recording that the original definition was produced under Unset Universe Checking. The universe graph therefore accepts inconsistent universe constraints from the inlined body, and Print Assumptions sees no trace of the unsafe context.

The bug has been open since 2020 (Coq issue #12155) and is documented in the project's dev/doc/critical-bugs.md. No fix has been merged as of Rocq 9.2.0.

Scoring

Field	Value
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 (High)
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 (Medium)
CWE	CWE-778 — Insufficient Logging

Affected Versions

Product	Affected	Fixed
Coq	8.11 – 8.20	Unfixed
Rocq Prover	8.20 – 9.2.0	Unfixed

Mitigation

• Run coqchk on all compiled .vo files before trusting proofs in production. coqchk catches the universe inconsistency that Print Assumptions misses.
• Audit module dependencies — the attack requires a module type with Parameter Inline that was compiled under Unset Universe Checking.
• No patched version is available as of Rocq 9.2.0.

References

Bug report	rocq-prover/rocq#12155
Critical bugs doc	dev/doc/critical-bugs.md
VulnCheck advisory	vulncheck.com

Timeline

Date	Event
2020	Bug reported by Jason Gross (coq/coq#12155)
2020–2026	Bug remains open, documented in critical-bugs.md
2026-08-24	CVE-2020-37268 published by VulnCheck
2026-08-24	Docker-reproducible PoC published

Credit

• Bug discovery: Jason Gross
• PoC packaging: Jonathan Brossard (@endrazine) — MOABI / PSIRT.com