CVE-2020-37268

Resumen

Print Assumptions no informa que una definición se produjo mientras la comprobación de universos estaba deshabilitada cuando esa definición llega al llamador a través de Parameter Inline en un tipo de módulo. Aplicar un funtor inserta el cuerpo del parámetro, y la inserción descarta el registro de que el término se construyó bajo Unset Universe Checking, por lo que la constante resultante no conserva rastro de la operación insegura. Una implementación de módulo puede, por tanto, demostrar False usando una inconsistencia de universos, exponerla a través de un parámetro insertado, y hacer que Print Assumptions informe la prueba dependiente como cerrada bajo el contexto global. Dado que Print Assumptions es la auditoría en proceso usada para confirmar que un desarrollo no se apoya en suposiciones inesperadas, una dependencia construida de esta manera pasa esa auditoría mientras demuestra proposiciones arbitrarias. El verificador independiente coqchk sí rechaza el archivo compilado resultante. El proyecto registra esto en dev/doc/critical-bugs.md bajo errores no corregidos y califica el riesgo como moderado cuando no se usa coqchk.

Fuentes

• rocq-cve-poc-12155PoC

  CVE-2020-37268 — Rocq/Coq Print Assumptions omite la comprobación de universos insegura mediante Parameter Inline