Rocq Print Assumptions hides unsafe universe checks
Original title: CVE-2020-37268: Rocq/Coq Print Assumptions omits unsafe universe checking inlined through Parameter Inline (0 = 1 demonstrated) — unfixed since 2020
Inlining a Parameter Inline body drops metadata that the definition was made with universe checking unset, and no fix is stated.
Jonathan Brossard described CVE-2020-37268, a soundness-audit bypass in the Rocq (formerly Coq) module system. A proof of False can be built that Print Assumptions reports as closed, with no axioms or unsafe flags visible. When a module type uses Parameter Inline and functor application inlines the body, metadata that the definition was produced under Unset Universe Checking is dropped. The title says the issue has been unfixed since 2020.
Unconfirmed: The post says the flaw is unfixed since 2020 but gives no affected or fixed version range.
- Print Assumptions reports the proof as closed under the global context.
- The bypass uses Parameter Inline and functor application.
- The post demonstrates a proof of 0 = 1.
- No fixed version is given.
Impact: Unsafe proofs can appear axiom-free and closed
| Product | Affected |
|---|---|
| Rocq | — |
| Coq | — |
Vulnerabilities mentioned
All| CVE | Vulnerability | CVSS | EPSS | Signals | Published |
|---|---|---|---|---|---|
| CVE-2020-37268 | Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter… | 6.8 | <1% |
From the original article
Posted by Jonathan Brossard on Oct 25 1. Summary ========== A soundness-audit bypass in the Rocq (formerly Coq) module system allows construction of a proof of False that Print Assumptions reports as closed under the global context — no axioms, no unsafe flags visible.
seclists.org
A short excerpt; the article and its images belong to the publisher. Summary, key facts and assessment above are AI-written from the article and can be wrong.