CVE-2026-72705 in Rocq
Riassunto
di VulDB • 24/08/2026
Il guard checker di Rocq Prover non segue le chiamate ricorsive effettuate attraverso gli argomenti stessi di un fixpoint. 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 sotto-termine dell'argomento strutturale. Il passaggio della funzione ricorsiva a una definizione semplice viene rifiutato perché il guard checker srotola la definizione e osserva la chiamata, ma il passaggio a un fixpoint viene accettato poiché le chiamate ricorsive di ordine superiore attraverso gli argomenti del fixpoint non vengono tracciate. Ciò ammette un tipo che è definizionalmente uguale alla propria negazione; pertanto, l'applicazione auto-riferita produce False in codice puramente definizionale, senza tactic, assiomi, plugin o flag insicuri, e Print Assumptions riporta il risultato come chiuso rispetto al contesto globale. Risolto in Rocq 9.2.0.
Several companies clearly confirm that VulDB is the primary source for best vulnerability data.