KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification

Imagine que você está construindo uma casa com um conjunto de tijolos mágicos e autocorretivos. Esses tijolos, chamados "Rust", são famosos porque possuem um inspetor de segurança integrado que se recusa a deixar você construir qualquer coisa instável. Se você tentar colocar uma janela onde deveria haver uma parede, o inspetor grita "Não!" e o impede antes mesmo de você assentar a primeira pedra. Isso torna o Rust incrivelmente seguro para construir software, prevenindo falhas e brechas de segurança antes que aconteçam. No entanto, às vezes um mestre construtor precisa fazer algo que o inspetor não entende — como usar uma ferramenta especial e perigosa para mover uma viga pesada rapidamente. No mundo do Rust, isso é chamado de "código unsafe" (inseguro). É como um passe secreto que permite ignorar o inspetor, mas isso vem com um preço alto: se você cometer um único erro, toda a casa pode desabar. Para manter a casa de pé, você precisa escrever um "livro de regras" matemático muito rigoroso (chamado de especificação) que prove exatamente como usar essas ferramentas perigosas. Mas escrever esses livros de regras à mão é incrivelmente difícil, lento e propenso ao erro humano.

É aqui que começa a história do KaPilot. Os pesquisadores por trás deste projeto fizeram uma pergunta simples: Podemos ensinar um cérebro de computador superinteligente (uma IA) a escrever esses livros de regras de segurança para nós? O desafio é que essas IAs são ótimas em escrever código, mas frequentemente copiam os erros do código que veem, em vez de entender a intenção por trás dele. Elas podem escrever um livro de regras que parece perfeito, mas que omite um detalhe minúsculo e mortal. O artigo apresenta o KaPilot, uma equipe de agentes de IA trabalhando juntos para resolver este quebra-cabeça. Em vez de apenas pedir à IA para "escrever uma regra", o KaPilot atua como um detetive, um escritor e um editor rigoroso, tudo em um só. Ele lê as notas do construtor (documentação), extrai os verdadeiros requisitos de segurança, escreve um rascunho, verifica se há lacunas e, em seguida, o submete a um teste rigoroso para garantir que ele realmente funcione. O resultado é um sistema que pode gerar automaticamente regras de segurança de alta qualidade, tornando muito mais fácil construir software seguro sem a necessidade de uma equipe de especialistas humanos para escrever cada regra à mão.

O Detetive, o Escritor e o Editor

Pense no processo de verificar código Rust inseguro como tentar escrever um manual de instruções perfeito para um carro de corrida de alta velocidade que não possui freios. Se o manual estiver errado, o carro bate. Se o manual for muito vago, o motorista não sabe como dirigir. Se o manual for muito rígido, o motorista não consegue se mover.

O KaPilot é um framework multiagente, que é apenas uma forma sofisticada de dizer que é uma equipe de personagens de IA especializados trabalhando juntos. Veja como eles desempenham seus papéis:

1. O Detetive (SafetyReq): Antes de escrever qualquer coisa, a equipe precisa saber quais deveriam ser as regras. Geralmente, essas regras estão escondidas nas notas confusas e escritas por humanos (documentação) que acompanham o código. O agente "SafetyReq" atua como um detetive. Ele lê essas notas, ignora o excesso de informações e extrai uma lista limpa e concisa de requisitos de segurança. É como transformar uma história vaga sobre "não toque no botão vermelho" em uma lista numerada clara: "1. Não pressione o botão vermelho. 2. Não fique a menos de 1,5 metro do botão vermelho". Esta etapa é crucial porque impede que a IA apenas copie os erros do código.
2. O Escritor (SpecGenerate): Assim que o detetive tem a lista, o agente "SpecGenerate" entra em cena. Ele é o escritor que transforma essa lista em uma linguagem formal e matemática que o computador possa entender (especificamente, uma linguagem chamada Kani). Ele não apenas adivinha; ele usa a lista do detetive como um guia estrito.
3. O Editor (SpecPrecheck): Antes que o rascunho do escritor vá para o chefe final, o agente "SpecPrecheck" o revisa. É um editor rigoroso que pergunta: "Você cobriu todos os pontos que o detetive encontrou? Sua frase é muito fraca? É forte demais?". Se o rascunho for desleixado, o editor o envia de volta para o escritor com notas específicas sobre como corrigi-lo. Isso acontece em um ciclo até que o rascunho esteja sólido.
4. O Piloto de Teste (SpecVerify): Finalmente, o agente "SpecVerify" pega o rascunho e o submete a um teste do mundo real. Ele usa uma ferramenta chamada Kani para simular milhões de diferentes cenários de direção para ver se o carro bate. Se o carro bater (a verificação falhar), o Piloto de Teste diz ao Escritor exatamente por que ele bateu, e o ciclo recomeça.

