CVE-2020-37268

Résumé

Print Assumptions ne signale pas qu'une définition a été produite alors que la vérification des univers était désactivée lorsque cette définition atteint l'appelant via Parameter Inline dans un type de module. L'application d'un foncteur intègre le corps du paramètre, et cette intégration supprime l'enregistrement indiquant que le terme a été construit sous Unset Universe Checking, de sorte que la constante résultante ne porte aucune trace de l'opération non sûre. Une implémentation de module peut donc prouver False à l'aide d'une incohérence d'univers, l'exposer via un paramètre intégré, et faire en sorte que Print Assumptions signale la preuve dépendante comme close sous le contexte global. Étant donné que Print Assumptions est l'audit en cours de processus utilisé pour confirmer qu'un développement ne repose sur aucune hypothèse inattendue, une dépendance construite de cette manière passe cet audit tout en prouvant des propositions arbitraires. Le vérificateur autonome coqchk rejette bien le fichier compilé résultant. Le projet consigne ce problème dans dev/doc/critical-bugs.md parmi les bogues non corrigés et évalue le risque comme modéré lorsque coqchk n'est pas utilisé.

Sources

• rocq-cve-poc-12155PoC

  CVE-2020-37268 — Rocq/Coq Print Assumptions omet la vérification des univers non sûrs via Parameter Inline