endrazine/rocq-cve-poc-21683CVE-2026-72705 — Le vérificateur Rocq Guard accepte un point fixe passé comme argument d'ordre supérieur
Prouver 0 = 1 sans axiome via le paradoxe de Russell en contournant le vérificateur de garde sur les fixpoints.
Découvert de manière autonome par Claude Opus 4.6 (Anthropic).
| Champ | Valeur |
|---|---|
| Rapport de bug | rocq-prover/rocq#21683 |
| Correctif | PR #21684 |
| Affecté | Rocq ≤ 9.1.0 / toutes les versions de Coq avec vérificateur de garde |
| Corrigé dans | 9.2.0 |
| 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-72705 |
Le vérificateur de garde accepte des fixpoints qui se passent eux-mêmes comme arguments d'ordre supérieur à un autre fixpoint, lequel les appelle ensuite sur des non-sous-termes de l'argument structurel. Passer une fonction récursive à une Definition (constante non-fixpoint) est correctement rejeté — le vérificateur de garde la déplie et voit l'appel problématique. Mais le passer à un Fixpoint est incorrectement accepté.
Cela crée un paradoxe de style Russell en 4 lignes :
Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.
où russell 1 est par définition égal à russell 1 -> False — un type
qui est sa propre négation. L'auto-application donne directement False.
L'exploit :
Print Assumptions rapporte « Closed under the global context »False tient en 4 lignes de code fonctionnelQed — purement définitionneldocker build -t rocq-cve-poc-21683 .
docker run --rm rocq-cve-poc-21683
Tout système qui fait confiance aux preuves vérifiées par le noyau de Rocq est affecté :
iterate_to_neg f n seed :=
match n with
| 0 => f seed -> False (* negate after n steps *)
| S m => iterate_to_neg f m seed
end
russell n :=
match n with
| 0 => True
| S m => iterate_to_neg russell 1 (S m) (* passes ITSELF *)
end
Le vérificateur de garde devrait rejeter russell parce qu'il se passe lui-même comme argument d'ordre supérieur à iterate_to_neg, qui l'appelle ensuite sur S m (qui n'est pas un sous-terme de n). Mais le vérificateur ne suit que les appels récursifs directs, pas les appels via des arguments de point fixe d'ordre supérieur.
russell 1 = iterate_to_neg russell 1 1
= iterate_to_neg russell 0 1
= russell 1 -> False
Donc russell 1 ≡ russell 1 -> False. C'est l'ensemble de Russell classique :
l'ensemble de tous les ensembles qui ne se contiennent pas eux-mêmes. L'auto-application donne :
delta : russell 1 -> False (* russell 1 = russell 1 -> False *)
delta x := x x (* x : russell 1 = russell 1 -> False *)
omega : False
omega := delta delta (* delta : russell 1 -> False = russell 1 *)
Ce bug a été trouvé de manière autonome par Claude Opus 4.6 lors d'une campagne de fuzzing nocturne mise en place par Tristan Stérin (@tcosmo), à partir d'indices fournis par Yannick Forster (@yforster) sur le vérificateur de gardes. L'IA a identifié le schéma de contournement du point fixe d'ordre supérieur et a construit l'exploit minimal iterate_to_neg/russell.
Voir : fil Zulip