endrazine/rocq-cve-poc-21683CVE-2026-72705 — Rocq Guard Checker accetta un fixpoint passato come argomento di ordine superiore
Dimostrazione di 0 = 1 senza assiomi tramite il paradosso di Russell attraverso il bypass del fixpoint nel guard checker.
Scoperta autonomamente da Claude Opus 4.6 (Anthropic).
| Campo | Valore |
|---|---|
| Bug report | rocq-prover/rocq#21683 |
| Fix | PR #21684 |
| Affected | Rocq ≤ 9.1.0 / tutte le versioni di Coq con guard checker |
| Fixed in | 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 (Always-Incorrect Control Flow Implementation) |
| CVE | CVE-2026-72705 |
Il guard checker accetta fixpoint che passano se stessi come argomenti di
ordine superiore a un altro fixpoint, il quale poi li invoca su non-sottotermini
dell'argomento strutturale. Passare una funzione ricorsiva a una Definition
(costante non-fixpoint) viene correttamente rifiutato — il guard checker la
espande e vede la chiamata problematica. Ma passarla a un Fixpoint viene
accettato in modo errato.
Questo crea un paradosso in stile Russell in 4 righe:
Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.
dove russell 1 è per definizione uguale a russell 1 -> False — un tipo
che è la propria negazione. L'auto-applicazione dà direttamente False.
L'exploit:
Print Assumptions riporta "Closed under the global context"False è composta da 4 righe di codice funzionaleQed — puramente definizionaledocker build -t rocq-cve-poc-21683 .
docker run --rm rocq-cve-poc-21683
Qualsiasi sistema che si affida alle prove verificate dal kernel di Rocq è interessato:
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
Il guard checker dovrebbe rifiutare russell perché passa se stesso come
argomento di ordine superiore a iterate_to_neg, che poi lo chiama su S m
(non un sottermine di n). Ma il checker traccia solo le chiamate ricorsive dirette,
non le chiamate attraverso argomenti di punto fisso di ordine superiore.
russell 1 = iterate_to_neg russell 1 1
= iterate_to_neg russell 0 1
= russell 1 -> False
Quindi russell 1 ≡ russell 1 -> False. Questo è il classico insieme di Russell: l'insieme di tutti gli insiemi che non contengono se stessi. L'auto-applicazione dà:
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 *)
Questo bug è stato trovato autonomamente da Claude Opus 4.6 durante un'esecuzione di fuzzing notturna allestita da Tristan Stérin (@tcosmo), sulla base di indicazioni di Yannick Forster (@yforster) sul guard checker. L'IA ha identificato il pattern di bypass del punto fisso di ordine superiore e ha costruito l'exploit minimale iterate_to_neg/russell.
Vedi: thread Zulip