Back to feed
19Track

Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport

rocq-prover rocq · CVE-2026-72704
0 news outlets0 CERTs and agencies1 research labs

Assessment: Track

SSVC decision points: exploitation poc, automatable no, technical impact partial, deployment low.

What is it?

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.

Evidence

Technical advisories1Detailed write-ups from security research teams

Exploitation

  • Exploit code published (not verified by us)
  • Exploited in the wild (confirmed by a source)
  • Listed as known exploited (CISA KEV)
CVSS
6.3
EPSS
–
First seen
1 h ago
Status
corroborated

All rocq-prover vulnerabilities