CVE-2020-37268

Riepilogo

Print Assumptions non segnala che una definizione è stata prodotta mentre il controllo degli universi era disabilitato quando tale definizione raggiunge il chiamante tramite Parameter Inline in un module type. L'applicazione di un funtore inlinea il corpo del parametro, e l'inlining elimina il record che il termine era stato costruito sotto Unset Universe Checking, quindi la costante risultante non porta alcuna traccia dell'operazione non sicura. Un'implementazione di modulo può pertanto dimostrare False sfruttando un'incoerenza degli universi, esporla tramite un parametro inlineato e far sì che Print Assumptions riporti la dimostrazione dipendente come chiusa rispetto al contesto globale. Poiché Print Assumptions è l'audit in-process utilizzato per confermare che uno sviluppo non si basi su assunzioni inattese, una dipendenza costruita in questo modo supera tale audit pur dimostrando proposizioni arbitrarie. Il checker standalone coqchk rifiuta invece il file compilato risultante. Il progetto documenta questo problema in dev/doc/critical-bugs.md tra i bug non corretti e valuta il rischio come moderato quando coqchk non viene utilizzato.

Fonti

• rocq-cve-poc-12155PoC

  CVE-2020-37268 — Rocq/Coq Print Assumptions omette il controllo unsafe delle universe tramite Parameter Inline