CVE-2026-72714
Description
A flaw was found in Rocq Prover. When a module that locally disabled the universe checking flag is closed, the prover fails to restore the universe graph's copy of this flag. This desynchronization allows the kernel to accept terms that are inconsistent with the universe, even though the system reports the check as enabled. A local user can exploit this to construct a proof of False, which can then be used to derive any proposition, leading to a critical integrity bypass or arbitrary code execution within the prover.
Statement
Red Hat Product Security has determined that this vulnerability does not affect any currently supported Red Hat product. This assessment may evolve based on further analysis and discovery. For more information about this vulnerability and the products it affects, please see the linked references.
Mitigation
Mitigation for this issue is either not available or the currently available options do not meet the Red Hat Product Security criteria comprising ease of use and deployment, applicability to widespread installation base, or stability.
Understanding the Weakness (CWE)
Integrity,Other
Technical Impact: Alter Execution Logic; Unexpected State
The attacker can gain access to otherwise unauthorized resources.
Integrity,Other
Technical Impact: Modify Application Data; Modify Files or Directories; Modify Memory; Other
Race conditions such as this kind may be employed to gain read or write access to resources which are not normally readable or writable by the user in question.
Integrity,Other
Technical Impact: Other
The resource in question, or other resources (through the corrupted one), may be changed in undesirable ways by a malicious user.
Non-Repudiation
Technical Impact: Hide Activities
If a file or other resource is written in this method, as opposed to in a valid way, logging of the activity may not occur.
Non-Repudiation,Other
Technical Impact: Other
In some cases it may be possible to delete files a malicious user might not otherwise have access to, such as log files.
Other
Technical Impact: Unexpected State
The product may perform invalid actions when the resource is in an unexpected state.
Frequently Asked Questions
Not sure what something means? Check out our Security Glossary.
Want to get errata notifications? Sign up here.
