CVE-2026-72705
Rocq Prover precedente alla 9.2.0: il Guard Checker accetta un fixpoint passato come argomento di ordine superiore
- Pubblicato
- 24 ago 2026
- Aggiornato
- 26 ott 2026
- Assegnazione CNA
- VulnCheck
- Evidenza osservata
- 26 ott 2026
CVSS primario
nvd · CVSS 4.0
CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:XBasso · prossimi 30 giorni
- Percentile
- 7,1%
- Data del modello
- 27 ott 2026
L'EPSS è una stima statistica, non una certezza o una misura di impatto. Combinalo con CVSS, stato KEV, esposizione e ambiente.
Riepilogo
Il controllo di guardia in Rocq Prover non segue le chiamate ricorsive effettuate tramite gli argomenti di un fixpoint stesso. Un fixpoint può passare se stesso come argomento di ordine superiore a un secondo fixpoint, che poi lo applica a un valore che non è un sottermine dell'argomento strutturale. Passare la funzione ricorsiva a una definizione semplice viene rifiutato perché il controllo srotola la definizione e osserva la chiamata, ma passarla a un fixpoint viene accettato perché le chiamate ricorsive di ordine superiore tramite gli argomenti di un fixpoint non vengono tracciate. Ciò ammette un tipo che è definizionalmente uguale alla propria negazione, cosicché l'auto-applicazione produce False in codice puramente definizionale, senza tattiche, assiomi, plugin o flag unsafe, e Print Assumptions riporta il risultato come chiuso rispetto al contesto globale. Corretto in Rocq 9.2.0.
Fonti
CVE-2026-72705 — Rocq Guard Checker accetta un fixpoint passato come argomento di ordine superiore
Utilizzo responsabile
Utilizza le informazioni sulla vulnerabilità solo sui sistemi che possiedi o che sei autorizzato a testare. Kitploit si collega ai metadati della ricerca pubblica e non memorizza codici exploit o payload dannosi.