CVE-2026-72704 — O verificador de guarda do Rocq confia em árvore recursiva corrompida após transporte

Provando 0 = 1 a partir de axiomas consistentes por meio da corrupção da árvore recursiva do ponto fixo do verificador de guarda.

Campo	Valor
Relatório de bug	rocq-prover/rocq#22024
Correção	PR #22027 (aberto)
Afetado	Rocq ≤ 9.2.0 / Coq 8.x (todas as versões com verificador de guarda)
CVSS 3.1	`AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — 7.1
CWE	CWE-670 (Implementação de fluxo de controle sempre incorreta)
CVE	CVE-2026-72704

Resumo da vulnerabilidade

O verificador de guarda do Rocq Prover (verificador de terminação para pontos fixos) falha em reverificar a representação de árvore recursiva dos argumentos de tipos indutivos quando eles são modificados por meio de transporte (rew). Um ponto fixo pode corromper silenciosamente a árvore recursiva para um parâmetro de tipo de um indutivo, e um segundo ponto fixo que chama o primeiro confiará na árvore recursiva corrompida sem verificação, aceitando uma definição não terminante como estruturalmente decrescente.

O exploit usa dois axiomas que são consistentes com CIC — eles são consequências diretas do axioma da univalência (a bijeção que troca 0↔1 fornece um caminho nat = nat em Type ao longo do qual o transporte envia 0 para 1). Um verificador de guarda sólido não deve derivar False a partir de axiomas consistentes.

O exploit:

Usa apenas dois axiomas consistentes (consequências da univalência)
Print Assumptions relata apenas esses dois axiomas — nenhum False, nenhum sorry
Sem plugins, recursos inseguros ou manipulação de universos
O verificador de guarda é a única fonte de inconsistência

Uso

docker build -t rocq-cve-poc-22024 .
docker run --rm rocq-cve-poc-22024

Saída esperada em uma versão vulnerável do Rocq:

[*] Compiling ZeroEqOne.v with rocq compile ...

zero_eq_one is defined
Axioms:
e : nat = nat
e1 : rew [fun T : Type => T] e in 0 = 1

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Axioms used: e (nat = nat), e1 (transport sends 0 to 1)
    These axioms are consistent (consequences of univalence).
    A sound guard checker must not derive False from them.

    Bug class:  Guard checker rectree corruption (CWE-670)
    Root cause: fixpoints can alter rectrees via transport; nested
                fixpoints trust the corrupted rectree without recheck
    Bug report: https://github.com/rocq-prover/rocq/issues/22024

Impacto

Qualquer sistema que confie nas provas verificadas pelo kernel do Rocq e use axiomas consistentes com a univalência é afetado:

Desenvolvimentos HoTT: qualquer projeto Rocq que use o axioma da univalência (ou extensionalidade proposicional, que pode desencadear a mesma classe de bug) pode ter seus pontos fixos verificados pelo guard checker aceitos silenciosamente, apesar da não terminação.
Software formalmente verificado: CompCert, CertiKOS, Iris e qualquer projeto que adicione axiomas personalizados consistentes com CIC está em risco se o guard checker for a única garantia de terminação.
Código com prova embutida: uma dependência maliciosa pode introduzir os dois axiomas e o ponto fixo corrompido, e então usar False a jusante.

Detalhes Técnicos

O Bug do Guard Checker

O guard checker do Rocq verifica se os pontos fixos são estruturalmente decrescentes construindo uma rectree — uma árvore que rastreia quais subtermos do argumento recursivo estão disponíveis em cada chamada recursiva. O bug é uma falha em duas etapas:

Corrupção da rectree: weird é um ponto fixo sobre Box A que aplica rew [Box] e (transporte ao longo de e : A = A) ao argumento recursivo no caso wrap. O guard checker aceita isso porque o transporte preserva o tipo indutivo Box, mas a rectree para o parâmetro A é silenciosamente alterada — após o transporte, o modelo interno do guard checker não rastreia mais com precisão quais valores fluem através de A.
Confiança não verificada: loop chama weird loop e (wrap _ (box _ n)). O guard checker verifica as próprias chamadas recursivas de loop, mas confia na rectree de weird para a chamada aninhada. Como a rectree de weird foi corrompida pelo transporte, o guard checker conclui incorretamente que loop é estruturalmente decrescente.

A Contradição

Com o guard checker enganado, loop é aceito apesar de ser não terminante. A prova então mostra:

loop 1 = S (loop 1)

ao desdobrar loop e weird, e usando e1 para mostrar que o transporte envia box nat 0 para box nat 1, que realimenta loop. Como ∀ n, n ≠ S n é demonstrável por indução, loop 1 = S (loop 1) produz False, e a partir dele 0 = 1.

Por que os Axiomas São Consistentes

Os dois axiomas:

e  : nat = nat :> Type
e1 : rew [fun T => T] e in 0 = 1

são consequências do axioma da univalência. Sob univalência, qualquer bijeção f : nat → nat fornece um caminho nat = nat em Type, e o transporte ao longo desse caminho age como f. A bijeção swap01 que envia 0↦1, 1↦0 e n↦n para n≥2 é uma tal bijeção, com swap01 0 = 1 testemunhando e1.

Sabe-se que a univalência é consistente com o CIC (validada por modelos de teoria de tipos cúbica). Portanto, esses axiomas não podem ser a fonte da contradição — o verificador de guarda é.

Comparação com outros PoCs

Aspecto	Rocq #22024 (este bug)	Rocq #22287	Lean #14484
Classe do bug	Corrupção da árvore de recursão no verificador de guarda	Dessincronização do estado de verificação de universos	Envenenamento do cache de inferência
Axiomas necessários	2 (consistentes com univalência)	Nenhum	Nenhum
Complexidade do exploit	~30 linhas	6 linhas	~20 linhas
Componente	Verificador de guarda (fixpoint)	Sistema de módulos (flag ugraph)	Verificador de tipos (declaração opaca)
Status da correção	PR #22027 (aberto)	Aberto	Corrigido (PR #14498)

Créditos

Descoberta do bug: Yann Leray (@yannl35133)
Empacotamento do PoC: Jonathan Brossard (@endrazine)

rocq-cve-poc-22024

Mais Populares