6.8
MEDIUM CVSS 4.0
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
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
The Common Vulnerability Scoring System is a standardized framework for assessing the severity of vulnerabilities in software and systems. We collect and displays CVSS scores from various sources for each CVE.
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
Ensure universe checking is enabled and properly configured to prevent proof bypasses.
  • 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.
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
EPSS is a daily estimate of the probability of exploitation activity being observed over the next 30 days. Following chart shows the EPSS score history of the vulnerability.