Resumo Técnico: Detecção Automática de Bugs de Contagem de Referências em Drivers do Kernel Linux

Declaração do Problema

No kernel monolítico Linux, os drivers de dispositivo operam no mesmo nível de privilégio que o núcleo do kernel, tornando bugs em drivers um risco crítico de segurança. A contagem de referências (refcount) é o mecanismo primário usado para gerenciar manualmente o ciclo de vida de objetos do kernel. Uma contagem de referências rastreia o número de referências ativas a um objeto; uma contagem positiva indica que o objeto está em uso, enquanto zero indica que é seguro liberá-lo.

Bugs de contagem de referências ocorrem quando a contagem não corresponde ao número real de referências. Contagens de referências excessivas levam a vazamentos de memória, enquanto contagens de referências insuficientes resultam em vulnerabilidades de uso-após-liberação (UAF). Essas questões são prevalentes devido à complexidade da base de código do kernel (os drivers constituem aproximadamente 66,5% do kernel) e à diversidade das implementações de drivers. Ferramentas existentes de análise estática frequentemente lutam com a escala e a complexidade do kernel Linux, resultando em altas taxas de falsos positivos ou falta de escalabilidade.

Metodologia: DrvHorn

Os autores apresentam o DrvHorn, uma ferramenta automatizada inovadora projetada para detectar bugs de contagem de referências especificamente dentro dos drivers do kernel Linux. A ferramenta transforma o problema de verificação de contagem de referências em um problema de verificação de asserções, aproveitando a interface estruturada fornecida pelo kernel Linux.

Arquitetura Central

O DrvHorn opera sobre o código-fonte do kernel Linux compilado para bitcode LLVM. Seu fluxo de trabalho consiste em quatro etapas principais:

1. Redução à Verificação de Asserções:
   Em vez de verificar todo o kernel, o DrvHorn foca na fase de inicialização do driver. Ele explora a observação de que, se a inicialização falhar, todos os recursos adquiridos devem ser liberados para prevenir vazamentos. A ferramenta gera um alvo de verificação que chama a função de inicialização do driver e afirma que a mudança líquida nas contagens de referências (para dispositivos, nós da árvore de dispositivos e nós de firmware) é zero ao falhar. Se a asserção falhar, um bug é reportado.

2. Modelagem do Kernel Linux:
   Para gerenciar a complexidade do kernel, o DrvHorn substitui APIs específicas do kernel por abstrações simplificadas que preservam o comportamento de contagem de referências:

   • Árvore de Dispositivos: Em vez de modelar as estruturas complexas de ponteiros de struct device_node, o DrvHorn modela as APIs (por exemplo, of_get_next_child, of_find_node_by_name) com base em quatro tipos distintos de comportamento (retornar NULL, retornar não-NULL, decrementar contagem de referências, ou nenhum decremento).
   • Dispositivos e Barramentos: APIs que retornam dispositivos com contagem de referências incrementada (por exemplo, usb_find_interface) são modeladas para retornar ponteiros para regiões de memória específicas e não-aliasadas, determinadas pelo argumento do barramento, prevenindo violações de aliasing espúrias.
   • Gerenciamento de Recursos de Dispositivo (Devres): A ferramenta simplifica __devm_add_action() invocando imediatamente a função de limpeza associada após o local da chamada, em vez de rastrear explicitamente a lista devres.

3. Fatiamento de Programa Agressivo:
   A Eliminação de Código Morto (DCE) padrão é insuficiente para a escala do kernel. O DrvHorn implementa uma técnica de fatiamento personalizada e agressiva:

   • Argumentos Essenciais: Argumentos que incorporam struct kref que podem modificar contagens de referências são marcados como essenciais.
   • Coleta de Instruções: A ferramenta coleta recursivamente instruções necessárias para a verificação de contagem de referências, incluindo ramificações, retornos e chamadas onde parâmetros dependem de argumentos essenciais.
   • Substituição de Não-Essenciais: Instruções não consideradas necessárias são removidas. Chamadas de função com resultados não essenciais são substituídas por valores não determinísticos (usando o atributo writeonly do LLVM para mitigar a perda de efeitos colaterais).

