CVE-2020-37268

Name of the Vulnerable Software and Affected Versions Coq (affected versions not specified)

Description Print Assumptions fails to report when a definition is produced while universe checking is disabled if that definition reaches the caller via Parameter Inline in a module type. When a functor is applied, the parameter body is inlined, which removes the record that the term was created under Unset Universe Checking. Consequently, the resulting constant shows no trace of the unsafe operation. This allows a module implementation to prove False using a universe inconsistency and expose it through an inlined parameter, while Print Assumptions incorrectly reports the dependent proof as closed under the global context. This bypasses the in-process audit used to ensure developments do not rely on unexpected assumptions, potentially allowing the proof of arbitrary propositions. The standalone checker coqchk correctly rejects the resulting compiled files.

Recommendations At the moment, there is no information about a newer version that contains a fix for this vulnerability. Use the standalone checker coqchk to validate compiled files.