Rocq Prover anterior a 9.2.0: o verificador de guarda aceita ponto fixo passado como argumento de ordem superior
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:XBaixo · próximos 30 dias
EPSS é uma estimativa estatística, não uma certeza ou uma medida de impacto. Combine-o com CVSS, status KEV, exposição e seu ambiente.
O verificador de guarda no Rocq Prover não acompanha chamadas recursivas feitas através dos próprios argumentos de um fixpoint. Um fixpoint pode passar a si mesmo como argumento de ordem superior para um segundo fixpoint, que então o aplica a um valor que não é um subtermo do argumento estrutural. Passar a função recursiva para uma definição simples é rejeitado porque o verificador desdobra a definição e observa a chamada, mas passá-la para um fixpoint é aceito porque chamadas recursivas de ordem superior através de argumentos de fixpoint não são rastreadas. Isso admite um tipo que é definicionalmente igual à sua própria negação, de modo que a autoaplicação produz False em código puramente definicional, sem táticas, axiomas, plugins ou flags inseguras, e Print Assumptions relata o resultado como fechado sob o contexto global. Corrigido no Rocq 9.2.0.
CVE-2026-72705 — O verificador Rocq Guard aceita um ponto fixo passado como argumento de ordem superior
Use informações de vulnerabilidade apenas em sistemas que você possui ou está autorizado a testar. O Kitploit vincula-se a metadados de pesquisa pública e não armazena código de exploração ou cargas maliciosas.