CVE-2026-72704
Rocq Prover até 9.2.0 Guard Checker confia em árvore recursiva corrompida após transporte
- Publicado
- 24 de ago. de 2026
- Atualizado
- 26 de out. de 2026
- Atribuindo CNA
- VulnCheck
- Evidência observada
- 26 de out. de 2026
CVSS primário
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
- Percentil
- 7,1%
- Data do modelo
- 25 de out. de 2026
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.
Resumo
O verificador de guarda no Rocq Prover não revalida a representação em árvore recursiva de um parâmetro de tipo indutivo depois que esse parâmetro foi alterado por transporte. Um ponto fixo pode aplicar uma reescrita ao longo de uma igualdade entre tipos ao seu argumento recursivo, o que o verificador de guarda aceita porque o tipo indutivo é preservado, enquanto a árvore recursiva registrada para o parâmetro é alterada. Um segundo ponto fixo que chama o primeiro herda a árvore recursiva alterada sem verificação, de modo que uma chamada que não é estruturalmente decrescente é aceita como terminante. A definição não terminante resultante prova que um número natural é igual ao seu próprio sucessor e, portanto, False, do qual qualquer proposição se segue. A demonstração usa dois axiomas que decorrem da univalência e são consistentes com o cálculo de construções indutivas, de modo que a contradição vem da verificação de guarda e não das suposições. Uma correção é proposta, mas não integrada.
Fontes
CVE-2026-72704 — O verificador Rocq Guard confia em árvore recursiva corrompida após transporte
Uso responsável
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.