Análise de Programas

Visão geral

Análise de programas (program analysis) é o estudo de técnicas para raciocinar automaticamente sobre o comportamento de software. Os objetivos centrais incluem provar ou refutar propriedades como:

Corretude (o programa atende à sua especificação?)
Segurança operacional (safety) (coisas “ruins” podem acontecer, como desreferenciamento de nulo ou estouro de buffer?)
Segurança (security) (entradas não confiáveis podem levar a exploits ou vazamentos de dados?)
Terminação (o programa sempre termina?)
Limites de recursos (tempo, memória, energia)

A análise de programas se insere firmemente nas tradições da I.A. clássica/simbólica (classical/symbolic AI): ela se baseia em semântica formal, lógica e resolução de restrições para derivar conclusões sobre programas. Na prática, ela alimenta analisadores estáticos em IDEs, otimizações de compiladores, detectores de vulnerabilidades e ferramentas de verificação. Ela também interage de perto com Satisfação de Restrições por meio de resolução SAT/SMT, e fornece fundamentos para Síntese de Programas (especialmente laços de síntese por verificação).

Um tema central é a tensão entre:

Solidez (soundness): nunca perder bugs reais (sem falsos negativos)
Precisão (precision): não reportar bugs espúrios demais (poucos falsos positivos)
Escalabilidade (scalability): lidar com grandes bases de código do mundo real

A maioria dos sistemas práticos faz compromissos entre esses três aspectos.

Análise estática vs dinâmica de programas

Análise estática

Análise estática (static analysis) raciocina sobre um programa sem executá-lo — a partir do código-fonte, bytecode ou uma representação intermediária (IR). Em princípio, ela pode explorar todas as execuções possíveis, inclusive casos extremos raros que testes podem não capturar.

Saídas típicas de uma análise estática:

avisos (possível desreferenciamento de ponteiro nulo)
provas (este acesso a array sempre está dentro dos limites)
fatos inferidos (a variável x aqui é sempre não negativa)
sumários (a função f pode alocar memória e deve ser liberada)

Análises estáticas frequentemente aproximam o comportamento para permanecer escaláveis; por isso analisadores estáticos podem reportar falsos positivos.

Análise dinâmica

Análise dinâmica (dynamic analysis) observa o comportamento durante a execução. Em geral, ela é:

mais precisa para as execuções que observa (valores concretos)
menos completa no geral (apenas caminhos cobertos são analisados)

Exemplos incluem:

sanitizers (ASan/UBSan), checagens de limites em tempo de execução
rastreamento dinâmico de taint
profiling e tracing
fuzzing (gera entradas para disparar falhas)
verificação em tempo de execução (checagem de propriedades temporais durante execuções)

Muitas ferramentas modernas são híbridas: misturam raciocínio estático com execução dinâmica (por exemplo, testes concolic — execução concreta + simbólica).

Fundamentos: semântica e representações de programa

A maioria das técnicas de análise se apoia em uma noção formal (explícita ou implícita) de semântica de programa (program semantics): o que uma instrução significa em termos de transições de estado?

Para tornar a análise viável, as ferramentas normalmente traduzem o código para representações como:

Grafos de fluxo de controle (CFGs) (control-flow graphs): nós são blocos básicos; arestas representam saltos possíveis.
Forma de atribuição única estática (SSA) (static single assignment): cada variável é atribuída uma vez, simplificando muitas análises.
Grafos de chamadas (call graphs): possíveis relações de chamada entre funções/métodos.

Essas representações transformam “raciocinar sobre programas” em “raciocinar sobre grafos e equações”.

Análise de fluxo de dados

Análise de fluxo de dados (dataflow analysis) é uma das famílias de análise estática mais usadas. Ela calcula fatos sobre pontos do programa propagando informações por um CFG até alcançar um ponto fixo (fixpoint) (nada mais muda).

Exemplos clássicos

Definições alcançáveis (reaching definitions): quais atribuições a uma variável poderiam alcançar este ponto do programa?
Variáveis vivas (live variables): quais valores atuais de variáveis podem ser usados mais adiante?
Expressões disponíveis (available expressions): quais expressões já foram computadas e não foram invalidadas?
Análise de taint (taint analysis) (frequentemente formulada como fluxo de dados): dados de fontes não confiáveis podem chegar a sinks sensíveis?

A visão de reticulado (por que pontos fixos aparecem)

Muitas análises de fluxo de dados definem:

um conjunto de fatos (por exemplo, “a variável x é constante com valor 7”)
uma forma de combinar fatos de diferentes caminhos (um join)
uma ordem parcial que descreve informação “mais precisa” vs “menos precisa”

