CVE-2020-37268
Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline
Description
Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter Inline in a module type. Applying a functor inlines the body of the parameter, and the inlining drops the record that the term was built under Unset Universe Checking, so the resulting constant carries no trace of the unsafe operation. A module implementation can therefore prove False using a universe inconsistency, expose it through an inlined parameter, and have Print Assumptions report the dependent proof as closed under the global context. Because Print Assumptions is the in-process audit used to confirm that a development rests on no unexpected assumptions, a dependency built this way passes that audit while proving arbitrary propositions. The standalone checker coqchk does reject the resulting compiled file. The project records this in dev/doc/critical-bugs.md under non-fixed bugs and rates the risk as moderate when coqchk is not used.
INFO
Published Date :
Aug. 24, 2026, 8:16 p.m.
Last Modified :
Aug. 24, 2026, 8:16 p.m.
Remotely Exploit :
No
Source :
[email protected]
Affected Products
The following products are affected by CVE-2020-37268
vulnerability.
Even if cvefeed.io is aware of the exact versions of the
products
that
are
affected, the information is not represented in the table below.
No affected product recoded yet
CVSS Scores
| Score | Version | Severity | Vector | Exploitability Score | Impact Score | Source |
|---|---|---|---|---|---|---|
| CVSS 3.1 | MEDIUM | 83251b91-4cc7-4094-a5c7-464a1b83ea10 | ||||
| CVSS 3.1 | MEDIUM | [email protected] | ||||
| CVSS 4.0 | MEDIUM | 83251b91-4cc7-4094-a5c7-464a1b83ea10 | ||||
| CVSS 4.0 | MEDIUM | [email protected] |
Solution
- Enable universe checking in all modules.
- Verify functor inlining preserves universe checking context.
- Use coqchk to validate compiled files.
- Address or document non-fixed bugs.
References to Advisories, Solutions, and Tools
Here, you will find a curated list of external links that provide in-depth
information, practical solutions, and valuable tools related to
CVE-2020-37268.
CWE - Common Weakness Enumeration
While CVE identifies
specific instances of vulnerabilities, CWE categorizes the common flaws or
weaknesses that can lead to vulnerabilities. CVE-2020-37268 is
associated with the following CWEs:
Common Attack Pattern Enumeration and Classification (CAPEC)
Common Attack Pattern Enumeration and Classification
(CAPEC)
stores attack patterns, which are descriptions of the common attributes and
approaches employed by adversaries to exploit the CVE-2020-37268
weaknesses.
We scan GitHub repositories to detect new proof-of-concept exploits. Following list is a collection of public exploits and proof-of-concepts, which have been published on GitHub (sorted by the most recently updated).
Results are limited to the first 15 repositories due to potential performance issues.
The following list is the news that have been mention
CVE-2020-37268 vulnerability anywhere in the article.
The following table lists the changes that have been made to the
CVE-2020-37268 vulnerability over time.
Vulnerability history details can be useful for understanding the evolution of a vulnerability, and for identifying the most recent changes that may impact the vulnerability's severity, exploitability, or other characteristics.
-
New CVE Received by [email protected]
Aug. 24, 2026
Action Type Old Value New Value Added Affected [{'repo': 'https://github.com/rocq-prover/rocq', 'vendor': 'rocq-prover', 'product': 'rocq', 'versions': [{'status': 'affected', 'version': '8.11', 'versionType': 'custom', 'lessThanOrEqual': '9.2.0'}], 'packageURL': 'pkg:github/rocq-prover/rocq', 'defaultStatus': 'unaffected'}] Added Description Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter Inline in a module type. Applying a functor inlines the body of the parameter, and the inlining drops the record that the term was built under Unset Universe Checking, so the resulting constant carries no trace of the unsafe operation. A module implementation can therefore prove False using a universe inconsistency, expose it through an inlined parameter, and have Print Assumptions report the dependent proof as closed under the global context. Because Print Assumptions is the in-process audit used to confirm that a development rests on no unexpected assumptions, a dependency built this way passes that audit while proving arbitrary propositions. The standalone checker coqchk does reject the resulting compiled file. The project records this in dev/doc/critical-bugs.md under non-fixed bugs and rates the risk as moderate when coqchk is not used. Added CVSS V4.0 AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:X Added CVSS V3.1 AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N Added CWE CWE-778 Added Reference https://github.com/endrazine/rocq-cve-poc-12155 Added Reference https://github.com/rocq-prover/rocq Added Reference https://github.com/rocq-prover/rocq/blob/master/dev/doc/critical-bugs.md Added Reference https://github.com/rocq-prover/rocq/issues/12155 Added Reference https://www.vulncheck.com/advisories/coq-and-rocq-prover-print-assumptions-omits-unsafe-universe-checking-inlined-through-parameter-inline