CVE-2020-37268 (CVSS 6.3)

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.

Is your site exposed to CVE-2020-37268?

Run a free security scan — no signup, results in seconds.

CVSS v3.1 Score

6.3

MEDIUM

CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N

EPSS — Exploit Prediction

0.0012

Probability of exploitation

0.02%

Percentile rank

EPSS estimates the probability that this vulnerability will be exploited in the wild within the next 30 days. A higher score means more likely to be exploited.

Weakness Type (CWE)

CWE-778 CWE-778

References

Other References

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

Frequently Asked Questions

What is 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 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. It has a CVSS v3.1 base score of 6.3 (MEDIUM).

How severe is CVE-2020-37268? +

CVE-2020-37268 has a CVSS v3.1 score of 6.3 out of 10, rated MEDIUM. This is a medium-severity vulnerability that should be remediated as part of regular maintenance. The EPSS score is 0.0012, placing it in the 0th percentile for exploitation probability.

How do I check if I'm vulnerable to CVE-2020-37268? +

You can use Secably's free Website Scanner to check your website for known vulnerabilities. For infrastructure scanning, use the Port Scanner to identify exposed services that may be affected. Check the vendor advisories linked above for specific patch and version information.

Related Vulnerabilities

CVE-2024-10863

: Insufficient Logging vulnerability in OpenText Secure Content Manager on Windows allows Audit Log Manipulation.This issue affects Secure Content Manager: …

CVE-2024-48967 10.0

The ventilator and the Service PC lack sufficient audit logging capabilities to allow for detection of malicious activity and subsequent …

CVE-2026-76208 8.2

phpMyFAQ versions 3.1.0 through 4.1.6 contain an authentication bypass vulnerability in AuthLdap::create(). When LDAP authentication is enabled, after a successful …

CVE-2025-2562 5.4

Insufficient logging in the autotyping feature in Devolutions Remote Desktop Manager on Windows allows an authenticated user to use a …

CVE-2025-32967 5.4

OpenEMR is a free and open source electronic health records and medical practice management application. A logging oversight in versions …

CVE-2025-62307 5.4

HCL IntelliOps Event Management (IEM) is affected by insufficient logging. Insufficient logging weakens accountability, obscures attack detection, and enables privilege …

CVE-2020-37268