endrazine/rocq-cve-poc-21682CVE-2026-72703 — El verificador Rocq Guard acepta un punto fijo no terminante mediante llamadas cruzadas no verificadas
Demostración de 0 = 1 sin axiomas mediante la omisión de parámetros uniformes en el verificador de guardas.
El verificador de guardas del kernel de Rocq (verificador de terminación de puntos fijos) trata todos los parámetros de un punto fijo mutuo anidado como uniformes sin examinar las llamadas entre los cuerpos del punto fijo. La función find_uniform_parameters en kernel/inductive.ml solo inspecciona las llamadas autorrecursivas; cuando ningún cuerpo se llama a sí mismo, todos los parámetros se consideran uniformes. Un parámetro que crece a través de una llamada cruzada puede entonces conservar una especificación de subtermo incorrecta, y se acepta una llamada recursiva aunque su argumento no sea estructuralmente menor.
Esto permite una definición no terminante que demuestra False, de la cual se sigue cualquier proposición, incluida 0 = 1.
La prueba no requiere axiomas, tácticas, plugins ni indicadores inseguros. Print Assumptions la reporta como cerrada bajo el contexto global.
docker build -t rocq-cve-poc-21682 .
docker run --rm rocq-cve-poc-21682
En una versión vulnerable (Rocq 8.20 – <9.2.0), la salida confirma la prueba de 0 = 1 sin axiomas.
En una versión parcheada (Rocq ≥9.2.0), el verificador de guardas rechaza el punto fijo.
Cualquier sistema que dependa de pruebas verificadas por el kernel de Rocq/Coq puede verse afectado si se ejecuta en una versión vulnerable sin mitigaciones adicionales:
.v malicioso en una dependencia podría introducir declaraciones no sólidasfind_uniform_parameters en kernel/inductive.ml solo inspecciona las llamadas autorrecursivas dentro de cada cuerpo de un punto fijo mutuo. Cuando ningún cuerpo contiene una llamada autorrecursiva (todas las llamadas son cruzadas entre cuerpos), todos los parámetros se marcan como uniformes. Un parámetro que en realidad varía entre llamadas cruzadas conserva una especificación de subtermo incorrecta, lo que permite al verificador de guardas aceptar una llamada recursiva sobre un argumento que no decrece estructuralmente.
| Campo | Valor |
|---|---|
| CVE | CVE-2026-72703 |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (Alta) |
| CVSS 4.0 | AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N — 6.8 (Media) |
| CWE | CWE-670 — Implementación de flujo de control siempre incorrecta |
| Producto | Afectadas | Corregidas |
|---|---|---|
| Rocq Prover | 8.20 – <9.2.0 | 9.2.0 |
coqchk sobre los archivos .vo compilados como medida de defensa en profundidad.| Informe de error | rocq-prover/rocq#21682 |
| Corrección | rocq-prover/rocq#21684 |
| Aviso de VulnCheck | vulncheck.com |
| Fecha | Evento |
|---|---|
| 2025 | Error reportado (rocq-prover/rocq#21682) |
| 2025 | Corrección fusionada (PR #21684) en Rocq 9.2.0 |
| 2026-08-24 | CVE-2026-72703 publicado por VulnCheck |
| 2026-08-24 | PoC reproducible con Docker publicado |