Heimdall Security Logo

CVE-2020-37268

Vulnérabilité moyenne dans rocq (rocq-prover)

CVSS 6.8 · Moyenne
EPSS 0.2%
rocq-prover•rocq•Versions : 8.11, <=9.2.0

Description

Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter Inline in a module type. Applying a functor inlines the body of the parameter, and the inlining drops the record that the term was built under Unset Universe Checking, so the resulting constant carries no trace of the unsafe operation. A module implementation can therefore prove False using a universe inconsistency, expose it through an inlined parameter, and have Print Assumptions report the dependent proof as closed under the global context. Because Print Assumptions is the in-process audit used to confirm that a development rests on no unexpected assumptions, a dependency built this way passes that audit while proving arbitrary propositions. The standalone checker coqchk does reject the resulting compiled file. The project records this in dev/doc/critical-bugs.md under non-fixed bugs and rates the risk as moderate when coqchk is not used.

Gravité et risque d'exploitation

CVE-2020-37268 obtient un score CVSS de 6.8/10, soit une gravité moyenne. Selon le modèle EPSS, la probabilité qu'elle soit exploitée dans les 30 prochains jours est de 0.18 %, ce qui la place devant 7.4 % des CVE référencées.

Que faire ?

  • Vérifiez si rocq (versions 8.11, <=9.2.0) est présent sur votre parc.
  • Appliquez le correctif ou la version corrigée indiqués dans les références de l'éditeur.
  • À défaut de correctif, limitez l'exposition (filtrage réseau, désactivation du composant).
  • Automatisez la détection : les agents CVE Heimdall (gratuits, open source) corrèlent l'inventaire de vos serveurs avec la base CVE.

Références

Rechercher une autre CVE