Strix
64.7K

CVE-2020-37268

MEDIUMCVSS 6.3/10EPSS 0.12%

Last modified

CVE-2020-37268 is a medium-severity vulnerability rated 6.3/10 on the CVSS scale. 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. EPSS estimates a 0.12% chance of exploitation in the next 30 days.

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

CVSS 3.1
6.3/10

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

CVSS 4.0
6.8/10

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/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

EPSS Probability
0.12%

2.1th percentile

Probability of exploitation in the next 30 days. Learn more

Weakness Enumeration

Affected Software

Source: CNA advisory (CVE.org). NVD analysis pending.

VendorProductVersions
rocq-proverrocq>= 8.11, <= 9.2.0

References

Timeline

Published
Last Modified
Status
Deferred

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 score of 6.3/10 (MEDIUM severity). The EPSS model estimates a 0.12% probability of exploitation in the next 30 days.
How do I fix CVE-2020-37268?
Check the vendor references and advisories linked above for patched versions and mitigation guidance. You can also run a Strix scan to test if your systems are affected.

How Strix Helps

Related CVEs from 2020

View all 2020CVEs →

Are you affected by CVE-2020-37268?

Run a free Strix scan to check your systems for this vulnerability.

Scan your code now

Source: NVD / NIST