Resumo Técnico: Heimdall

Declaração do Problema

Os programas do Extended Berkeley Packet Filter (eBPF) são críticos para extensões do kernel Linux em redes, observabilidade e segurança. Embora o verificador de eBPF no kernel imponha segurança de memória de baixo nível e terminação, ele falha em impor propriedades de nível superior no código-fonte, como disciplina de inicialização, consistência de esquema e tratamento de erros. Os autores documentam seis classes de bugs de nível de fonte que são compilados e passam pelo verificador do kernel, mas podem corromper dados silenciosamente, vazar informações sensíveis ou produzir resultados de aplicação incorretos.

As vulnerabilidades-chave identificadas incluem:

• Estado Não Inicializado: Programas que emitem structs residentes na pilha sem inicialização a zero vazam resíduos da pilha por CPU, incluindo ponteiros do kernel e endereços de retorno suficientes para recuperar os deslocamentos de Randomização de Layout de Espaço de Endereços do Kernel (KASLR).
• Retornos de Funções Auxiliares Não Verificados: Funções auxiliares (por exemplo, bpf_probe_read_user_str) que falham são frequentemente ignoradas, causando a emissão de dados antigos da pilha em vez de strings truncadas.
• Incompatibilidades de Buffer/Tamanho: Desenvolvedores que passam tamanhos incorretos para funções auxiliares de saída podem vazar campos privados adjacentes contendo ponteiros do kernel.
• Incompatibilidades de Gancho/Contexto: O uso de estruturas de contexto incorretas (por exemplo, __sk_buff em um gancho XDP) leva a dados mal interpretados.
• Confusão de Tipo/Esquema de Mapa: Incompatibilidades entre os tamanhos declarados de valores de mapa e os dados reais, ou reinterpretação de resultados de busca em mapa como tipos não relacionados.
• Confusão de Sinalizado/Não Sinalizado: Armazenar valores de retorno de funções auxiliares sinalizados (indicando erros) em campos não sinalizados cria grandes valores positivos espúrios usados como chaves de mapa.

Além disso, o próprio verificador de eBPF possui vulnerabilidades conhecidas (por exemplo, poda não sólida, validação de contrato ausente) que podem ser exploradas. A migração para uma linguagem segura em memória como Rust poderia fechar essas lacunas, mas a reescrita manual é impraticável em escala, e as ferramentas de tradução automatizadas existentes carecem do rigor necessário para garantir equivalência semântica ou segurança no contexto do eBPF.

Metodologia: O Pipeline Heimdall

O Heimdall é um pipeline automatizado que traduz programas legados libbpf em C para Rust idiomático e seguro Aya. Ele emprega um processo iterativo de cinco estágios combinando Modelos de Linguagem de Grande Escala (LLMs), análise estática e verificação formal:

1. Tradução por LLM: Um LLM traduz o código-fonte C para Rust usando mapeamentos da API Aya, macros de gancho e exemplos funcionais.
2. Compilação e Verificação no Kernel: O código Rust gerado é compilado para bytecode eBPF. Guardas de lint do compilador (por exemplo, negando blocos unsafe não utilizados) e o verificador do kernel verificam segurança e correção básicas. Erros são enviados de volta ao LLM para reparo.
3. Verificação de Segurança (Análise Estática): Um motor de análise estática personalizado varre o código-fonte Rust em busca de saídas de escape inseguras que o compilador e o verificador possam perder. Isso inclui proibir reservas de buffers de anel não tipadas, impor inicialização a zero e exigir tratamento explícito de tipos Result para retornos de funções auxiliares.
4. Execução Simbólica: Tanto o binário C original quanto o binário Rust compilado são carregados em um backend eBPF personalizado para angr. Este backend modela funções auxiliares eBPF, mapas, relocalizações e operações atômicas. Ele realiza execução simbólica para explorar todos os caminhos viáveis, gerando fórmulas estruturadas para valores de retorno e efeitos colaterais de mapas.
5. Verificação de Equivalência: Um solucionador baseado em Z3 verifica se os programas C e Rust são semanticamente equivalentes. Os autores introduzem Equivalência Semântica Condicional, que exige equivalência apenas em entradas que satisfazem condições de segurança declaradas (por exemplo, chamadas de funções auxiliares com sucesso). Isso permite que a tradução Rust mais segura (que trata erros ou preenche memória com zeros) seja considerada equivalente à fonte C com bugs nos caminhos onde o bug é acionado, enquanto ainda verifica que a lógica é preservada em caminhos válidos. Se um contraexemplo for encontrado, ele é enviado de volta ao LLM para reparo direcionado.

