CVE-2026-72714 — Verificação de Universos do Rocq Dessincronizada Após o Fechamento de Módulo

Provando 0 = 1 sem axiomas por meio da dessincronização da flag de verificação de universos no escopo de módulo.

Campo	Valor
Relatório de bug	rocq-prover/rocq#22287
Correção	Nenhuma (issue aberta em 2026-08-16)
Afetado	Rocq ≤ 9.2.0 / Coq 8.x (todas as versões com Hurkens na stdlib)
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1
CWE	CWE-488 (Exposição de Elemento de Dados à Sessão Errada), CWE-20 (Validação de Entrada Imprópria)
CVE	CVE-2026-72714

Resumo da Vulnerabilidade

O sistema de módulos do Rocq Prover falha em delimitar corretamente o escopo da flag Local Unset Universe Checking. Quando usada dentro de um módulo, a flag deveria ser restaurada ao seu estado anterior quando o módulo é fechado. No entanto, o grafo de universos (ugraph) mantém sua própria cópia da flag, que fica dessincronizada com o estado global no fechamento do módulo.

Após a dessincronização:

• Test Universe Checking reporta ativado (a flag global foi restaurada)
• O ugraph ainda tem a verificação de universos desativada (sua cópia não foi restaurada)
• O kernel, portanto, aceita termos inconsistentes em universos sem erro

Com a verificação de universos efetivamente desativada, o paradoxo de Hurkens se aplica: TypeNeqSmallType.paradox explora o fato de que Type@{u} e Type@{v} com u < v podem ser confundidos quando as restrições de universos não são impostas, produzindo uma prova direta de False.

O exploit:

• Não usa axiomas, plugins ou recursos inseguros
• Print Assumptions reporta "Closed under the global context"
• Requer apenas Stdlib.Logic.Hurkens (parte da biblioteca padrão)
• Tem 6 linhas de código de prova

Uso

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

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

[*] Compiling ZeroEqOne.v ...
Universe Checking is on.
bad is defined
Closed under the global context
zero_eq_one is defined
Closed under the global context

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms (closed under the global context)

    Bug class:  Universe checking state desync (CWE-488)
    Root cause: ugraph retains stale Local Unset Universe Checking flag
    Bug report: https://github.com/rocq-prover/rocq/issues/22287

Impacto

Qualquer sistema que confie nas provas verificadas pelo kernel do Rocq é afetado:

• Software formalmente verificado: CompCert (compilador C verificado), CertiKOS (kernel de SO verificado), Iris (framework de lógica de separação concorrente), MathComp — qualquer argumento de segurança construído sobre uma prova Rocq é inválido se o ambiente de prova tiver esse dessincronização de flag.
• Código com prova embutida: um arquivo .v malicioso em uma dependência pode introduzir silenciosamente declarações não sólidas das quais provas subsequentes dependem.
• Contratos inteligentes: projetos que usam Rocq para desenvolvimento verificado de contratos inteligentes (por exemplo, ConCert) podem ter suas garantias de segurança anuladas.

Detalhes Técnicos

Causa Raiz

O grafo de universos (ugraph) no kernel contém sua própria cópia da flag Universe Checking. Quando um módulo usa Local Unset Universe Checking, a flag é modificada tanto no estado global quanto no ugraph. Quando o módulo é fechado, o estado global é restaurado a partir do estado salvo do módulo, mas a cópia do ugraph não é sincronizada, deixando a verificação de universos efetivamente desativada.

Fluxo de Ataque

┌─────────────────────────────────────────────────────┐
│ 1. Universes u v.  Constraint u < v.                │
│    → Declare universes with strict ordering          │
├─────────────────────────────────────────────────────┤
│ 2. Module Off.                                       │
│      Local Unset Universe Checking.                  │
│    End Off.                                          │
│    → ugraph flag stays OFF after module closes        │
├─────────────────────────────────────────────────────┤
│ 3. Test Universe Checking.  → reports "on" (LIE)     │
├─────────────────────────────────────────────────────┤
│ 4. eapply TypeNeqSmallType.paradox; reflexivity.     │
│    → Kernel accepts universe-inconsistent proof       │
│    → False proved with no axioms                     │
├─────────────────────────────────────────────────────┤
│ 5. zero_eq_one : 0 = 1                              │
│    → Derived via exfalso                             │
└─────────────────────────────────────────────────────┘

Comparação com bugs do kernel do Lean 4

Aspecto	Rocq #22287 (este bug)	Lean #14484	Lean #14576
Assistente de provas	Rocq (Coq)	Lean 4	Lean 4
Classe do bug	Dessincronização de estado no sistema de módulos	Envenenamento de cache de inferência	Confusão de tipos via projeções
Complexidade do exploit	6 linhas	~20 linhas	~50 linhas
Sistema de universos/tipos	Verificação de universos contornada	FVar opaco aceito	Parâmetros fantasma escapam
Status da correção	Aberto	Corrigido (PR #14498)	Corrigido (PR #14577)

Créditos

• Descoberta do bug: Gaëtan Gilbert (@SkySkimmer)
• Empacotamento do PoC: Jonathan Brossard (@endrazine)