U.S. flag   An official website of the United States government
Dot gov

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Https

Secure .gov websites use HTTPS
A lock (Dot gov) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

National Vulnerability Database

National Vulnerability Database

NVD

National Vulnerability Database
  1. Vulnerabilities

CVE-2020-37268 Detail

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.


Metrics

 
NVD enrichment efforts reference publicly available information to associate vector strings. CVSS information contributed by other sources is also displayed.
CVSS 4.0 Severity and Vector Strings:

NIST CVSS score
NIST: NVD
N/A
NVD assessment not yet provided.

Nist CVSS score does not match with CNA score
CNA:  VulnCheck
CVSS-B 6.8 MEDIUM
Vector:  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

References to Advisories, Solutions, and Tools

By selecting these links, you will be leaving NIST webspace. We have provided these links to other web sites because they may have information that would be of interest to you. No inferences should be drawn on account of other sites being referenced, or not, from this page. There may be other web sites that are more appropriate for your purpose. NIST does not necessarily endorse the views expressed, or concur with the facts presented on these sites. Further, NIST does not endorse any commercial products that may be mentioned on these sites. Please address comments about this page to [email protected].

URL Source(s) Tag(s)
https://github.com/endrazine/rocq-cve-poc-12155 VulnCheck
https://github.com/rocq-prover/rocq VulnCheck
https://github.com/rocq-prover/rocq/blob/master/dev/doc/critical-bugs.md VulnCheck
https://github.com/rocq-prover/rocq/issues/12155 VulnCheck
https://www.vulncheck.com/advisories/coq-and-rocq-prover-print-assumptions-omits-unsafe-universe-checking-inlined-through-parameter-inline VulnCheck

Weakness Enumeration

CWE-ID CWE Name Source
CWE-778 Insufficient Logging VulnCheck  

Change History

1 change records found show changes

Quick Info

CVE Dictionary Entry:
CVE-2020-37268
NVD Published Date:
08/24/2026
NVD Last Modified:
08/24/2026
Source:
VulnCheck