CVE-2020-37268

Bir modül tipinde Parameter Inline aracılığıyla çağırıcıya ulaşan bir tanım için, universe kontrolü devre dışıyken bu tanımın üretildiği Print Assumptions tarafından raporlanmamaktadır. Bir functor'ın uygulanması parametrenin gövdesini inline eder ve bu işlem terimin Unset Universe Checking altında oluşturulduğuna dair kaydı siler; böylece sonuçlanan sabit, güvenli olmayan işlemin hiçbir izini taşımaz. Bu nedenle, bir modül uygulaması universe tutarsızlığı kullanarak False ifadesini kanıtlayabilir, bunu inline edilmiş bir parametre üzerinden açığa çıkarabilir ve Print Assumptions'ın bağımlı kanıtı küresel bağlam altında kapalı olarak raporlamasını sağlayabilir. Print Assumptions, bir geliştirmenin beklenmedik varsayımlara dayanmadığını onaylamak için kullanılan süreç içi denetim olduğu için, bu şekilde oluşturulan bir bağımlılık rastgele önermeleri kanıtlarken söz konusu denetimden geçer. Bağımsız denetleyici coqchk ise sonuçlanan derlenmiş dosyayı reddeder. Proje bunu dev/doc/critical-bugs.md dosyasında düzeltilmemiş hatalar altında kaydetmekte ve coqchk kullanılmadığında riski orta düzeyde olarak değerlendirmektedir.