endrazine/rocq-cve-poc-12155CVE-2020-37268 — Rocq/Coq Print Assumptions omite la comprobación de universos insegura mediante Parameter Inline
Eludiendo la auditoría de pruebas mediante la inserción (inlining) de funtores de módulos — sin corregir desde 2020.
Print Assumptions no informa de que una definición se construyó con la
comprobación de universos deshabilitada cuando esa definición llega al
llamador a través de Parameter Inline en un tipo de módulo. La aplicación
de funtores inserta el cuerpo del parámetro y descarta el registro del
contexto Unset Universe Checking, por lo que la constante resultante no
muestra ningún indicio de la operación insegura.
Un módulo puede, por tanto, usar una inconsistencia de universos para
demostrar False, y Print Assumptions informa de la prueba dependiente
como cerrada bajo el contexto global — sin axiomas, sin indicadores de
inseguridad visibles.
coqchk sí rechaza el archivo .vo compilado resultante, pero la auditoría
de suposiciones en proceso (Print Assumptions) no detecta el problema.
docker build -t rocq-cve-poc-12155 .
docker run --rm rocq-cve-poc-12155
En una versión vulnerable (Rocq 8.11 – 9.2.0, y todas las Coq 8.x con el
sistema de módulos), la salida confirma la prueba de 0 = 1 con Print Assumptions informando de ella como cerrada.
Cualquier flujo de trabajo que dependa de Print Assumptions como única
comprobación de integridad puede verse afectado:
.v
malicioso en una dependencia podría introducir declaraciones no sólidas
que superen la auditoría de suposicionescoqchk sobre la
salida compiladaCuando un tipo de módulo declara Parameter Inline, la aplicación de
funtores inserta el cuerpo del parámetro en el contexto llamador. Esta
inserción descarta los metadatos que registran que la definición original se
produjo bajo Unset Universe Checking. Por tanto, el grafo de universos
acepta restricciones de universos inconsistentes procedentes del cuerpo
insertado, y Print Assumptions no ve ningún rastro del contexto inseguro.
El fallo está abierto desde 2020 (incidencia de Coq #12155) y está
documentado en el archivo dev/doc/critical-bugs.md del proyecto. No se ha
fusionado ninguna corrección a fecha de Rocq 9.2.0.
| Campo | Valor |
|---|---|
| CVE | CVE-2020-37268 |
| 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-778 — Registro insuficiente |
| Producto | Afectadas | Corregida |
|---|---|---|
| Coq | 8.11 – 8.20 | Sin corregir |
| Rocq Prover | 8.20 – 9.2.0 | Sin corregir |
coqchk sobre todos los archivos .vo compilados antes de
confiar en las pruebas en producción. coqchk detecta la inconsistencia
de universos que Print Assumptions pasa por alto.Parameter Inline que se haya compilado bajo Unset Universe Checking.| Informe de error | rocq-prover/rocq#12155 |
| Documento de errores críticos | dev/doc/critical-bugs.md |
| Aviso de VulnCheck | vulncheck.com |
| Fecha | Evento |
|---|---|
| 2020 | Error reportado por Jason Gross (coq/coq#12155) |
| 2020–2026 | El error permanece abierto, documentado en critical-bugs.md |
| 2026-08-24 | CVE-2020-37268 publicado por VulnCheck |
| 2026-08-24 | PoC reproducible con Docker publicado |