Para suportar isso, os autores construíram um backend completo de eBPF para o angr, incluindo um carregador ELF, definição de arquitetura, elevador VEX IR e stubs de funções auxiliares. Eles também desenvolveram uma codificação de cadeia ITE personalizada para modelar efeitos colaterais de mapas sob chaves simbólicas, capturando a semântica "última escrita vence".

Contribuições Principais

• Pipeline Heimdall: O primeiro sistema automatizado a traduzir programas de produção eBPF de C para Rust com garantias formais por programa de preservação de comportamento observável.
• Equivalência Condicional: Uma abordagem de verificação inovadora que valida traduções que melhoram a segurança (que se comportam de forma diferente em caminhos que acionam bugs) restringindo verificações de equivalência a caminhos de execução seguros.
• Backend de Execução Simbólica eBPF: Um backend completo de eBPF para o angr que modela funções auxiliares do kernel, mapas e chamadas BPF-para-BPF, permitindo raciocínio formal no nível de bytecode.
• Analisador Estático Safe-Aya: Um motor de políticas que rejeita padrões inseguros de Rust (por exemplo, buffers de anel não tipados, erros de funções auxiliares ignorados) que passam no verificador do kernel.
• Descobertas de Segurança: Descoberta de vazamentos de informações previamente não relatados em dez programas de código aberto eBPF, incluindo recuperação de KASLR via resíduos de pilha e vazamentos de conteúdo entre eventos em buffers de anel.
• Benchmark e Avaliação: Um benchmark público de 102 programas eBPF e uma avaliação abrangente do pipeline de tradução.

Resultados

O sistema foi avaliado em 102 programas eBPF do mundo real de várias fontes (libbpf-tools, libbpf-bootstrap, KEN, Suricata, etc.).

• Taxa de Sucesso: O Heimdall produziu 96 traduções formalmente verificadas como equivalentes (94,1%). As seis restantes foram parcialmente verificadas (devido a limites de execução simbólica) ou excederam os limites de escalabilidade do solucionador.
• Fechamento de Bugs: Nas 96 traduções verificadas, o Heimdall fechou 100% das instâncias observadas de estado não inicializado, retornos de funções auxiliares não verificados e confusão sinalizado/não sinalizado.
• Comparação com Baselines: Comparado a agentes LLM de base sem o pipeline Heimdall, o Heimdall (Agente) alcançou uma taxa de três tentativas de 98% (Compilar, Verificar no Kernel, Segurança, Equivalência) versus 4–12% para as baselines.
• Sobrecarga de Tempo de Execução: Validação em tempo de execução em 10 programas mostrou que as traduções em Rust geralmente incorreram em sobrecarga modesta (média geométrica variando de 0,44× a 3,60× em comparação com C), com a maioria situando-se entre 1,14× e 1,89×.
• Segurança: As traduções eliminaram os padrões inseguros específicos (memória não inicializada, erros não verificados) que causaram as vulnerabilidades identificadas.

Significado

O artigo afirma que o Heimdall é o primeiro sistema a automatizar a migração segura em memória de programas de produção eBPF com garantias formais por programa de que a migração preserva o comportamento observável. Ele aborda a lacuna entre as garantias de baixo nível do verificador do kernel e os requisitos de segurança de alto nível de aplicações modernas de eBPF. Ao combinar LLMs com verificação formal e análise estática, o Heimdall demonstra que a tradução automatizada pode produzir código que não apenas está sintaticamente correto, mas também semanticamente equivalente e livre de classes específicas de bugs de segurança de nível de fonte que o verificador do kernel não consegue detectar. O trabalho estabelece um novo benchmark para migração eBPF e fornece uma base para construir extensões de kernel mais robustas e seguras em memória.