CVE-2020-37268
Description
A flaw was found in Coq and Rocq provers. The Print Assumptions feature, which is used to audit the soundness of proofs, fails to report when a definition was created without proper "universe checking" (a mechanism to ensure logical consistency). This occurs when the definition is incorporated through "Parameter Inline" in a module type. An attacker could exploit this to introduce logically false statements into a proof, bypassing the audit and potentially leading to the acceptance of invalid mathematical or logical conclusions.
Statement
Red Hat Product Security has determined that this vulnerability does not affect any currently supported Red Hat product. This assessment may evolve based on further analysis and discovery. For more information about this vulnerability and the products it affects, please see the linked references.
Mitigation
To mitigate the risk associated with this flaw, ensure that the `coqchk` standalone checker is consistently used to validate compiled Coq files. The `coqchk` tool is designed to detect and reject files that exploit the `Print Assumptions` omission, thereby preventing the acceptance of logically inconsistent proofs within the Coq environment.
Understanding the Weakness (CWE)
Integrity,Other
Technical Impact: Varies by Context; Unexpected State
Errors that are not properly reported could place the system in an unexpected state that could lead to unintended behaviors.
Frequently Asked Questions
Not sure what something means? Check out our Security Glossary.
Want to get errata notifications? Sign up here.
