Description

The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.

Executive Summary

Technical Details

Mitigations

References

Additional Metadata

{
  "score": "6.3",
  "pubDate": "2026-08-24T20:17:18.240Z",
  "pubdate": "2026-08-24T20:17:18.240Z",
  "executiveSummary": "A logic soundness vulnerability exists in the guard checker of the Rocq Prover, specifically within the mutual fixpoint parameter uniformity analysis. The flaw allows the admission of non-terminating definitions as structurally decreasing due to incorrect handling of parameters in nested mutual fixpoints.\nThe primary impact of this vulnerability is the breakdown of logical consistency, leading to the derivation of a proof of False from which any arbitrary proposition can be proven. This undermines the core security guarantee of the theorem prover, which relies on the strict enforcement of termination for all recursive definitions.\nThe vulnerability affects Rocq Prover (formerly Coq) version 8.20 and is resolved in version 9.2.0. The attack vector is entirely internal to the proof assistant language, requiring no network exposure, authentication, or special privileges.\nAn attacker can exploit this flaw using standard proof scripts without utilizing axioms, plugins, or unsafe flags. The resulting inconsistent term is certified as closed under the global context by Print Assumptions, posing severe risks to the integrity of formally verified software and mathematical proofs.",
  "technicalDetails": "The root cause of the vulnerability resides in the function find_uniform_parameters located in kernel/inductive.ml. When evaluating nested mutual fixpoints, the guard checker incorrectly assumes that a parameter is uniform without examining cross-calls between the different bodies of the fixpoint.\nSpecifically, find_uniform_parameters exclusively inspects self-recursive calls. If an individual body within the mutual fixpoint does not call itself directly, the function concludes that all of its parameters are uniform, even if cross-calls exist between different bodies of the same fixpoint.\nConsequently, a parameter that structurally grows via a cross-call from one body to another improperly retains the subterm specification inherited from the enclosing fixpoint. When a recursive call is subsequently guarded by this invalid specification, the guard checker accepts the argument as structurally smaller than the input, despite it not actually decreasing.\nThis logic failure permits the admission of non-terminating definitions into the environment under the false classification of being structurally decreasing. Step-by-step exploitation proceeds by constructing a mutual fixpoint where parameters grow across bodies without self-calls, tricking the kernel into accepting an infinite loop or unbounded recursion.\nThis violation of termination checking results in the construction of a term whose value evaluates to its own successor. Applying standard paradoxes or cyclic evaluation over this term yields a proof of False. Because the proof relies solely on kernel-level evaluation flaws, Print Assumptions reports the resulting term as closed under the global context without flagging any usage of axioms or unsafe extensions."
}