Resumo Técnico: Verificação Estática Baseada em LLM de Código Contra Requisitos em Linguagem Natural

Declaração do Problema

As ferramentas convencionais de análise estática (por exemplo, Coverity, SonarQube) são eficazes na detecção de defeitos de codificação, problemas de segurança de memória e padrões de vulnerabilidade conhecidos. No entanto, carecem da capacidade de verificar se o código implementado satisfaz requisitos funcionais escritos em linguagem natural. Existe uma lacuna crítica na detecção de defeitos de lógica de negócios, como um programa que implementa adição em vez de multiplicação, ou uma política de senha que contradiz estruturalmente sua especificação em linguagem natural. Esses defeitos frequentemente não contêm assinaturas de vulnerabilidade reconhecíveis e são difíceis de expor por meio de testes dinâmicos devido à cobertura limitada de casos de teste, à dificuldade de definir oráculos de teste e à complexidade de grandes espaços de entrada. O desafio é realizar análise estática consciente de requisitos e consciente de semântica que verifique o código contra especificações em linguagem natural sem exigir compilação, execução ou ambientes de tempo de execução.

Metodologia

O artigo propõe um fluxo de trabalho baseado em LLM de duas etapas projetado para abordar o problema de verificação dependente de especificação no contexto de cibersegurança de veículos inteligentes. Essa abordagem evita pedir a um único LLM que verifique diretamente o código contra especificações extensas em linguagem natural, o que arrisca alucinação, variabilidade de saída e perda de contexto. Em vez disso, introduz uma representação intermediária estruturada.

Etapa 1: Mineração de Regras Baseada em IA (ruleMiner)

O primeiro agente, ruleMiner, processa requisitos em linguagem natural frase por frase para extrair um conjunto de regras verificáveis.

• Lógica de Extração: Retém apenas lógica normativa e falseável (por exemplo, declarações explícitas "deverá" e declarações contextualmente obrigatórias "deveria").
• Tratamento de Ambiguidade: Material explicativo, permissivo ou subjetivo é excluído. Termos como "aleatório" ou "forte" não são convertidos em regras a menos que fundamentados em condições mensuráveis.
• Registro de Defeitos: Ambiguidades, autocontradições e declarações não verificáveis não são traduzidas em regras. Em vez disso, são explicitamente registradas em uma estrutura de dados requirements_specs_issues para evitar que requisitos defeituosos contaminem verificações a jusante.
• Melhoria de Completude: Para abordar a variabilidade de saída, o sistema emprega uma relação metamórfica (MR1): mesmo com a temperatura do LLM definida como 0, execuções repetidas podem produzir saídas diferentes. Uma estratégia de agrupamento é usada para reconciliar e mesclar saídas de múltiplas execuções (1–3 execuções) para gerar um conjunto de regras mais completo.

Etapa 2: Auditoria de Código Baseada em IA (codeAuditor)

O segundo agente, codeAuditor, avalia o código-fonte contra o conjunto de regras extraído.

• Raciocínio Semântico: Diferentemente de scanners baseados em padrões, o codeAuditor raciocina sobre o conteúdo semântico, derivando pontos de verificação concretos, como valores permitidos/proibidos, limiares, condições de unicidade e gatilhos operacionais.
• Verificação Baseada em Evidências: Verifica esses pontos contra código-fonte, configurações, constantes, lógica de validação e relações de chamada entre arquivos.
• Critérios Estritos: Uma regra não é considerada satisfeita meramente pela presença de identificadores sugestivos ou comentários. Por outro lado, uma proibição não é sinalizada como violada a menos que haja evidência de um caminho de habilitação real ou comportamento alcançável.

Estudo de Caso Industrial e Resultados

A metodologia foi aplicada a um estudo de caso industrial de segurança pública envolvendo um subsistema de segurança WiFi veicular.

Observações Principais

