Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code

O estudo "Broken by Default" utiliza verificação formal com o solucionador Z3 para demonstrar que a maioria dos códigos gerados por sete modelos de IA de ponta em contextos de segurança contém vulnerabilidades matematicamente provadas, com nenhuma das ferramentas de análise ou instruções de segurança convencionais conseguindo mitigar eficazmente esses riscos.

O essencial

Imagine que você contratou um estagiário superinteligente, mas que nunca trabalhou antes. Ele lê milhões de livros, sabe a teoria de tudo e consegue escrever código de computador em segundos. O problema? Ele aprendeu a escrever código olhando para a internet inteira, onde muita gente comete erros.

Este estudo, chamado "Quebrado por Padrão", é como uma prova de estresse brutal para esse estagiário (e sete outros, os melhores do mundo). Os pesquisadores queriam saber: "Se pedirmos para ele escrever código seguro, ele consegue?"

A resposta curta e assustadora é: Não. Na maioria das vezes, ele entrega código cheio de buracos.

Aqui está a explicação do estudo, traduzida para o dia a dia:

1. O Teste: O "Exame de Segurança"

Os pesquisadores deram 500 tarefas diferentes para 7 modelos de Inteligência Artificial (IA) famosos (como GPT-4o, Gemini, Claude, etc.). As tarefas eram coisas do mundo real: criar senhas, gerenciar memória, fazer cálculos matemáticos.

• A Analogia: Imagine pedir para 7 cozinheiros diferentes fazerem um prato complexo. O teste não foi apenas ver se o prato ficou gostoso, mas se eles esqueceram de tirar o vidro da sopa ou se usaram ingredientes estragados.

2. A Descoberta Chocante: "Quebrado por Padrão"

O resultado foi alarmante:

• Mais da metade (55,8%) do código gerado por essas IAs tinha falhas de segurança graves.
• O "melhor" modelo (Gemini 2.5 Flash) ainda falhou em quase metade dos casos.
• O "pior" (GPT-4o) falhou em mais de 60% dos casos.

A Metáfora: É como se você comprasse um carro novo de uma fábrica de ponta, e 6 de cada 10 carros saíssem da linha de montagem com o freio de mão puxado ou com o tanque de gasolina furado. O carro anda, mas é perigoso.

3. A Ferramenta Mágica: O "Detetive Matemático" (Z3)

Como os pesquisadores sabiam que o código estava realmente quebrado? Eles não usaram apenas regras simples (como procurar a palavra "perigoso"). Eles usaram uma ferramenta chamada Z3, que é como um detetive matemático superpoderoso.

• Como funciona: Em vez de apenas olhar para o código, o Z3 tenta "quebrar" a lógica do código matematicamente. Ele pergunta: "Existe algum número que eu possa jogar aqui para fazer o sistema explodir?"
• Se o Z3 diz "Sim, aqui está o número exato que faz o sistema cair", então o erro é proven (provado). Não é uma suspeita; é um fato matemático.
• Eles também testaram isso na vida real, rodando o código e vendo ele travar (como um carro batendo no muro), confirmando que as falhas eram reais.

4. O Grande Problema: Os "Óculos de Segurança" não funcionam

Os pesquisadores tentaram duas coisas para consertar o problema:

A. Pedir para ser mais cuidadoso:
Eles disseram para a IA: "Por favor, escreva código seguro, não cometa erros".

• Resultado: A taxa de erros caiu apenas ligeiramente (de 65% para 61%).
• Importante: Essa pequena melhoria foi observada em um teste específico com um subconjunto menor de 50 prompts (versão v1), e não nos 500 prompts do teste completo.
• Analogia: É como pedir para um motorista que dirige mal: "Por favor, dirija com cuidado". Se ele não sabe dirigir, o aviso não ajuda. O problema está na "memória muscular" dele, não na vontade.

B. Usar ferramentas de verificação comuns:
Eles rodaram o código gerado pelas IAs através de 6 ferramentas de segurança que as empresas usam hoje (como Semgrep, CodeQL, etc.).

• Resultado: As ferramentas tradicionais perderam 97,8% das falhas que o "Detetive Matemático" (Z3) encontrou.
• Analogia: Imagine que você tem um vazamento de água invisível no teto. Você usa um detector de umidade comum e ele não apita. Só um raio-X especial consegue ver o vazamento. As ferramentas atuais são cegas para os erros mais comuns que as IAs cometem.

5. A Ironia Final: Eles sabem que estão errados?

Os pesquisadores pegaram o código com erro, mostraram para a mesma IA que o criou e perguntaram: "Esse código tem erro?".

