CVE-2020-37268 — Rocq/Coq Print Assumptions omet la vérification des univers non sûre via Parameter Inline

Contournement de l'audit de preuve via l'inlining de foncteur de module — non corrigé depuis 2020.

Résumé de la vulnérabilité

Print Assumptions ne signale pas qu'une définition a été construite avec la vérification des univers désactivée lorsque cette définition parvient à l'appelant via Parameter Inline dans un type de module. L'application de foncteur inline le corps du paramètre et supprime la trace du contexte Unset Universe Checking, de sorte que la constante résultante ne montre aucun signe de l'opération non sûre.

Un module peut donc exploiter une incohérence d'univers pour prouver False, et Print Assumptions rapporte la preuve dépendante comme close sous le contexte global — aucun axiome, aucun indicateur non sûr visible.

coqchk rejette bien le fichier .vo compilé résultant, mais l'audit des hypothèses en cours de processus (Print Assumptions) ne détecte pas le problème.

Utilisation

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

Sur une version vulnérable (Rocq 8.11 – 9.2.0, et tous les Coq 8.x avec le système de modules), la sortie confirme la preuve de 0 = 1 avec Print Assumptions la rapportant comme close.

Impact

Tout flux de travail qui s'appuie sur Print Assumptions comme unique contrôle d'intégrité peut être affecté :

• 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 sûres qui passent l'audit des hypothèses
• Contrats intelligents vérifiés (ConCert)
• Tout projet n'exécutant pas régulièrement coqchk sur la sortie compilée

Cause racine

Lorsqu'un type de module déclare Parameter Inline, l'application de foncteur inline le corps du paramètre dans le contexte appelant. Cet inlining écarte les métadonnées enregistrant que la définition d'origine a été produite sous Unset Universe Checking. Le graphe d'univers accepte donc des contraintes d'univers incohérentes provenant du corps inliné, et Print Assumptions ne voit aucune trace du contexte non sûr.

Le bug est ouvert depuis 2020 (ticket Coq #12155) et est documenté dans le fichier dev/doc/critical-bugs.md du projet. Aucun correctif n'a été fusionné à ce jour pour Rocq 9.2.0.

Notation

Champ	Valeur
CVE	CVE-2020-37268
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-778 — Journalisation insuffisante

Versions affectées

Produit	Affecté	Corrigé
Coq	8.11 – 8.20	Non corrigé
Rocq Prover	8.20 – 9.2.0	Non corrigé

Atténuation

• Exécutez coqchk sur tous les fichiers .vo compilés avant de faire confiance aux preuves en production. coqchk détecte l'incohérence d'univers que Print Assumptions manque.
• Auditez les dépendances de modules — l'attaque nécessite un type de module avec Parameter Inline qui a été compilé sous Unset Universe Checking.
• Aucune version corrigée n'est disponible à ce jour pour Rocq 9.2.0.

Références

Rapport de bug	rocq-prover/rocq#12155
Doc des bugs critiques	dev/doc/critical-bugs.md
Avis VulnCheck	vulncheck.com

Chronologie

Date	Événement
2020	Bug signalé par Jason Gross (coq/coq#12155)
2020–2026	Le bug reste ouvert, documenté dans critical-bugs.md
2026-08-24	CVE-2020-37268 publié par VulnCheck
2026-08-24	PoC reproductible via Docker publié

Crédits

• Découverte du bug : Jason Gross
• Packaging du PoC : Jonathan Brossard (@endrazine) — MOABI / PSIRT.com