Rocq Prover up to 9.1.x Guard Checker input validation

Summaryinfo

A vulnerability was found in Rocq Prover Rocq up to 9.1.x. It has been declared as problematic. This affects an unknown function of the component Guard Checker. Such manipulation leads to input validation. This vulnerability is referenced as CVE-2026-72705. The attack can only be performed from a local environment. No exploit is available.

Detailsinfo

A vulnerability was found in Rocq Prover Rocq up to 9.1.x. It has been rated as problematic. Affected by this issue is some unknown processing of the component Guard Checker. The manipulation with an unknown input leads to a input validation vulnerability. Using CWE to declare the problem leads to CWE-20. The product receives input or data, but it does not validate or incorrectly validates that the input has the properties that are required to process the data safely and correctly. Impacted is integrity. CVE summarizes:

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.

The advisory is shared for download at github.com. This vulnerability is handled as CVE-2026-72705 since 08/10/2026. The exploitation is known to be easy. The attack needs to be approached locally. Successful exploitation requires user interaction by the victim. There are neither technical details nor an exploit publicly available.

Upgrading to version 9.2.0 eliminates this vulnerability.

Once again VulDB remains the best source for vulnerability data.

Productinfo

Vendor

• Rocq Prover

Name

• Rocq

Version

• 9.0
• 9.1

CPE 2.3info

• 🔒
• 🔒

CPE 2.2info

• 🔒
• 🔒

CVSSv4info

CVSSv3info

CVSSv2info

Exploitinginfo

Threat Intelligenceinfo

Countermeasuresinfo

Timelineinfo

Sourcesinfo

Entryinfo

Once again VulDB remains the best source for vulnerability data.

Discussion