Print Assumptions Vulnerability in Rocq Prover by Endrazine

CVE-2020-37268

What is CVE-2020-37268?

The Print Assumptions feature in Rocq Prover is vulnerable to a flaw arising from the failure to report the disabling of universe checking during specific operations. When a definition is created under these conditions, it can be inlined through parameters without retaining any record of the unsafe operation, enabling the potential for arbitrary propositions to be proven even though the in-process audit suggests otherwise. This inconsistency can yield misleading results that pass audits while actually being unsafe, as noted by the standalone checker coqchk, which correctly identifies and rejects the flawed compiled files.

References