CVE-2020-37268

CVE-2020-37268 is a medium-severity vulnerability with a CVSS 3.x base score of 6.3. It is not currently listed as actively exploited by CISA, and its EPSS exploit-prediction score is low. The underlying weakness is classified as CWE-778.

Key facts

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.

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.
How severe is CVE-2020-37268?
CVE-2020-37268 has a CVSS 3.x base score of 6.3, rated medium severity. It is exploitable over local access with low attack complexity, requires no privileges and user interaction. Impact on confidentiality is none, integrity high, and availability none.
Is CVE-2020-37268 being actively exploited?
It is not currently listed in CISA's KEV catalog. Its EPSS exploit-prediction score is 0% (7th percentile), an estimate of the probability of exploitation in the next 30 days.
How do I fix CVE-2020-37268?
Review the linked vendor and NVD advisories for patched versions and mitigations, then upgrade or apply the recommended workaround.
When was CVE-2020-37268 published?
CVE-2020-37268 was published on 2026-08-24 and last updated on 2026-09-08.

References

Other CWE-778 vulnerabilities

Browse all CWE-778 vulnerabilities →