CVE-2026-72714 — Estado de comprobación de universos de Rocq desincronizado tras el cierre de un módulo

Demostrando 0 = 1 sin axiomas mediante la desincronización del flag de comprobación de universos con ámbito de módulo.

Campo	Valor
Informe de error	rocq-prover/rocq#22287
Corrección	Ninguna (issue abierto a fecha de 2026-08-16)
Afectado	Rocq ≤ 9.2.0 / Coq 8.x (todas las versiones con Hurkens en la stdlib)
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1
CWE	CWE-488 (Exposición de un elemento de datos a una sesión incorrecta), CWE-20 (Validación de entrada incorrecta)
CVE	CVE-2026-72714

Resumen de la vulnerabilidad

El sistema de módulos de Rocq Prover no aplica correctamente el ámbito al flag Local Unset Universe Checking. Cuando se usa dentro de un módulo, el flag debería restaurarse a su estado anterior al cerrarse el módulo. Sin embargo, el grafo de universos (ugraph) mantiene su propia copia del flag, que queda desincronizada con el estado global al cerrarse el módulo.

Tras la desincronización:

• Test Universe Checking informa on (el flag global fue restaurado)
• El ugraph sigue teniendo la comprobación de universos off (su copia no fue restaurada)
• El kernel, por tanto, acepta términos inconsistentes en universos sin error

Con la comprobación de universos efectivamente deshabilitada, se aplica la paradoja de Hurkens: TypeNeqSmallType.paradox explota el hecho de que Type@{u} y Type@{v} con u < v pueden confundirse cuando no se aplican las restricciones de universos, produciendo una demostración directa de False.

El exploit:

• No usa ningún axioma, plugin ni característica insegura
• Print Assumptions informa "Closed under the global context"
• Solo requiere Stdlib.Logic.Hurkens (parte de la biblioteca estándar)
• Consta de 6 líneas de código de demostración

Uso

docker build -t rocq-cve-poc-22287 .
docker run --rm rocq-cve-poc-22287

Salida esperada en una versión vulnerable de Rocq:

[*] Compiling ZeroEqOne.v ...
Universe Checking is on.
bad is defined
Closed under the global context
zero_eq_one is defined
Closed under the global context

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms (closed under the global context)

    Bug class:  Universe checking state desync (CWE-488)
    Root cause: ugraph retains stale Local Unset Universe Checking flag
    Bug report: https://github.com/rocq-prover/rocq/issues/22287

Impacto

Cualquier sistema que confíe en las pruebas verificadas por el kernel de Rocq se ve afectado:

• Software verificado formalmente: CompCert (compilador de C verificado), CertiKOS (kernel de SO verificado), Iris (framework de lógica de separación concurrente), MathComp — cualquier caso de seguridad construido sobre una prueba de Rocq es inválido si el entorno de pruebas tenía esta desincronización de la flag.
• Código con pruebas adjuntas (proof-carrying code): un archivo .v malicioso en una dependencia puede introducir silenciosamente declaraciones no sólidas de las que dependen las pruebas posteriores.
• Contratos inteligentes: los proyectos que usan Rocq para el desarrollo verificado de contratos inteligentes (por ejemplo, ConCert) podrían ver anuladas sus garantías de seguridad.

Detalles técnicos

Causa raíz

El grafo de universos (ugraph) en el kernel contiene su propia copia de la flag Universe Checking. Cuando un módulo usa Local Unset Universe Checking, la flag se modifica tanto en el estado global como en el ugraph. Cuando el módulo se cierra, el estado global se restaura desde el estado guardado del módulo, pero la copia del ugraph no se sincroniza, dejando la comprobación de universos efectivamente deshabilitada.

Flujo del ataque

┌─────────────────────────────────────────────────────┐
│ 1. Universes u v.  Constraint u < v.                │
│    → Declare universes with strict ordering          │
├─────────────────────────────────────────────────────┤
│ 2. Module Off.                                       │
│      Local Unset Universe Checking.                  │
│    End Off.                                          │
│    → ugraph flag stays OFF after module closes        │
├─────────────────────────────────────────────────────┤
│ 3. Test Universe Checking.  → reports "on" (LIE)     │
├─────────────────────────────────────────────────────┤
│ 4. eapply TypeNeqSmallType.paradox; reflexivity.     │
│    → Kernel accepts universe-inconsistent proof       │
│    → False proved with no axioms                     │
├─────────────────────────────────────────────────────┤
│ 5. zero_eq_one : 0 = 1                              │
│    → Derived via exfalso                             │
└─────────────────────────────────────────────────────┘

Comparación con errores del kernel de Lean 4

Aspecto	Rocq #22287 (este error)	Lean #14484	Lean #14576
Asistente de pruebas	Rocq (Coq)	Lean 4	Lean 4
Clase de error	Desincronización de estado en el sistema de módulos	Envenenamiento de la caché de inferencia	Confusión de tipos mediante proyecciones
Complejidad del exploit	6 líneas	~20 líneas	~50 líneas
Sistema de universos/tipos	Verificación de universos eludida	FVar opaco aceptado	Parámetros fantasma escapan
Estado de la corrección	Abierto	Corregido (PR #14498)	Corregido (PR #14577)

Créditos

• Descubrimiento del error: Gaëtan Gilbert (@SkySkimmer)
• Empaquetado del PoC: Jonathan Brossard (@endrazine)