endrazine/rocq-cve-poc-21683CVE-2026-72705 — O verificador Rocq Guard aceita um ponto fixo passado como argumento de ordem superior
Provando 0 = 1 sem axiomas via paradoxo de Russell através do bypass do verificador de guarda em fixpoints.
Descoberto autonomamente por Claude Opus 4.6 (Anthropic).
| Campo | Valor |
|---|---|
| Relatório de bug | rocq-prover/rocq#21683 |
| Correção | PR #21684 |
| Afetado | Rocq ≤ 9.1.0 / todas as versões do Coq com verificador de guarda |
| Corrigido em | 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 (Implementação de fluxo de controle sempre incorreta) |
| CVE | CVE-2026-72705 |
O verificador de guarda aceita fixpoints que se passam a si mesmos como argumentos
de ordem superior para outro fixpoint, que então os chama sobre não-subtermos
do argumento estrutural. Passar uma função recursiva para uma Definition
(constante não-fixpoint) é corretamente rejeitado — o verificador de guarda a
desdobra e vê a chamada problemática. Mas passá-la para um Fixpoint é
incorretamente aceito.
Isso cria um paradoxo no estilo de Russell em 4 linhas:
Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.
onde russell 1 é definicionalmente igual a russell 1 -> False — um tipo
que é a sua própria negação. A autoaplicação dá False diretamente.
O exploit:
Print Assumptions reporta "Closed under the global context"False tem 4 linhas de código funcionalQed — puramente definicionaldocker build -t rocq-cve-poc-21683 .
docker run --rm rocq-cve-poc-21683
Qualquer sistema que confie nas provas verificadas pelo kernel do Rocq é afetado:
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
O verificador de guarda deveria rejeitar russell porque ele se passa como um argumento de ordem superior para iterate_to_neg, que então o chama em S m (não um subtermo de n). Mas o verificador rastreia apenas chamadas recursivas diretas, não chamadas através de argumentos de ponto fixo de ordem superior.
russell 1 = iterate_to_neg russell 1 1
= iterate_to_neg russell 0 1
= russell 1 -> False
Assim, russell 1 ≡ russell 1 -> False. Este é o conjunto de Russell clássico:
o conjunto de todos os conjuntos que não contêm a si mesmos. A autoaplicação resulta em:
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 *)
Este bug foi encontrado de forma autônoma pelo Claude Opus 4.6 durante uma
execução de fuzzing noturna configurada por Tristan Stérin (@tcosmo), com base em indicações de
Yannick Forster (@yforster) sobre o verificador de guardas. A IA identificou o
padrão de contorno de ponto fixo de ordem superior e construiu o exploit mínimo
iterate_to_neg/russell.
Veja: thread do Zulip