endrazine/rocq-cve-poc-22024CVE-2026-72704 — Rocq Guard Checker confía en un árbol recursivo corrupto tras el transporte
Demostrando 0 = 1 a partir de axiomas consistentes mediante la corrupción del rectree del punto fijo del verificador de guardas.
| Campo | Valor |
|---|---|
| Informe de error | rocq-prover/rocq#22024 |
| Corrección | PR #22027 (abierta) |
| Afectado | Rocq ≤ 9.2.0 / Coq 8.x (todas las versiones con verificador de guardas) |
| 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-72704 |
El verificador de guardas de Rocq Prover (verificador de terminación para puntos fijos) no vuelve a
comprobar la representación rectree de los argumentos de tipos inductivos cuando estos se
modifican mediante transporte (rew). Un punto fijo puede corromper silenciosamente el rectree
de un parámetro de tipo de un inductivo, y un segundo punto fijo que llama al primero
confiará en el rectree corrupto sin verificación, aceptando una
definición no terminante como estructuralmente decreciente.
El exploit utiliza dos axiomas que son consistentes con CIC — son consecuencias
directas del axioma de univalencia (la biyección que intercambia 0↔1 da una ruta
nat = nat en Type a lo largo de la cual el transporte envía 0 a 1). Un verificador de guardas
sólido no debe derivar False a partir de axiomas consistentes.
El exploit:
Print Assumptions informa solo esos dos axiomas — sin False, sin sorrydocker build -t rocq-cve-poc-22024 .
docker run --rm rocq-cve-poc-22024
Salida esperada en una versión vulnerable de Rocq:
[*] Compiling ZeroEqOne.v with rocq compile ...
zero_eq_one is defined
Axioms:
e : nat = nat
e1 : rew [fun T : Type => T] e in 0 = 1
[!] VULNERABILITY CONFIRMED
zero_eq_one : 0 = 1
Axioms used: e (nat = nat), e1 (transport sends 0 to 1)
These axioms are consistent (consequences of univalence).
A sound guard checker must not derive False from them.
Bug class: Guard checker rectree corruption (CWE-670)
Root cause: fixpoints can alter rectrees via transport; nested
fixpoints trust the corrupted rectree without recheck
Bug report: https://github.com/rocq-prover/rocq/issues/22024
Cualquier sistema que confíe en las pruebas verificadas por el kernel de Rocq y utilice axiomas consistentes con la univalencia se ve afectado:
False en etapas posteriores.El guard checker de Rocq verifica que los puntos fijos son estructuralmente decrecientes mediante la construcción de un rectree — un árbol que rastrea qué sub términos del argumento recursivo están disponibles en cada llamada recursiva. El error es un fallo en dos pasos:
Corrupción del rectree: weird es un punto fijo sobre Box A que aplica
rew [Box] e (transporte a lo largo de e : A = A) al argumento recursivo
en el caso wrap. El guard checker acepta esto porque el transporte
preserva el tipo inductivo Box, pero el rectree para el parámetro
A se altera silenciosamente — tras el transporte, el modelo interno del guard checker
ya no rastrea con precisión qué valores fluyen a través de A.
Confianza no verificada: loop llama a weird loop e (wrap _ (box _ n)).
El guard checker verifica las llamadas recursivas propias de loop pero confía en
el rectree de weird para la llamada anidada. Dado que el rectree de weird ha sido
corrompido por el transporte, el guard checker concluye incorrectamente
que loop es estructuralmente decreciente.
Con el guard checker engañado, loop es aceptado a pesar de ser
no terminante. La prueba entonces muestra:
loop 1 = S (loop 1)
al desplegar loop y weird, y usando e1 para mostrar que transport envía
box nat 0 a box nat 1, que retroalimenta a loop. Dado que
∀ n, n ≠ S n es demostrable por inducción, loop 1 = S (loop 1) produce
False, y de ahí 0 = 1.
Los dos axiomas:
e : nat = nat :> Type
e1 : rew [fun T => T] e in 0 = 1
son consecuencias del axioma de univalencia. Bajo univalencia, cualquier biyección
f : nat → nat da una ruta nat = nat en Type, y el transporte a lo largo
de esa ruta actúa como f. La biyección swap01 que envía 0↦1, 1↦0, y
n↦n para n≥2 es tal biyección, con swap01 0 = 1 atestiguando e1.
Se sabe que la univalencia es consistente con CIC (validada por modelos de teoría de tipos cúbica). Por lo tanto, estos axiomas no pueden ser el origen de la contradicción — el verificador de guardas lo es.
| Aspecto | Rocq #22024 (este bug) | Rocq #22287 | Lean #14484 |
|---|---|---|---|
| Clase de bug | Corrupción del árbol de guardas | Desincronización del estado de verificación de universos | Envenenamiento de la caché de inferencia |
| Axiomas necesarios | 2 (consistentes con univalencia) | Ninguno | Ninguno |
| Complejidad del exploit | ~30 líneas | 6 líneas | ~20 líneas |
| Componente | Verificador de guardas (fixpoint) | Sistema de módulos (flag ugraph) | Verificador de tipos (decl. opaca) |
| Estado de la corrección | PR #22027 (abierto) | Abierto | Corregido (PR #14498) |