runtimeverification/kernel-c-to-rust-spikeEndurecimento dos parsers em C do kernel por meio de reescrita em Rust + fuzzing diferencial + verificação formal. Primeiro alvo: UVC (CVE-2024-53104).
Um parser C do kernel Linux crítico para a segurança pode ser endurecido reescrevendo-o em
Rust, com a reescrita demonstrada como equivalente ao original e depois formalmente
verificada? Este spike executa o ciclo completo sobre um alvo: o parser de descritores
de vídeo UVC (uvc_parse_format/uvc_parse_frame de drivers/media/usb/uvc/,
v7.2-rc2), escolhido por ter carregado duas CVEs independentes de segurança de memória com dezesseis
anos de diferença (CVE-2008-3496, CVE-2024-53104, esta última no catálogo CISA KEV).
Extrair a folha C (c/). A lógica de parsing copiada byte a byte do
kernel; apenas o ambiente foi substituído por stubs (// SPIKE-STUB). Compila para uma
biblioteca com ABI C. A folha extraída inclui a passagem de contagem e a alocação dimensionada,
de modo que a classe de bug da CVE-2024-53104 (o parsing escrevendo além do que a
contagem alocou) é alcançável, não abstraída.
Reescrever em Rust (rust/). A mesma folha de parsing em Rust seguro, mesma ABI C
e struct de resultado. Cada desvio em relação ao C é marcado com // DEVIATION
e documentado.
Fuzzing diferencial (fuzz/). Um harness LibAFL em rustc estável executa
ambas as implementações a partir de uma única entrada e compara as saídas campo a campo.
Resultado: após corrigir uma incompatibilidade de portabilidade em um ponto de
overflow de sinal dependente do compilador, zero divergências em 54.019 execuções com 93% de
cobertura de arestas. No código fiel da v7.2-rc2 nenhum acesso fora dos limites é alcançável
(ambas as CVEs estão corrigidas). Um controle negativo opcional (--features vuln,
espelhado em ambas as linguagens) reintroduz a incompatibilidade da CVE-2024-53104: na
mesma entrada o C faz uma escrita fora dos limites no heap (ASan), o Rust entra em panic
de forma segura. Detalhes: fuzz/RESULTS.md.
Verificação formal (verify/). A folha Rust fiel é extraída via
Charon e Aeneas para Lean 4 sem nenhum sorry no código gerado, e
sem bloqueio por union (diferente do spike do Binder). Dois teoremas, em
verify/VERIFY-REPORT.md e ROADMAP.md:
ok / fail controlado /
não terminação, nunca um resultado de comportamento indefinido): provado, sem sorry.
Isso torna explícita, como uma afirmação verificada, a propriedade de segurança de memória que o
C não possui.sorry, juntamente com dois princípios reutilizáveis de raciocínio de laço do Aeneas e
ausência de divisão para os 5 laços estruturalmente terminantes. O restante se reduz
a um núcleo nomeado de correção funcional de caminhamento posicional (quatro lemas declarados);
veja ROADMAP.md.O ciclo é demonstrado de ponta a ponta em um alvo. A reescrita é mostrada
equivalente ao C por fuzzing diferencial; a diferença de segurança de memória é
tornada concreta pelo controle negativo; o Rust é extraído de forma limpa para Lean e
sua propriedade de segurança total é verificada por máquina. Para o teorema de ausência de panic, o
invariante de contagem (o núcleo da CVE-2024-53104) está provado sem sorry e o
trabalho restante é reduzido a um núcleo nomeado de correção funcional, declarado mas ainda
não provado. O status completo da prova e os lemas em aberto estão em ROADMAP.md.
c/ — a folha C extraída e seus stubsrust/ — a reescrita em Rust segurofuzz/ — o fuzzer diferencial LibAFL, resultados e controle da classe de CVEverify/ — extração Charon/Aeneas/Lean e teoremasROADMAP.md — status da prova e os lemas em aberto restantesOPEN_CHALLENGES.md — tarefas concretas que um contribuidor pode assumir*/README.md, fuzz/RESULTS.md, verify/VERIFY-REPORT.md — detalhes por etapaKernel v7.2-rc2 (referência somente leitura). Rust estável 1.94.0. LibAFL 0.15.
Charon 909ff09a (v0.1.220, --preset=aeneas), Aeneas c2015b86, Lean/mathlib
v4.31.0.