CVE-2026-72704 — Le vérificateur de garde de Rocq fait confiance à un arbre récursif corrompu après transport

Prouver 0 = 1 à partir d'axiomes cohérents via la corruption de l'arbre récursif du point fixe du vérificateur de garde.

Champ	Valeur
Rapport de bug	rocq-prover/rocq#22024
Correctif	PR #22027 (ouverte)
Affecté	Rocq ≤ 9.2.0 / Coq 8.x (toutes les versions avec vérificateur de garde)
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1
CWE	CWE-670 (Implémentation de flux de contrôle toujours incorrecte)
CVE	CVE-2026-72704

Résumé de la vulnérabilité

Le vérificateur de garde du Rocq Prover (vérificateur de terminaison pour les points fixes) ne parvient pas à revérifier la représentation en arbre récursif des arguments de type inductif lorsqu'ils sont modifiés via le transport (rew). Un point fixe peut silencieusement corrompre l'arbre récursif du paramètre de type d'un inductif, et un second point fixe qui appelle le premier fera confiance à l'arbre récursif corrompu sans vérification, acceptant une définition non terminante comme structurellement décroissante.

L'exploit utilise deux axiomes qui sont cohérents avec le CIC — ils sont des conséquences directes de l'axiome d'univalence (la bijection échangeant 0↔1 donne un chemin nat = nat dans Type le long duquel le transport envoie 0 vers 1). Un vérificateur de garde sain ne doit pas dériver False à partir d'axiomes cohérents.

L'exploit :

• N'utilise que deux axiomes cohérents (conséquences de l'univalence)
• Print Assumptions ne rapporte que ces deux axiomes — pas de False, pas de sorry
• Aucun plugin, aucune fonctionnalité dangereuse, aucune manipulation d'univers
• Le vérificateur de garde est la seule source de non-solidité

Utilisation

docker build -t rocq-cve-poc-22024 .
docker run --rm rocq-cve-poc-22024

Sortie attendue sur une version Rocq vulnérable :

[*] Compiling ZeroEqOne.v with rocq compile ...

zero_eq_one is defined
Axioms:
e : nat = nat
e1 : rew [fun T : Type => T] e in 0 = 1

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Axioms used: e (nat = nat), e1 (transport sends 0 to 1)
    These axioms are consistent (consequences of univalence).
    A sound guard checker must not derive False from them.

    Bug class:  Guard checker rectree corruption (CWE-670)
    Root cause: fixpoints can alter rectrees via transport; nested
                fixpoints trust the corrupted rectree without recheck
    Bug report: https://github.com/rocq-prover/rocq/issues/22024

Impact

Tout système qui fait confiance aux preuves vérifiées par le noyau de Rocq et utilise des axiomes cohérents avec l'univalence est affecté :

• Développements HoTT : tout projet Rocq utilisant l'axiome d'univalence (ou l'extensionalité propositionnelle, qui peut déclencher la même classe de bug) pourrait voir ses points fixes vérifiés par le guard checker silencieusement acceptés malgré leur non-terminaison.
• Logiciels formellement vérifiés : CompCert, CertiKOS, Iris, et tout projet qui ajoute des axiomes personnalisés cohérents avec le CIC est à risque si le guard checker est la seule garantie de terminaison.
• Code porteur de preuve : une dépendance malveillante peut introduire les deux axiomes et le point fixe corrompu, puis utiliser False en aval.

Détails techniques

Le bug du guard checker

Le guard checker de Rocq vérifie que les points fixes décroissent structurellement en construisant un rectree — un arbre qui suit quels sous-termes de l'argument récursif sont disponibles à chaque appel récursif. Le bug est une défaillance en deux étapes :

1. Corruption du rectree : weird est un point fixe sur Box A qui applique rew [Box] e (transport le long de e : A = A) à l'argument récursif dans le cas wrap. Le guard checker l'accepte car le transport préserve le type inductif Box, mais le rectree pour le paramètre A est silencieusement altéré — après le transport, le modèle interne du guard checker ne suit plus précisément quelles valeurs circulent à travers A.

2. Confiance non vérifiée : loop appelle weird loop e (wrap _ (box _ n)). Le guard checker vérifie les propres appels récursifs de loop mais fait confiance au rectree de weird pour l'appel imbriqué. Comme le rectree de weird a été corrompu par le transport, le guard checker conclut à tort que loop décroît structurellement.

La contradiction

Le guard checker étant trompé, loop est accepté bien qu'il ne termine pas. La preuve montre alors :

loop 1 = S (loop 1)

en dépliant loop et weird, et en utilisant e1 pour montrer que transport envoie box nat 0 vers box nat 1, qui revient dans loop. Puisque ∀ n, n ≠ S n est prouvable par induction, loop 1 = S (loop 1) donne False, et de là 0 = 1.

Pourquoi les axiomes sont cohérents

Les deux axiomes :

e  : nat = nat :> Type
e1 : rew [fun T => T] e in 0 = 1

sont des conséquences de l'axiome d'univalence. Sous l'univalence, toute bijection f : nat → nat donne un chemin nat = nat dans Type, et le transport le long de ce chemin agit comme f. La bijection swap01 qui envoie 0↦1, 1↦0, et n↦n pour n≥2 est une telle bijection, avec swap01 0 = 1 témoignant de e1.

L'univalence est connue pour être cohérente avec le CIC (validée par des modèles de théorie des types cubiques). Par conséquent, ces axiomes ne peuvent pas être la source de la contradiction — c'est le vérificateur de garde qui l'est.

Comparaison avec d'autres PoC

Aspect	Rocq #22024 (ce bug)	Rocq #22287	Lean #14484
Classe de bug	Corruption de l'arbre de récursion du vérificateur de garde	Désynchronisation de l'état de vérification des univers	Empoisonnement du cache d'inférence
Axiomes nécessaires	2 (cohérents avec l'univalence)	Aucun	Aucun
Complexité de l'exploit	~30 lignes	6 lignes	~20 lignes
Composant	Vérificateur de garde (point fixe)	Système de modules (drapeau ugraph)	Vérificateur de types (décl. opaque)
État du correctif	PR #22027 (ouverte)	Ouverte	Corrigé (PR #14498)

Crédits

• Découverte du bug : Yann Leray (@yannl35133)
• Packaging du PoC : Jonathan Brossard (@endrazine)