rocq-prover Rocq bis 9.1.x Guard Checker kernel/inductive.ml find_uniform_parameters erweiterte Rechte

CVSS Meta Temp ScoreAktueller Exploitpreis (≈)CTI Interest Score
5.2$0-$5k0.99+

Zusammenfassunginfo

In rocq-prover Rocq bis 9.1.x wurde eine problematische Schwachstelle ausgemacht. Betroffen ist die Funktion find_uniform_parameters der Datei kernel/inductive.ml der Komponente Guard Checker. Mittels dem Manipulieren mit unbekannten Daten kann eine erweiterte Rechte-Schwachstelle ausgenutzt werden. Diese Schwachstelle trägt die Bezeichnung CVE-2026-72703. Es ist möglich, den Angriff aus der Ferne durchzuführen. Es gibt keinen verfügbaren Exploit.

Detailsinfo

Es wurde eine problematische Schwachstelle in rocq-prover Rocq bis 9.1.x ausgemacht. Dabei betrifft es die Funktion find_uniform_parameters der Datei kernel/inductive.ml der Komponente Guard Checker. Mittels Manipulieren mit einer unbekannten Eingabe kann eine erweiterte Rechte-Schwachstelle ausgenutzt werden. Im Rahmen von CWE wurde eine Klassifizierung als CWE-20 vorgenommen. Dies wirkt sich aus auf die Integrität. CVE fasst zusammen:

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.

Auf github.com kann das Advisory eingesehen werden. Die Verwundbarkeit wird seit dem 10.08.2026 unter CVE-2026-72703 geführt. Das Ausnutzen gilt als leicht. Der Angriff kann über das Netzwerk erfolgen. Zur Ausnutzung ist keine spezifische Authentisierung erforderlich. Es wird vorausgesetzt, dass das Opfer eine spezifische Handlung vornimmt. Es sind zwar technische Details, jedoch kein verfügbarer Exploit zur Schwachstelle bekannt.

Ein Upgrade auf die Version 9.2.0 vermag dieses Problem zu beheben.

If you want to get best quality of vulnerability data, you may have to visit VulDB.

Produktinfo

Hersteller

Name

Version

CPE 2.3info

CPE 2.2info

CVSSv4info

VulDB Vector: 🔒
VulDB Zuverlässigkeit: 🔍

CNA CVSS-B Score: 🔒
CNA CVSS-BT Score: 🔒
CNA Vector: 🔒

CVSSv3info

VulDB Meta Base Score: 5.3
VulDB Meta Temp Score: 5.2

VulDB Base Score: 4.3
VulDB Temp Score: 4.1
VulDB Vector: 🔒
VulDB Zuverlässigkeit: 🔍

CNA Base Score: 6.3
CNA Vector (VulnCheck): 🔒

CVSSv2info

AVACAuCIA
💳💳💳💳💳💳
💳💳💳💳💳💳
💳💳💳💳💳💳
VektorKomplexitätAuthentisierungVertraulichkeitIntegritätVerfügbarkeit
freischaltenfreischaltenfreischaltenfreischaltenfreischaltenfreischalten
freischaltenfreischaltenfreischaltenfreischaltenfreischaltenfreischalten
freischaltenfreischaltenfreischaltenfreischaltenfreischaltenfreischalten

VulDB Base Score: 🔒
VulDB Temp Score: 🔒
VulDB Zuverlässigkeit: 🔍

Exploitinginfo

Klasse: Erweiterte Rechte
CWE: CWE-20
CAPEC: 🔒
ATT&CK: 🔒

Physisch: Teilweise
Lokal: Ja
Remote: Ja

Verfügbarkeit: 🔒
Status: Nicht definiert
Preisentwicklung: 🔍
Aktuelle Preisschätzung: 🔒

0-Dayfreischaltenfreischaltenfreischaltenfreischalten
Heutefreischaltenfreischaltenfreischaltenfreischalten

Threat Intelligenceinfo

Interesse: 🔍
Aktive Akteure: 🔍
Aktive APT Gruppen: 🔍

Gegenmassnahmeninfo

Empfehlung: Upgrade
Status: 🔍

0-Day Time: 🔒

Upgrade: Rocq 9.2.0

Timelineinfo

10.08.2026 CVE zugewiesen
24.08.2026 +14 Tage Advisory veröffentlicht
24.08.2026 +0 Tage VulDB Eintrag erstellt
24.08.2026 +0 Tage VulDB Eintrag letzte Aktualisierung

Quelleninfo

Advisory: github.com
Status: Bestätigt

CVE: CVE-2026-72703 (🔒)
GCVE (CVE): GCVE-0-2026-72703
GCVE (VulDB): GCVE-100-394818

Eintraginfo

Erstellt: 24.08.2026 22:24
Anpassungen: 24.08.2026 22:24 (78)
Komplett: 🔍
Cache ID: 216::103

If you want to get best quality of vulnerability data, you may have to visit VulDB.

Diskussion

Bisher keine Kommentare. Sprachen: de + en.

Bitte loggen Sie sich ein, um kommentieren zu können.

Are you interested in using VulDB?

Download the whitepaper to learn more about our service!