CVE-2020-37268
MediumCVSS 6.3Exploitation Probability (EPSS)
Low risk7th percentile - higher than 7% of all known CVEs
Summary
Print Assumptions in Coq 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.
Risk Assessment
The risk is that a malicious library can prove false statements and the Print Assumptions audit will not detect it, potentially leading to unsound foundations for formal proofs.
Recommendation
Use coqchk to verify compiled files and manually check for universe inconsistencies. Also track fixes in Coq.
Related vulnerabilities
- CVE-2026-6715Critical
IBM Concert 1.0 through 3.0.1.1 allows an attacker to supply crafted input that is incorporated into an operating system command without adequate validation or sanitization. Successful exploitation allows remote attackers to execute arbitrary commands on the underlying operating system with the privileges of the affected service.
- CVE-2026-17466Critical
IBM Optim versions 1.0.0, 1.1.0, and 1.2.0 are vulnerable to path traversal, allowing a remote authenticated attacker to obtain sensitive information.
- CVE-2026-15266Critical
IBM Concert 1.0 through 3.0.1.1 contains components that allow potentially unsafe command execution, which could be exploited to run arbitrary system commands on the host.
- CVE-2026-114464Critical
IBM Process Mining 2.0.0 through 2.2.1 has improper access control, which could allow a remote attacker to obtain sensitive information.
- CVE-2026-107331Critical
IBM DataStage on Cloud Pak for Data 5.4.0.0 has an absolute-path traversal vulnerability that could allow a remote authenticated attacker to obtain sensitive information.
- CVE-2026-109900Critical
The Melapress Role Editor plugin for WordPress (through version 1.3.0) contains an incorrect privilege assignment vulnerability that allows privilege escalation. A low-privileged user can gain a higher level of access within the system.
- CVE-2026-101117Critical
IBM WebSphere Extreme Scale versions 8.6.1.0 through 8.6.2.2 have an improper Content Security Policy configuration that could allow a remote attacker to bypass security restrictions. The flaw concerns browser-side protection mechanisms.
- CVE-2026-124494Critical
SunEditor before 3.4.0 contains a stored cross-site scripting vulnerability because the html.clean() sanitizer's _normalizeURL() function decodes named entities like : to an empty string. Attackers can inject href values such as javascript: that pass the _isSafeURL() check but are decoded by browsers, executing JavaScript when victims click stored links.
- CVE-2026-124493Critical
SunEditor before 3.4.0 contains a stored cross-site scripting vulnerability in the DocumentType constructor that injects header textContent into innerHTML without HTML escaping. Attackers can store entity-encoded HTML in h1-h6 headers that executes JavaScript when editors using document:header mode initialize, enabling session cookie theft.
- CVE-2026-124490Critical
OpenEMR before 8.3.0 contains a path traversal vulnerability in the RingCentral RCFaxClient disposeDocument() method of oe-module-faxsms that allows authenticated attackers to read and write arbitrary files via the file_path parameter. Attackers can use action=download to read credentials and source code, or action=setup with base64 content to write web-executable files for code execution.
Original NVD description (English source)
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.
Vulnerability data from NVD (NIST) · CISA KEV · EPSS