• Resultado: A IA acertou 78,7% das vezes! Ela sabia que o código era ruim quando estava revisando.
• O Problema: Mas quando ela estava criando o código, ela esquecia tudo e cometia o erro de novo.
• Analogia: É como um aluno que tira nota zero na prova de matemática, mas quando o professor corrige a prova, o aluno diz: "Ah, claro! Eu sabia que estava errado, só esqueci de checar" enquanto escrevia.

Conclusão: O que fazer?

O estudo conclui que, por enquanto, não podemos confiar cegamente no código gerado por IA, especialmente em sistemas críticos (como bancos, hospitais ou controle de tráfego).

As lições principais:

1. Trate o código da IA como se fosse de um estagiário sem supervisão: Você precisa revisar tudo.
2. Pedir "seja seguro" não adianta: A melhoria é mínima e depende de subconjuntos pequenos; você precisa de revisão humana ou ferramentas muito mais avançadas.
3. As ferramentas atuais não bastam: Elas não conseguem pegar os erros matemáticos sutis que as IAs fazem.
4. O código precisa ser testado na vida real: Não basta olhar o texto; tem que rodar e ver se quebra.

Em resumo: A IA é uma ferramenta incrível para acelerar o trabalho, mas ela nasceu com defeito quando o assunto é segurança. Se você usar o código dela sem checar, está basicamente construindo uma casa sobre areia movediça.

Resumo técnico

Resumo Técnico: Broken by Default

1. O Problema

A adoção massiva de assistentes de codificação com IA (como GitHub Copilot, ChatGPT, Claude e Gemini) em domínios sensíveis à segurança (backends, sistemas embarcados, criptografia) levanta uma questão crítica não quantificada: qual é a taxa de explorabilidade real do código gerado por essas IAs?

Estudos anteriores focaram em correspondência de padrões estáticos ou inspeção manual, que não conseguem provar definitivamente se uma vulnerabilidade é explorável. O artigo argumenta que o código gerado por IA é "quebrado por padrão" e que as instruções de segurança nos prompts (ex: "escreva código seguro") são insuficientes para mitigar riscos estruturais.

2. Metodologia

O estudo introduz uma abordagem rigorosa baseada em verificação formal, diferenciando-se de análises heurísticas tradicionais.

• Corpo de Dados: Foram gerados 3.500 artefatos de código a partir de 500 prompts de segurança crítica, distribuídos em 5 categorias de CWE (100 prompts cada):
  • MEM: Alocação de memória e indexação de arrays (C/C++).
  • INT: Aritmética inteira e conversão de tipos.
  • AUTH: Hashing de senhas e gerenciamento de sessão.
  • CRYPTO: Geração de chaves e uso de números aleatórios.
  • INP: Injeção de SQL, manipulação de caminhos de arquivo e comandos de shell.
• Modelos Avaliados: 7 modelos de ponta (Frontier LLMs) acessíveis publicamente em 2026, incluindo GPT-4o, GPT-4.1, Claude Haiku 4.5, Gemini 2.5 Flash, Mistral Large, Llama 3.3 70B e Llama 4 Scout. Todos operados em temperatura 0 (modo determinístico).
• Pipeline COBALT: Uma ferramenta de análise que combina:
  1. Extração de padrões de vulnerabilidade via AST.
  2. Codificação Z3 SMT: Condições de vulnerabilidade são traduzidas em fórmulas lógicas para o solucionador Z3 Satisfiability Modulo Theories (SMT).
  3. Extração de Testemunhas (Witnesses): Se o Z3 retorna "SAT" (satisfatível), um valor concreto (ex: um número específico que causa overflow) é extraído, provando matematicamente a explorabilidade.
• Validação em Tempo de Execução: 7 vulnerabilidades selecionadas foram testadas com GCC AddressSanitizer (ASAN) para confirmar falhas reais (corrupção de memória, vazamento de dados).
• Experimentos Auxiliares:
  • Ablação de Prompt Seguro: Reavaliação com instruções explícitas de segurança. Nota importante: Esta ablação foi conduzida especificamente em um sub-corpus de 50 prompts (v1), e não no benchmark completo de 500 prompts, para fins de replicabilidade e controle experimental.
  • Comparação de Ferramentas: Teste de 6 ferramentas industriais (Semgrep, Bandit, Cppcheck, Clang SA, FlawFinder, CodeQL) contra os artefatos.
  • Assimetria Geração-Revista: Os modelos revisaram seu próprio código gerado para detectar falhas.

3. Principais Contribuições

