CVE-2026-72704

Résumé

Le vérificateur de garde de Rocq Prover ne revérifie pas la représentation arborescente récursive d'un paramètre de type inductif après que ce paramètre a été modifié par transport. Un point fixe peut appliquer une réécriture le long d'une égalité entre types à son argument récursif, ce que le vérificateur de garde accepte parce que le type inductif est préservé, tandis que l'arbre récursif enregistré pour le paramètre est altéré. Un second point fixe qui appelle le premier hérite de l'arbre récursif altéré sans vérification, de sorte qu'un appel qui n'est pas structurellement décroissant est accepté comme terminant. La définition non terminante qui en résulte prouve qu'un entier naturel est égal à son propre successeur et donc False, d'où découle n'importe quelle proposition. La démonstration utilise deux axiomes qui découlent de l'univalence et sont cohérents avec le calcul des constructions inductives, de sorte que la contradiction provient de la vérification de garde plutôt que des hypothèses. Un correctif est proposé mais non fusionné.

Sources

• rocq-cve-poc-22024PoC

  CVE-2026-72704 — Rocq Guard Checker fait confiance à un arbre récursif corrompu après transport