Essa estrutura é geralmente um reticulado (lattice), permitindo que algoritmos iterativos convirjam para um ponto fixo.

Exemplo prático: propagação de constantes (simplificada)

Considere:

int f(int a) {
  int x = 3;
  int y = x + 4;
  if (a > 0) {
    x = 10;
  }
  return x + y;
}

Uma análise de propagação de constantes poderia inferir:

Após int x = 3;, x é constante 3.
y se torna constante 7.
Após o if, x é ou 3 ou 10 dependendo do ramo, então x deixa de ser uma única constante.

Esse tipo de raciocínio habilita otimizações de compilador e também apoia a descoberta de bugs (por exemplo, detectar ramos impossíveis ou divisão por zero).

Sensibilidade ao fluxo e ao contexto

Dois ajustes principais:

Sensível ao fluxo (flow-sensitive): fatos dependem do ponto do programa (mais preciso, mais caro).
Sensível ao contexto (context-sensitive): fatos dependem do contexto de chamada (mais preciso entre procedimentos, mais caro).

Para sistemas grandes, analisadores frequentemente escolhem sensibilidade seletiva (por exemplo, sensível ao contexto para funções pequenas, ou apenas para código crítico de segurança).

Interpretação abstrata

Interpretação abstrata (abstract interpretation) é uma teoria geral para projetar análises estáticas sólidas aproximando a semântica de programas.

Ideia central

Em vez de executar o programa em estados concretos (valores exatos de memória), nós o executamos em estados abstratos (abstract states) que resumem muitos estados concretos possíveis.

Domínio concreto (concrete domain): todos os estados exatos possíveis do programa (enorme/infinito).
Domínio abstrato (abstract domain): um espaço de resumo tratável (intervalos, sinais, formas, etc.).

Uma abstração sólida garante que, se a análise abstrata diz “seguro”, então todas as execuções concretas são seguras em relação à propriedade verificada.

Exemplo: análise por intervalos

A análise por intervalos rastreia cada variável como um intervalo ([min, max]).

int g(int n) {
  int x = n;
  if (x < 0) x = -x;     // absolute value
  int y = 10 / x;
  return y;
}

Se n pode ser 0, então x pode ser 0, e 10 / x pode dividir por zero. A análise por intervalos poderia computar:

inicialmente: x ∈ [-∞, +∞]
após if (x < 0) x = -x: x ∈ [0, +∞]
divisão 10 / x: problemática porque o intervalo inclui 0 → reporta um possível erro

Isso é sólido (não perde o bug real), mas pode ser impreciso em outras situações. Por exemplo, se você também tivesse if (n != 0) ..., uma análise por intervalos grosseira ainda poderia incluir 0 a menos que rastreie restrições relacionais.

Pontos fixos, widening, narrowing

Laços criam equações como “o estado na cabeça do laço depende de si mesmo”, exigindo um cálculo de ponto fixo.

Como domínios abstratos podem ter cadeias ascendentes infinitas (por exemplo, intervalos podem continuar aumentando), a interpretação abstrata usa:

alargamento (widening): força a convergência rapidamente por superaproximar o crescimento
estreitamento (narrowing): opcionalmente refina o resultado depois

Essa é uma razão-chave pela qual a interpretação abstrata escala para código real mantendo solidez.

Além de intervalos: domínios abstratos mais ricos

Octógonos / poliedros: rastreiam relações como x - y ≤ c (mais preciso, mais custoso)
Domínios de alias/points-to: raciocinam sobre referências no heap
Análise de forma (shape analysis): propriedades de listas/árvores ligadas
Domínios numéricos para verificação de ML: domínios abstratos adaptados a camadas de redes neurais (por exemplo, relaxações lineares), frequentemente usados para verificar propriedades de robustez de Redes Neurais

Execução simbólica

Execução simbólica (symbolic execution) executa um programa usando entradas simbólicas (symbolic inputs) em vez de valores concretos. Ela rastreia:

um estado simbólico (symbolic state) (expressões sobre símbolos de entrada)
uma condição de caminho (path condition): restrições que precisam valer para seguir o caminho atual

Quando o executor encontra um desvio como if (x > 0), ele bifurca:

um caminho adiciona a restrição x > 0
o outro adiciona x ≤ 0

Exemplo: gerando uma entrada de contraexemplo

int h(int x, int y) {
  if (x > 0) {
    if (y == x + 1) {
      assert(y != 5);
    }
  }
  return 0;
}

A execução simbólica define x = X, y = Y inicialmente.

Para violar a asserção y != 5 (isto é, fazer y == 5) ao longo do caminho aninhado, precisamos:

X > 0
Y == X + 1
Y == 5

