CVE-2026-72714 — Vérification des univers de Rocq désynchronisée après la fermeture d'un module

Prouver 0 = 1 sans axiome via la désynchronisation du drapeau de vérification des univers à portée de module.

Champ	Valeur
Rapport de bug	rocq-prover/rocq#22287
Correctif	Aucun (issue ouverte au 2026-08-16)
Affecté	Rocq ≤ 9.2.0 / Coq 8.x (toutes les versions avec Hurkens dans la stdlib)
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1
CWE	CWE-488 (Exposition d'un élément de données à une mauvaise session), CWE-20 (Validation d'entrée incorrecte)
CVE	CVE-2026-72714

Résumé de la vulnérabilité

Le système de modules du Rocq Prover ne parvient pas à délimiter correctement la portée du drapeau Local Unset Universe Checking. Lorsqu'il est utilisé à l'intérieur d'un module, le drapeau devrait être restauré à son état précédent à la fermeture du module. Cependant, le graphe des univers (ugraph) maintient sa propre copie du drapeau, qui se désynchronise de l'état global lors de la fermeture du module.

Après la désynchronisation :

• Test Universe Checking indique on (le drapeau global a été restauré)
• L'ugraph a toujours la vérification des univers off (sa copie n'a pas été restaurée)
• Le noyau accepte donc des termes incohérents vis-à-vis des univers sans erreur

La vérification des univers étant effectivement désactivée, le paradoxe de Hurkens s'applique : TypeNeqSmallType.paradox exploite le fait que Type@{u} et Type@{v} avec u < v peuvent être confondus lorsque les contraintes d'univers ne sont pas appliquées, produisant une preuve directe de False.

L'exploit :

• N'utilise aucun axiome, plugin ou fonctionnalité non sûre
• Print Assumptions indique "Closed under the global context"
• Nécessite uniquement Stdlib.Logic.Hurkens (partie de la bibliothèque standard)
• Représente 6 lignes de code de preuve

Utilisation

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

Sortie attendue sur une version Rocq vulnérable :

[*] Compiling ZeroEqOne.v ...
Universe Checking is on.
bad is defined
Closed under the global context
zero_eq_one is defined
Closed under the global context

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms (closed under the global context)

    Bug class:  Universe checking state desync (CWE-488)
    Root cause: ugraph retains stale Local Unset Universe Checking flag
    Bug report: https://github.com/rocq-prover/rocq/issues/22287

Impact

Tout système qui fait confiance aux preuves vérifiées par le noyau de Rocq est affecté :

• Logiciels formellement vérifiés : CompCert (compilateur C vérifié), CertiKOS (noyau OS vérifié), Iris (framework de logique de séparation concurrente), MathComp — tout dossier de sûreté reposant sur une preuve Rocq est invalide si l'environnement de preuve a subi cette désynchronisation du drapeau.
• Code porteur de preuve : un fichier .v malveillant dans une dépendance peut introduire silencieusement des déclarations non sûres sur lesquelles reposent les preuves en aval.
• Contrats intelligents : les projets utilisant Rocq pour le développement vérifié de contrats intelligents (par exemple, ConCert) pourraient voir leurs garanties de sécurité annulées.

Détails techniques

Cause racine

Le graphe d'univers (ugraph) dans le noyau contient sa propre copie du drapeau Universe Checking. Lorsqu'un module utilise Local Unset Universe Checking, le drapeau est modifié à la fois dans l'état global et dans le ugraph. Lorsque le module se ferme, l'état global est restauré à partir de l'état sauvegardé du module, mais la copie du ugraph n'est pas synchronisée, laissant la vérification des univers effectivement désactivée.

Déroulement de l'attaque

┌─────────────────────────────────────────────────────┐
│ 1. Universes u v.  Constraint u < v.                │
│    → Declare universes with strict ordering          │
├─────────────────────────────────────────────────────┤
│ 2. Module Off.                                       │
│      Local Unset Universe Checking.                  │
│    End Off.                                          │
│    → ugraph flag stays OFF after module closes        │
├─────────────────────────────────────────────────────┤
│ 3. Test Universe Checking.  → reports "on" (LIE)     │
├─────────────────────────────────────────────────────┤
│ 4. eapply TypeNeqSmallType.paradox; reflexivity.     │
│    → Kernel accepts universe-inconsistent proof       │
│    → False proved with no axioms                     │
├─────────────────────────────────────────────────────┤
│ 5. zero_eq_one : 0 = 1                              │
│    → Derived via exfalso                             │
└─────────────────────────────────────────────────────┘

Comparaison avec les bugs du noyau Lean 4

Aspect	Rocq #22287 (ce bug)	Lean #14484	Lean #14576
Assistant de preuve	Rocq (Coq)	Lean 4	Lean 4
Classe de bug	Désynchronisation d'état dans le système de modules	Empoisonnement du cache d'inférence	Confusion de types via les projections
Complexité de l'exploit	6 lignes	~20 lignes	~50 lignes
Système d'univers/types	Vérification des univers contournée	FVar opaque accepté	Fuite de paramètres fantômes
État du correctif	Ouvert	Corrigé (PR #14498)	Corrigé (PR #14577)

Crédits

• Découverte du bug : Gaëtan Gilbert (@SkySkimmer)
• Packaging du PoC : Jonathan Brossard (@endrazine)