Description

The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. Fixed in Rocq 9.2.0.

Executive Summary

Technical Details

Mitigations

References

Additional Metadata

{
  "score": "6.3",
  "pubDate": "2026-08-24T20:17:18.520Z",
  "pubdate": "2026-08-24T20:17:18.520Z",
  "executiveSummary": "An algorithmic flaw exists within the guard checker of the Rocq Prover, specifically related to the tracking of recursive calls made through higher-order fixpoint arguments. This vulnerability permits the construction of a type that is definitionally equal to its own negation.\nThe impact of this flaw is severe, allowing the derivation of False in purely definitional code without requiring tactics, axioms, plugins, or unsafe flags. The system incorrectly evaluates the term as closed under the global context during Print Assumptions evaluations.\nAffected systems include the Rocq Prover prior to version 9.2.0. The vulnerability stems from insufficient tracking of recursive functions when passed as higher-order arguments to secondary fixpoints, bypassing standard termination checks.\nAttackers with the capability to write proof definitions in the affected environment can exploit this behavior to compromise logical consistency. No network exposure or authentication is inherently required, as exploitation is driven entirely through crafted input code processed by the prover.",
  "technicalDetails": "The vulnerability resides in the guard checker component of the Rocq Prover, which is responsible for ensuring the termination of fixpoint definitions to maintain logical consistency. The root cause is the failure of the guard checker to follow recursive calls made through a fixpoint's own arguments when passed in a higher-order context.\nSpecifically, when a fixpoint passes itself as a higher-order argument to a second fixpoint, the second fixpoint may apply it to a value that is not a strict subterm of the original structural argument. While passing a recursive function to a plain definition is correctly rejected because the checker unfolds the definition and observes the illicit call, passing it to another fixpoint is erroneously accepted due to untracked higher-order recursive pathways.\nThe step-by-step attack flow involves defining a primary recursive fixpoint, passing this fixpoint as a parameter into a secondary fixpoint, and subsequently applying it to non-subterm values. Because the guard checker fails to track these higher-order argument flows across fixpoint boundaries, the termination invariant is violated.\nThis mechanism admits a type that is definitionally equal to its own negation, facilitating self-application that ultimately yields False within purely definitional code. Consequently, Print Assumptions reports the compromised derivation as closed under the global context.\nThe affected product is Rocq Prover versions prior to 9.2.0. Exploitation requires no privileges, authentication, or network exposure, operating entirely locally through the submission of malformed logical definitions that subvert the structural recursion guarantees."
}