Isso se torna um problema de resolução de restrições. Um solver pode encontrar X = 4, Y = 5, produzindo uma entrada concreta de contraexemplo que dispara a asserção.

Desafios

Explosão de caminhos (path explosion): o número de caminhos cresce exponencialmente com desvios e laços.
Complexidade das restrições: restrições podem envolver strings, bit-vectors, heap, ponto flutuante etc.
Modelagem do ambiente (environment modeling): chamadas de sistema, bibliotecas, concorrência complicam uma execução fiel.

Para escalar, ferramentas usam poda (por exemplo, orientação por cobertura), sumários, fusão de estados ou limitam a profundidade de exploração.

Execução concolic

A execução concolic (concrete + symbolic) executa o programa concretamente enquanto constrói restrições simbólicas, sendo frequentemente usada em testes automatizados. Ela pode ser mais escalável do que a execução simbólica pura e combina bem com fuzzing.

Resolução SAT/SMT na análise de programas

Muitas técnicas de análise de programas reduzem perguntas sobre programas a resolução de restrições (constraint solving):

SAT: satisfatibilidade de lógica proposicional (variáveis booleanas)
SMT: satisfatibilidade módulo teorias—lógica de primeira ordem com teorias de fundo como:
- bit-vectors (inteiros de máquina)
- arrays (modelagem de memória)
- aritmética linear
- funções não interpretadas
- ponto flutuante (com suporte crescente, mas caro)

Isso é intimamente relacionado a Satisfação de Restrições: a análise de programas frequentemente gera restrições e usa solvers como backends.

Como os solvers são usados

Descarregar condições de verificação (discharging verification conditions): provar asserções, pré/pós-condições, invariantes.
Encontrar contraexemplos: se as restrições são satisfatíveis, extrair um modelo (entrada) que dispara um bug.
Laços de refinamento (refinement loops): usar contraexemplos para refinar abstrações (ver CEGAR abaixo).
Núcleos insatisfatíveis (unsat cores): identificar quais restrições causam inconsistência, útil para depurar especificações ou minimizar condições de falha.

Verificação por modelo limitada (BMC)

BMC desenrola laços até um limite k e codifica o programa finito resultante em SAT/SMT. Se encontrar uma violação dentro de k passos, retorna um rastro de contraexemplo concreto. Se não encontrar, isso não necessariamente prova corretude além do limite (a menos que raciocínio adicional seja usado).

BMC é amplamente usada porque muitas vezes é eficaz para encontrar bugs reais rapidamente.

CEGAR (Refinamento de Abstração Guiado por Contraexemplo)

Uma arquitetura comum para verificação escalável:

Começar com uma abstração grosseira (barata, possivelmente imprecisa).
Se ela reportar “seguro”, aceitar.
Se ela reportar um contraexemplo, checar se é real usando uma consulta precisa ao solver.
Se for espúrio, refinar a abstração para eliminá-lo e repetir.

CEGAR é uma ponte prática entre interpretação abstrata e precisão alimentada por SMT.

Propriedades e análises típicas

Propriedades de safety

desreferenciamento de nulo
estouro de buffer / fora dos limites (out-of-bounds)
uso após liberação (use-after-free), dupla liberação (double free)
overflow de inteiro
condições de corrida (com análises conscientes de concorrência)

Algumas são tratadas com análises leves (sistemas de tipos, checagens locais), outras exigem raciocínio interprocedural mais profundo.

Propriedades de security

Análises de segurança comuns incluem:

Análise de taint: rastrear dados de fontes não confiáveis (requisição HTTP, arquivo, entrada do usuário) até sinks sensíveis (consultas SQL, execução de shell).
Fluxo de informação (information flow): garantir que segredos não vazem para saídas públicas (propriedades no estilo não interferência).
Checagens de privilégio e política: garantir que regras de controle de acesso sejam respeitadas.

A análise de taint frequentemente é implementada como uma análise de fluxo de dados especializada com fontes/sinks e sanitizers específicos do domínio.

Análise de terminação e recursos

Terminação é mais difícil do que checagem de safety (terminação geral é indecidível), mas existem aproximações úteis:

encontrar funções de ranking (ranking functions) que diminuem a cada iteração de laço
usar interpretação abstrata sobre domínios bem fundamentados
inferir limites de custo (análise amortizada, resolução de recorrências)

Essas técnicas importam em sistemas de tempo real, contratos inteligentes e código crítico de segurança.

Aplicações práticas

Otimização de compiladores

Análises clássicas de fluxo de dados (liveness, reaching definitions, available expressions) são fundamentais para:

eliminação de código morto
alocação de registradores
eliminação de subexpressões comuns
dobramento/propagação de constantes