1. Verificação Formal em Escala: Primeira aplicação de solucionadores SMT (Z3) para estabelecer "verdade fundamental" (ground-truth) de explorabilidade em grande escala em código de IA, movendo-se além de heurísticas baseadas em padrões.
2. Prova de Explorabilidade Real: Demonstração de que vulnerabilidades comuns (como overflow em alocação de memória) não são apenas teóricas, mas geram crashes reais confirmados por ASAN.
3. Identificação de Lacuna Estrutural: Evidência de que ferramentas de análise estática industriais (incluindo CodeQL) são cegas para vulnerabilidades matemáticas complexas (como overflow aritmético em malloc) que o Z3 detecta facilmente.
4. Descoberta de Assimetria Cognitiva: Revelação de que os modelos possuem o conhecimento para identificar vulnerabilidades quando em modo de revisão, mas falham consistentemente em evitá-las durante a geração.

4. Resultados Chave

Taxas de Vulnerabilidade

• Média Geral: 55,8% de todos os artefatos continham pelo menos uma vulnerabilidade identificada pelo COBALT.
• Provas Formais: 1.055 vulnerabilidades foram formalmente provadas como exploráveis via testemunhas Z3 SAT.
• Desempenho por Modelo:
  • Pior: GPT-4o (62,4% de vulnerabilidade, Nota F).
  • Melhor: Gemini 2.5 Flash (48,4% de vulnerabilidade, Nota D).
  • Conclusão: Nenhum modelo atingiu uma nota melhor que D (nenhum abaixo de 45% de falha).

Distribuição por Categoria

• Aritmética Inteira (INT): 87% de taxa de falha (a mais alta). O padrão falho comum foi a falta de verificação de overflow em cálculos de tamanho de alocação (malloc(n * sizeof(T))).
• Alocação de Memória (MEM): 67% de taxa de falha.
• Outras: Input Handling (56%), Autenticação (44%), Criptografia (25%).

Validação em Tempo de Execução

• De 7 casos de prova de conceito (PoC) testados, 6 resultaram em falhas confirmadas pelo AddressSanitizer (heap overflow, leitura fora dos limites, etc.).
• Um caso de injeção de SQL permitiu a extração completa de dados, incluindo números de cartão de crédito sintéticos.

Experimentos Auxiliares

1. Prompt Seguro (Ablação): Adicionar instruções explícitas de segurança reduziu a taxa média de vulnerabilidade de apenas 4 pontos percentuais (de 64,8% para 60,8%) no sub-corpus de 50 prompts (v1). Quatro de cinco modelos permaneceram com nota F.
2. Comparação de Ferramentas:
   • As 6 ferramentas industriais combinadas detectaram apenas 7,6% dos artefatos.
   • Elas perderam 97,8% das vulnerabilidades provadas pelo Z3.
   • O CodeQL teve uma taxa de erro de 100% (0/90) nos artefatos provados formalmente.
3. Assimetria Geração-Revista:
   • Quando os modelos revisaram seu próprio código vulnerável, identificaram corretamente 78,7% das falhas.
   • Isso prova que o problema não é falta de conhecimento, mas uma falha na aplicação espontânea desse conhecimento durante a geração.

5. Significado e Implicações

• Ineficácia de Instruções de Prompt: A segurança não pode ser garantida apenas adicionando "escreva código seguro" ao prompt. Os padrões vulneráveis estão internalizados nos pesos do modelo devido aos dados de treinamento (onde código C seguro com verificações de overflow é raro).
• Limitação das Ferramentas Atuais: Ferramentas de análise estática baseadas em padrões ou rastreamento de fluxo de dados (taint tracking) são estruturalmente incapazes de detectar overflow aritmético em alocações sem raciocínio aritmético concreto. O Z3 é apresentado como a única metodologia capaz de preencher essa lacuna.
• Recomendações para Desenvolvedores:
  1. Tratar todo código C/C++ gerado por IA como código não revisado, exigindo auditoria de segurança explícita.
  2. Não confiar em ferramentas como Semgrep, Bandit ou CodeQL para detectar overflow em aritmética de alocação.
  3. Utilizar verificação formal ou revisão humana para aritmética de alocação.
  4. Compilar e testar todo código de sistema gerado por IA com -fsanitize=address,undefined.

Conclusão

O estudo conclui que os assistentes de codificação com IA atuais produzem código inseguro por padrão. A metodologia de verificação formal via Z3 SMT é essencial para estabelecer a verdade sobre a explorabilidade dessas vulnerabilidades, uma vez que as ferramentas industriais existentes falham em detectar a maioria dos riscos mais críticos (especialmente overflow inteiro). A assimetria entre a capacidade de revisão e a geração dos modelos sugere que o treinamento atual não transfere adequadamente o conhecimento de segurança para a tarefa de geração de código.