CVE-2026-72704
Vulnérabilité moyenne dans rocq (rocq-prover)
Description
The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because the inductive type is preserved, while the recursive tree recorded for the parameter is altered. A second fixpoint that calls the first inherits the altered recursive tree without verification, so a call that is not structurally decreasing is accepted as terminating. The resulting non-terminating definition proves that a natural number equals its own successor and therefore False, from which any proposition follows. The demonstration uses two axioms that follow from univalence and are consistent with the calculus of inductive constructions, so the contradiction comes from the guard check rather than from the assumptions. A fix is proposed but not merged.
Gravité et risque d'exploitation
CVE-2026-72704 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 6.7 % des CVE référencées.
Que faire ?
- Vérifiez si rocq (versions 0, <=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.