1. Detecção de Defeitos de Requisitos: O pipeline identificou com sucesso requisitos contraditórios. Por exemplo, uma política de senha exigia tipos específicos de caracteres, mas fornecia um padrão de exemplo que não atendia a essas condições. O ruleMiner sinalizou corretamente isso como conteúdo contraditório em requirements_specs_issues em vez de gerar uma regra falsa. Esse defeito permaneceu não detectado por mais de um ano.
2. Detecção de Incompatibilidade de Lógica: O sistema identificou uma incompatibilidade entre um requisito (ponto de acesso WiFi desativado quando "não em uso") e a implementação. A implementação dependia de condições de inatividade local em vez do estado do sistema mais amplo implicado pelo requisito. Isso revelou um defeito de requisito (estado de gatilho indefinido) em vez de um simples erro de codificação.
3. Achados Quantitativos:
   • Requisitos: De 222 itens analisados, 75 problemas de requisitos foram relatados. A inspeção manual do subconjunto de segurança WiFi não encontrou regras extraídas incorretas.
   • Código: A análise da base de código madura de WiFi produziu 8 achados "Falha/Desconhecido". A inspeção manual confirmou nenhum falso positivo. Um problema de codificação de alta prioridade foi detectado e posteriormente corrigido pela equipe de desenvolvimento.
   • Cobertura: O fluxo de trabalho verificou mais de 50% dos requisitos que anteriormente só podiam ser avaliados por meio de testes de software.

Contribuições Principais

1. Pipeline de Verificação de Duas Etapas: Um fluxo de trabalho inovador que desacopla o esclarecimento de requisitos da auditoria de código, usando um conjunto de regras intermediário para reduzir modos de falha do LLM (alucinação, variabilidade) e melhorar a explicabilidade.
2. Tratamento Explícito de Defeitos: A introdução da estrutura requirements_specs_issues garante que requisitos ambíguos ou contraditórios sejam trazidos à tona em vez de serem normalizados silenciosamente em regras verificáveis por máquina, mas semanticamente não confiáveis.
3. Integração de Testes Metamórficos: A aplicação de relações metamórficas (especificamente o agrupamento de múltiplas execuções de LLM) para melhorar a completude e a consistência da mineração de regras.
4. Análise Estática Orientada a Lógica de Negócios: Uma mudança da detecção baseada em padrões para o raciocínio consciente de semântica, capaz de identificar incompatibilidades em gatilhos, caminhos de execução e lógica de aplicação que ferramentas convencionais ignoram.

Significado e Alegações

O artigo posiciona essa abordagem como uma estratégia complementar e não de substituição para testes dinâmicos e análise estática convencional. Seu significado principal reside em:

• Verificação Deslocada para a Esquerda: Permitir a detecção de defeitos de lógica de negócios mais cedo no ciclo de vida de desenvolvimento, sem a necessidade de compilação, execução ou ambientes de tempo de execução.
• Abordagem do Problema do Oráculo de Teste: Ao raciocinar sobre a semântica do código-fonte e a lógica de implementação em vez de depender exclusivamente de saídas de programa esperadas, a cadeia de ferramentas baseada em LLM ajuda a mitigar a dificuldade de definir oráculos de teste para lógica de negócios complexa.
• Rastreabilidade Industrial: Destacar a dependência crítica de rastreabilidade de alta qualidade (por exemplo, histórico de solicitações de mesclagem) entre requisitos e código, observando que lacunas na rastreabilidade organizacional podem limitar a interpretação definitiva dos achados.

Os autores mantêm um tom modesto, observando que os resultados quantitativos são preliminares e não alegações de benchmark. Eles reconhecem que o recall e a completude da mineração de regras não foram avaliados exaustivamente devido ao esforço manual necessário. No entanto, a experiência sugere que integrar o esclarecimento de requisitos, a conscientização sobre rastreabilidade e a análise estática baseada em LLM representa uma direção promissora para garantia industrial.