Mesmo quando o objetivo é desempenho e não corretude, o raciocínio subjacente é análise de programas.

Descoberta de bugs em CI

Muitas organizações executam analisadores estáticos a cada mudança para capturar problemas cedo:

incompatibilidades de nulabilidade
vazamentos de recursos
uso perigoso de APIs
erros de concorrência

Ferramentas modernas frequentemente priorizam relatórios acionáveis em vez de solidez total, porque a atenção de desenvolvedores é limitada.

Auditoria de segurança e conformidade

A análise de programas apoia:

encontrar vulnerabilidades de injeção
provar propriedades de implementações de protocolos criptográficos (em configurações restritas)
verificar conformidade com políticas (por exemplo, “PII nunca chega aos logs”)

Verificação de sistemas com IA

Em sistemas com forte presença de IA, a análise de programas aparece de pelo menos duas formas:

Analisar o software ao redor: pipelines de dados, extração de atributos, pós-processamento e checagens de safety ainda são código comum e se beneficiam de análise.
Raciocínio formal sobre componentes aprendidos: análises especializadas podem verificar propriedades limitadas de Redes Neurais, como robustez a pequenas perturbações. Muitas abordagens reutilizam ideias de interpretação abstrata (superaproximando o comportamento da rede) e resolução SMT/MILP (buscando contraexemplos adversariais).

Realidades de engenharia: por que análise é difícil

Aliasing e o heap

Ponteiros e heaps mutáveis complicam o raciocínio: muitos nomes de variáveis podem se referir ao mesmo local de memória. As análises frequentemente precisam de uma análise de points-to/alias (points-to/alias analysis) como pré-requisito.

Escolhas de precisão incluem:

modelagem de heap sensível a campos vs insensível a campos
abstração por local de alocação (agrupar objetos por onde foram alocados)
abstrações de forma para listas/árvores

Análise interprocedural

Programas reais são modulares. Para escalar, analisadores computam sumários de função (function summaries) (pré/pós-condições, efeitos) e os reutilizam nos pontos de chamada. Sensibilidade ao contexto melhora a precisão, mas pode explodir o custo.

Concorrência

Threads introduzem entrelaçamentos. Muitas ferramentas usam:

análises de lockset (heurística)
raciocínio happens-before
exploração limitada com model checking
detectores dinâmicos de corrida

A análise de concorrência permanece uma das áreas mais desafiadoras.

Conexões com outros tópicos de IA simbólica

A análise de programas está profundamente ligada a outros temas de IA clássica:

Ela depende de formalismos lógicos e representações simbólicas, conectando-se a Representação de Conhecimento.
Ela usa SAT/SMT e propagação de restrições como motores centrais, sobrepondo-se a Satisfação de Restrições.
Ela apoia a construção automatizada de programas via laços de síntese como síntese indutiva guiada por contraexemplo (CEGIS) (counterexample-guided inductive synthesis (CEGIS)) — uma técnica importante em Síntese de Programas.
Muitos fluxos de verificação e síntese se assemelham a planejamento sobre espaços de estados simbólicos (escolher ações/transformações para alcançar um objetivo), ecoando ideias de Planejamento (Simbólico).

Ferramentas e ecossistemas comuns (representativos)

Embora o campo seja amplo, estas categorias são comuns na prática:

Frameworks de interpretação abstrata (por exemplo, analisadores industriais, plataformas acadêmicas)
Motores de execução simbólica (por exemplo, ferramentas no estilo KLEE)
Model checkers / ferramentas de BMC (por exemplo, verificadores limitados no estilo CBMC)
Solvers SMT (por exemplo, Z3, CVC5) usados como backends para restrições e contraexemplos
Analisadores estáticos de produção integrados a revisão de código e CI (frequentemente misturando heurísticas com núcleos formais)

A escolha de ferramentas depende fortemente da linguagem (C/C++ vs Java vs Rust), do modelo de runtime e de quais propriedades importam.

Resumo

A análise de programas fornece maneiras automatizadas de compreender e restringir o comportamento de programas. Os pilares principais incluem:

Análise de fluxo de dados: propagação escalável de fatos em CFGs
Interpretação abstrata: aproximação sólida e principiada via domínios abstratos e pontos fixos
Execução simbólica: exploração baseada em caminhos usando valores simbólicos e restrições
Resolução SAT/SMT: um backend poderoso para provar condições ou gerar entradas de contraexemplo

No software moderno — e especialmente em sistemas de IA críticos para safety e security — a análise de programas é tanto um conjunto de ferramentas prático quanto um exemplo central de raciocínio simbólico clássico aplicado à engenharia do mundo real.