CVE-2026-72703 — Le vérificateur de garde de Rocq accepte un point fixe non terminant via des appels croisés non vérifiés

Preuve de 0 = 1 sans axiome via le contournement des paramètres uniformes du vérificateur de garde.

Résumé de la vulnérabilité

Le vérificateur de garde du noyau de Rocq (vérificateur de terminaison des points fixes) traite tous les paramètres d'un point fixe mutuel imbriqué comme uniformes sans examiner les appels entre les corps du point fixe. La fonction find_uniform_parameters dans kernel/inductive.ml n'inspecte que les appels auto-récursifs ; lorsqu'aucun corps ne s'appelle lui-même, chaque paramètre est jugé uniforme. Un paramètre qui croît via un appel croisé peut alors conserver une spécification de sous-terme incorrecte, et un appel récursif est accepté même si son argument n'est pas structurellement plus petit.

Cela permet une définition non terminante qui prouve False, d'où découle n'importe quelle proposition — y compris 0 = 1.

La preuve ne nécessite aucun axiome, tactique, plugin ni indicateur non sécurisé. Print Assumptions la rapporte comme close sous le contexte global.

Utilisation

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

Sur une version vulnérable (Rocq 8.20 – <9.2.0), la sortie confirme la preuve de 0 = 1 sans aucun axiome.

Sur une version corrigée (Rocq ≥9.2.0), le vérificateur de garde rejette le point fixe.

Impact

Tout système qui s'appuie sur des preuves vérifiées par le noyau de Rocq/Coq peut être affecté s'il s'exécute sur une version vulnérable sans mesure d'atténuation supplémentaire :

• Compilateurs formellement vérifiés (CompCert)
• Noyaux de systèmes d'exploitation vérifiés (CertiKOS)
• Frameworks de logique de séparation (Iris)
• Bibliothèques mathématiques (MathComp)
• Code porteur de preuve où un fichier .v malveillant dans une dépendance pourrait introduire des déclarations non valides
• Contrats intelligents vérifiés (ConCert)

Cause racine

find_uniform_parameters dans kernel/inductive.ml n'inspecte que les appels auto-récursifs au sein de chaque corps d'un point fixe mutuel. Lorsqu'aucun corps ne contient d'appel auto-récursif (tous les appels sont des appels croisés entre corps), chaque paramètre est marqué comme uniforme. Un paramètre qui varie réellement au fil des appels croisés conserve une spécification de sous-terme incorrecte, ce qui permet au vérificateur de garde d'accepter un appel récursif sur un argument qui ne décroît pas structurellement.

Notation

Champ	Valeur
CVE	CVE-2026-72703
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (Élevé)
CVSS 4.0	AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N — 6.8 (Moyen)
CWE	CWE-670 — Implémentation de flux de contrôle toujours incorrecte

Versions affectées

Produit	Affectées	Corrigées
Rocq Prover	8.20 – <9.2.0	9.2.0

Atténuation

• Mettre à niveau vers Rocq 9.2.0 ou une version ultérieure.
• Exécuter coqchk sur les fichiers .vo compilés comme mesure de défense en profondeur.

Références

Rapport de bug	rocq-prover/rocq#21682
Correctif	rocq-prover/rocq#21684
Avis VulnCheck	vulncheck.com

Chronologie

Date	Événement
2025	Bug signalé (rocq-prover/rocq#21682)
2025	Correctif fusionné (PR #21684) dans Rocq 9.2.0
2026-08-24	CVE-2026-72703 publié par VulnCheck
2026-08-24	PoC reproductible via Docker publié

Crédits

• Découverte du bug : Tristan Stérin, Claude Opus 4.6 (Anthropic)
• Correctif du noyau : PR #21684
• Packaging du PoC : Jonathan Brossard (@endrazine) — MOABI / PSIRT.com