Resumo Técnico: BODHI: Inferência de Especificação Precisa do Kernel do SO

Declaração do Problema

A verificação formal de kernels de sistemas operacionais (SO) é crítica para sistemas de segurança crítica, mas é limitada pelo esforço manual necessário para construir especificações formais precisas. Embora os Modelos de Linguagem de Grande Escala (LLMs) tenham demonstrado proficiência na geração geral de código, sua capacidade de sintetizar especificações formais para kernels de SO permanece limitada. A benchmark OSV-Bench, que avalia a conversão de implementações de chamadas de sistema em C para especificações de máquina de estado em Python/Z3, revelou uma lacuna de desempenho significativa: a melhor pontuação Pass@1 relatada entre 12 modelos avaliados foi de apenas 55,10%.

Essa lacuna decorre de quatro desafios principais:

1. Complexidade de contexto longo: Os prompts contêm aproximadamente 26 mil tokens, incluindo modelos de programação, exemplos e código alvo.
2. Lacuna semântica: A tarefa exige traduzir código imperativo de kernel em C para especificações declarativas em Python/Z3, envolvendo paradigmas de programação fundamentalmente diferentes.
3. Preocupações intercaladas: O código C frequentemente mistura lógica de pré-condição (verificação de erros) e pós-condição (mutação de estado), que devem ser estritamente separadas em especificações formais.
4. Conhecimento específico de domínio: As APIs de kernel envolvem padrões especializados (por exemplo, fórmulas de entradas de tabela de páginas, semântica de contagem de referências, operações de flush de TLB) que não são cobertos pelo treinamento de LLMs de propósito geral.

Metodologia: BODHI

Os autores propõem o BODHI, um método de prompting com conhecimento de domínio que amplia prompts padrão de poucos exemplos com um Guia de Tradução de C para Python estruturado. Diferentemente da Cadeia de Pensamento (CoT) padrão ou da Cadeia de Pensamento Estruturada (SCoT), que focam na geração de etapas de raciocínio intermediárias, o BODHI injeta material de referência estruturado no contexto de entrada.

Estrutura do Prompt

O prompt do BODHI mantém os quatro componentes da linha de base OSV-Bench:

1. Prompt do sistema (instruções).
2. Modelo de programação (definições de classes, constantes, funções).
3. Cinco exemplos de poucos exemplos (pares de implementação em C e especificação em Z3).
4. Tarefa alvo (descrição funcional e código em C).

O BODHI adiciona um quinto componente: um Guia de Tradução de 519 linhas inserido entre os exemplos de poucos exemplos e a tarefa alvo. Essa posição aproveita o "efeito de recência" na atenção dos transformadores, garantindo que padrões específicos de domínio estejam mais acessíveis durante a geração.

Design do Guia de Tradução

O guia é organizado em 15 categorias derivadas de uma análise iterativa de falhas em um modelo de nível intermediário (Claude Haiku 4.5). Ele segue o princípio de Separação de Preocupações, distinguindo entre extração de pré-condição e geração de pós-condição. As categorias são agrupadas em três níveis:

• Nível 1 (Sintaxe): Abrange modelos de especificação, tradução de pré-condição (negação de verificações de erro em C), padrões de pós-condição, sintaxe de campos de mapa (distinguindo leitura () de escrita []), regras de operadores e prefixos de constantes.
• Nível 2 (Semântica de Domínio): Abrange fórmulas de Entrada de Tabela de Páginas (PTE) (distinguindo x86 de IOMMU), metadados de sombra, contagem de referências, operações de flush de TLB, nomes de ponteiros de estado e mapeamento de nomes de campos.
• Nível 3 (Completude): Aborda expansão de funções auxiliares em C, inventários de auxiliares disponíveis e padrões complexos de máquina de estado de IPC.

Crucialmente, o guia funciona como um "livro didático de domínio" contendo regras gerais de tradução e padrões ilustrativos, não soluções específicas para tarefas ou código completo.

Contribuições Principais

1. Guia de Tradução Específico de Domínio: Um guia estruturado de 15 categorias cobrindo padrões de tradução de C para Python/Z3 derivados de especificações verificadas de verdade fundamental.
2. Avaliação Abrangente: Testes em nove modelos de seis provedores (Anthropic, Mistral, Amazon, DeepSeek, Meta, Alibaba), cobrindo arquiteturas densas, mistura de especialistas e raciocínio.
3. Análise de Erros: Uma detalhada decomposição mostrando que o BODHI reduz erros tanto de sintaxe quanto semânticos, com o impacto mais significativo em modelos de nível intermediário que possuem capacidades de seguimento de instruções, mas carecem de conhecimento específico de domínio.
4. Novo Estado da Arte: Alcançando um Pass@1 de 96,73% na OSV-Bench, superando substancialmente o melhor anterior de 55,10%.

Resultados

• Ganhos de Desempenho: O BODHI melhorou as pontuações Pass@1 para todos os modelos testados, com ganhos variando de +11,0% (Qwen3) a +31,8% (Devstral 2).
• Melhor Desempenho: A configuração de Claude Opus 4.6 + BODHI alcançou 96,73%, falhando em apenas 8 de 245 tarefas.
• Redução de Erros:
  • Erros de Sintaxe: O BODHI reduziu significativamente erros de sintaxe, particularmente incompatibilidades de tipo/tipo e mau uso de API (por exemplo, usar parênteses para escritas em mapa). Para o Devstral 2, erros de sintaxe caíram de 31,0% para 8,2%.
  • Erros Semânticos: O guia abordou efetivamente erros de padrões de domínio (por exemplo, fórmulas PTE incorretas) e erros de lógica de tradução. Para o Claude Opus 4.6, as falhas da linha de base foram quase exclusivamente erros de padrões de domínio; o BODHI reduziu esses para 2,4%.
• Agnosticismo de Modelo: As melhorias foram consistentes em arquiteturas e provedores diversos, sugerindo que a técnica não está vinculada aos dados de treinamento de uma família específica de modelos.
• Otimização de Nível Intermediário: Os maiores ganhos relativos foram observados em modelos de nível intermediário (por exemplo, Devstral 2, Claude Haiku 4.5), que possuem capacidade suficiente de seguimento de instruções para utilizar o guia, mas carecem do conhecimento intrínseco de domínio dos modelos de nível superior.

Significado e Alegações

O artigo alega que a injeção de conhecimento de domínio é uma técnica agnóstica de modelo que efetivamente preenche a lacuna entre geração de código de propósito geral e síntese de especificação formal. Os autores argumentam que o gargalo na verificação de kernel de SO não é a capacidade de raciocínio do LLM (já que modelos otimizados para raciocínio como o1 e DeepSeek-R1 não superaram modelos padrão de seguimento de instruções), mas sim a falta de conhecimento específico de tradução.

Ao estruturar o conhecimento de domínio em um guia de referência em vez de depender apenas de exemplos de poucos exemplos, o BODHI permite que os LLMs lidem corretamente com semânticas complexas de kernel, como fórmulas de tabela de páginas e contagem de referências. O trabalho demonstra que existe uma divisão produtiva de trabalho onde especialistas humanos constroem o guia de domínio, e os LLMs o aplicam em escala para alcançar síntese de especificação quase perfeita. Os autores observam que a abordagem é limitada pelo custo de construção do guia e pela capacidade do modelo de aderir a formatos de saída, mas oferece um caminho reproduzível para melhorar a verificação formal sem re-treinamento do modelo.