CVE-2020-37268
MediumCVSS 6.3Exploitation Probability (EPSS)
Low risk2th percentile - higher than 2% 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-4813Critical
A vulnerability in the XSL export module of Lutece Core up to version 7.1.7 allows authenticated administrators to execute code remotely. The XML/XSLT processing configuration does not enable secure processing mode (FEATURE_SECURE_PROCESSING), allowing Java extension functions to be executed from malicious XSL stylesheets. An attacker with administrator privileges can upload a manipulated XSL transformation file and trigger its execution during user export operations, resulting in the execution of arbitrary code on the server.
- CVE-2026-78319Critical
A service running on the affected products contains a potential Time-of-Check Time-of-Use (TOCTOU) race condition. An unauthenticated remote attacker could exploit this race condition to bypass intended security controls. This may result in the execution of unauthorized code.
- CVE-2026-83772Critical
A vulnerability was detected in Cobham SATCOM VSAT7090 Maritime Satellite Router up to 20260704. The issue affects the function c_set_reports_decode of the file mail-report.sh in the JSON Parsing component. Manipulation of the argument sender/recipients results in command injection. The attack can be launched remotely. The exploit is public and may be used. The vendor was contacted but did not respond.
- CVE-2026-75865Critical
The WPLP Cookie Consent plugin for WordPress up to version 4.4.1 is vulnerable to arbitrary file upload due to missing file type validation in the saas_upload_logo() function combined with an authorization bypass on the WPLP connector REST endpoints. This allows unauthenticated attackers to upload arbitrary files on the server, potentially leading to remote code execution.
- CVE-2026-67394Critical
A critical local privilege escalation via OS command injection vulnerability has been discovered in Plesk for Linux, affecting versions from 18.0.34 before 18.0.79.9 and 18.0.80.5. It allows a customer or reseller with shell access to elevate privileges to the root account on the hosting server.
- CVE-2026-83524Critical
A command injection vulnerability was detected in RedPort Optimizer wXa-203, wXa-213, and wXa-223 up to 20260704, affecting the exec function of the file /xgatev1/system/datetime.php in the System Clock component. The attack can be initiated remotely, and the exploit has been publicly disclosed.
- CVE-2026-82971Critical
A command injection vulnerability was found in QVidium Opera11 version 3.3.2a26-Ax4x-opera11, affecting an unknown part of the file /cgi-bin/net_tr.cgi in the CGI Script component, through manipulation of the ipaddr argument. The attack can be initiated remotely, and the exploit has been publicly disclosed. The vendor has ceased operations and no longer supports these products.
- CVE-2026-82954Critical
A path traversal vulnerability was detected in Dokploy up to version 0.29.7, affecting the writeTraefikConfigInPath function in the file packages/server/src/utils/traefik/application.ts of the Settings component, through manipulation of the path argument. The attack can be launched remotely, and the exploit is public.
- CVE-2026-82226Critical
An unauthenticated PHP Object Injection vulnerability was detected in Tickera versions up to 3.6.0.2. This vulnerability may allow an attacker to execute arbitrary code or perform other unauthorized actions.
- CVE-2026-81780Critical
An unauthenticated Arbitrary File Upload vulnerability was detected in Hash Form versions up to 1.4.2. This vulnerability may allow an attacker to upload malicious files to the server.
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.