A Estratégia de "Embaralhar e Misturar"

É aqui que a equipe fica realmente esperta. Às vezes, a IA gera algumas versões diferentes do livro de regras. Uma versão pode ter uma condição de "início" (pré-condição) perfeita, mas uma condição de "fim" (pós-condição) fraca. Outra pode ter um início fraco, mas um fim perfeito. Se você apenas escolher uma, pode perder a melhor combinação.

O KaPilot usa uma estratégia chamada "shuffle-and-implication" (embaralhar e implicação). Imagine que você tem um baralho de cartas, onde cada carta é uma parte diferente do livro de regras. A equipe embaralha essas cartas, misturando o melhor "início" de uma versão com o melhor "fim" de outra. Eles então testam essas novas combinações para ver se elas funcionam ainda melhor do que os rascunhos originais. É como pegar o melhor motor de um carro e os melhores pneus de outro para construir o carro de corrida definitivo. Isso garante que eles não se contentem apenas com um livro de regras "bom o suficiente", mas encontrem o melhor possível.

O Que Eles Descobriram

Os pesquisadores testaram o KaPilot em 124 diferentes trechos de código Rust inseguro. Eles os dividiram em dois grupos:

• O Conjunto de Ouro (54 funções): Estas possuíam livros de regras de "verdade fundamental" escritos por especialistas humanos, para que a equipe pudesse verificar se o trabalho do KaPilot estava correto.
• O Conjunto Ultra (70 funções): Estas não possuíam livros de regras humanos, então a equipe apenas verificou se o KaPilot conseguia gerar qualquer livro de regras funcional.

Os resultados foram impressionantes. Para o Conjunto de Ouro, o KaPilot gerou com sucesso um livro de regras funcional para 88,9% das funções. Mais importante ainda, 57,4% das vezes, o livro de regras que ele escreveu era tão bom quanto, ou até melhor do que, o escrito pelos especialistas humanos. Para o Conjunto Ultra, ele conseguiu criar livros de regras funcionais para 71,4% das funções.

Quando compararam o KaPilot com outra ferramenta de IA chamada AutoSpec (que foi adaptada para trabalhar com este novo sistema), o KaPilot venceu de longe. Ele produziu 14,8% mais livros de regras que realmente passaram nos testes e 25,9% mais livros de regras que eram semanticamente equivalentes ou melhores do que os escritos por humanos.

Por Que Isso Importa

O artigo argumenta que simplesmente pedir a uma IA para "escrever uma regra de segurança baseada neste código" não funciona bem. A IA tende a copiar as falhas do código ou se confundir com a complexidade. Ao dividir a tarefa em uma equipe de especialistas — um para ler as notas, um para escrever, um para editar e um para testar — o KaPilot evita essas armadilens.

Os pesquisadores também descobriram que a qualidade das notas humanas (documentação) importa muito. Se as notas forem vagas, a IA tem dificuldades. Mas quando as notas são claras, o KaPilot brilha. Eles também descobriram que sua estratégia de "embaralhar" foi um ingrediente fundamental; sem ela, o sistema frequentemente se contentaria com uma solução medíocre em vez de encontrar a combinação perfeita de regras.

Em suma, o KaPilot sugere que não precisamos escolher entre a expertise humana e a velocidade da IA. Ao usar a IA como uma equipe de assistentes especializados que seguem um processo lógico e rigoroso, podemos automatizar a criação de regras de segurança para as partes mais perigosas do nosso software, tornando o mundo digital um lugar mais seguro para viver. O artigo não afirma que isso resolve todos os problemas (alguns loops complexos ainda precisam de ajuda humana), mas prova que esta abordagem multiagente é um passo gigantesco para tornar a verificação de software automática e confiável.