CVE-2026-72703

Résumé

Le vérificateur de garde dans Rocq Prover traite un paramètre d'un point fixe mutuel imbriqué comme uniforme sans examiner les appels entre les différents corps de ce point fixe. find_uniform_parameters dans kernel/inductive.ml n'inspecte que les appels auto-récursifs, de sorte que lorsqu'aucun corps ne s'appelle lui-même, la fonction conclut que tous les paramètres sont uniformes. Un paramètre qui croît via un appel croisé d'un corps à un autre conserve donc la spécification de sous-terme héritée du point fixe englobant, et un appel récursif gardé par cette spécification est accepté bien que l'argument ne soit pas structurellement plus petit. Une définition non terminante est admise comme structurellement décroissante, ce qui produit un terme dont la valeur est égale à son propre successeur et donc une preuve de False, à partir de laquelle toute proposition découle. La preuve ne nécessite aucun axiome, plugin ni indicateur unsafe, et Print Assumptions la rapporte comme close sous le contexte global. Introduit dans Coq 8.20 et corrigé dans Rocq 9.2.0.

Sources

• rocq-cve-poc-21682PoC

  CVE-2026-72703 — Rocq Guard Checker accepte un point fixe non terminant via des appels croisés non vérifiés