4. Verificação Baseada em CHC:
   O problema de asserção reduzido é resolvido usando o SeaHorn, um solucionador de Cláusulas de Horn com Restrições (CHC). Os autores escolheram o SeaHorn em vez de verificadores de modelo limitados (como SeaBMC) porque solucionadores CHC são mais adequados para lidar com os loops comuns em manipulações de contagem de referências sem exigir limites manuais de desenrolamento de loops.

Contribuições Principais

• Invariante Inovadora: A derivação de uma invariante universal de contagem de referências aplicável a todos os drivers: a diferença de contagem de referências deve ser zero quando a inicialização do driver falha.
• Ferramenta Automatizada: O desenvolvimento do DrvHorn, que integra modelagem de kernel, fatiamento agressivo e resolução CHC para alcançar detecção totalmente automatizada.
• Escalabilidade e Precisão: A capacidade de analisar milhares de drivers com uma taxa de falsos positivos significativamente menor em comparação com ferramentas anteriores do estado da arte.
• Impacto no Mundo Real: A descoberta e correção de bugs previamente desconhecidos no kernel Linux.

Resultados da Avaliação

Os autores avaliaram o DrvHorn em 3.387 drivers de plataforma no kernel Linux v6.6 x86-64 (compilado com allyesconfig).

• Detecção de Bugs: O DrvHorn reportou 777 bugs potenciais.
• Validação: Inspeção manual confirmou 545 como bugs reais.
• Falsos Positivos: Houve 232 falsos positivos, resultando em uma taxa de falsos positivos de 29,9%. Os autores observam que 27 desses foram causados por falta de solidez na política de fatiamento (fluxo de informação indireto), enquanto a maioria foi devido à análise conservadora de ponteiros no modelo de memória do solucionador.
• Novidade: 424 dos bugs confirmados eram previamente desconhecidos.
• Mesclagens Upstream: Os autores enviaram correções para os bugs descobertos, e 45 foram mesclados no kernel Linux.
• Falsos Negativos: Testes contra 17 bugs conhecidos corrigidos desde o lançamento v6.6 mostraram que o DrvHorn perdeu apenas um (devido a limitações de fatiamento relacionadas ao fluxo de informação indireto), sugerindo uma baixa taxa de falsos negativos.
• Tempo Esgotado: A ferramenta esgotou o tempo em 807 drivers (limite de 300 segundos), frequentemente devido a loops aninhados complexos em funções utilitárias.
• Comparação: Quando comparado ao SeaBMC (verificação de modelo limitada), o SeaBMC perdeu 39,4% dos bugs reais encontrados pelo DrvHorn e esgotou o tempo em 24,2% deles, confirmando a superioridade da abordagem baseada em CHC para esta tarefa específica.

Significado e Alegações

O artigo afirma que o DrvHorn alcança um equilíbrio de escalabilidade e precisão que ferramentas anteriores lutaram para atingir no diverso ecossistema de drivers Linux. Ao focar especificamente em drivers e explorar a interface de drivers do kernel para derivar uma invariante simples, a ferramenta evita a necessidade de invariantes complexas e específicas de subsistemas que frequentemente afligem outros esforços de verificação.

Os autores enfatizam que, embora o DrvHorn não seja nem sólido nem completo (pode perder bugs ou reportar falsos positivos), sua utilidade prática é demonstrada pelo alto número de bugs reais e previamente desconhecidos descobertos e pelo sucesso na integração de correções upstream. A ferramenta representa um passo significativo em direção à verificação estática totalmente automatizada e de alta precisão de drivers do kernel Linux, abordando um vetor crítico de vulnerabilidade de segurança.

Limitações Reconhecidas:

• A ferramenta atualmente foca na fase de inicialização; a extensão para funções de limpeza/terminação é deixada para trabalhos futuros.
• Atualmente, não verifica contagens de referências para tipos além de struct kref.
• A taxa de falsos positivos, embora menor que estudos anteriores, ainda é não trivial (29,9%), em grande parte devido à modelagem conservadora de memória no solucionador.
• O fluxo de informação indireto não é totalmente capturado pela política de fatiamento, levando a alguns bugs perdidos e falsos positivos.