Execução Simbólica

Visão geral

Execução simbólica (Symbolic execution) é uma técnica de análise de programas que executa um programa sobre entradas simbólicas em vez de valores concretos. Em vez de executar um programa uma vez para uma única entrada, a execução simbólica explora muitas execuções possíveis ao mesmo tempo, rastreando:

Expressões simbólicas (symbolic expressions) para variáveis do programa (por exemplo, x = α + 1 em vez de x = 42)
Uma condição de caminho (path condition, PC): uma fórmula lógica que descreve as restrições que devem valer para que a execução siga o caminho atual

Sempre que o programa ramifica (por exemplo, if (x > 0)), a execução simbólica conceitualmente bifurca:

um estado assume x > 0 e adiciona isso à condição de caminho
o outro estado assume x <= 0 e adiciona isso em seu lugar

Um caminho é viável se sua condição de caminho for satisfatível. Determinar a viabilidade e gerar entradas de exemplo normalmente é feito com solucionadores SAT/SMT (SAT/SMT solvers), conectando a execução simbólica de perto a tópicos de satisfação de restrições como Resolução SAT e Resolução SMT.

A execução simbólica é amplamente usada para:

Encontrar bugs (falhas de asserção, crashes, estouros de inteiro)
Geração de testes (testes unitários de alta cobertura, testes de regressão)
Análise de segurança (encontrar caminhos de exploração, descoberta de vulnerabilidades no estilo taint)

Conceitos centrais

Entradas simbólicas e estado simbólico

Na execução simbólica, algumas entradas do programa são tratadas como símbolos (desconhecidos). Por exemplo, se x é simbólico, podemos representá-lo como α (uma variável simbólica).

À medida que o programa executa, cada variável do programa torna-se uma expressão sobre entradas simbólicas:

Se y = x + 2 e x = α, então y = α + 2
Se z = y * y, então z = (α + 2)^2

A análise mantém um estado simbólico (symbolic state), geralmente consistindo de:

um mapeamento de variáveis do programa (e posições de memória) para expressões simbólicas
a condição de caminho atual

Condições de caminho

Uma condição de caminho é uma conjunção de restrições acumuladas a partir de ramificações:

após if (x > 0) no lado “then”, a PC inclui α > 0
após outra verificação if (x < 10) no lado “then”, a PC inclui α > 0 ∧ α < 10

A PC caracteriza com precisão o conjunto de entradas que fazem aquele caminho executar.

Viabilidade via SAT/SMT

Para decidir se um caminho é viável (e para produzir entradas concretas), a execução simbólica consulta um solucionador:

Se as restrições forem puramente booleanas, um backend de Solucionadores SAT é suficiente.
Programas reais envolvem inteiros, vetores de bits, arrays, ponteiros e mais, então as ferramentas geralmente dependem de SMT (Satisfatibilidade Módulo Teorias) via sistemas como Z3 ou CVC5. Veja Satisfatibilidade Módulo Teorias (SMT).

Se o solucionador encontrar uma atribuição satisfatória, ele fornece um modelo (model) (valores concretos para entradas simbólicas) que pode ser transformado em um caso de teste.

Um exemplo prático: explorando caminhos e gerando testes

Considere esta função em estilo C:

int foo(int x, int y) {
    if (x > 10) {
        if (y == x + 1) {
            return 1;
        } else {
            return 2;
        }
    } else {
        return 3;
    }
}

Considere x = α e y = β como simbólicos.

Em if (x > 10), bifurque:
- Caminho A: PC = (α > 10)
- Caminho B: PC = (α <= 10)
No Caminho A, em if (y == x + 1), bifurque novamente:
- Caminho A1: PC = (α > 10) ∧ (β = α + 1)
- Caminho A2: PC = (α > 10) ∧ (β ≠ α + 1)

Agora você tem três caminhos finais (A1 retorna 1, A2 retorna 2, B retorna 3). Um solucionador pode gerar testes concretos:

Para (α <= 10), um modelo é α = 0 (β pode ser qualquer coisa)
Para (α > 10) ∧ (β = α + 1), um modelo é α = 11, β = 12
Para (α > 10) ∧ (β ≠ α + 1), um modelo é α = 11, β = 0

Esses se tornam três testes que cobrem todos os retornos.

Exemplo de busca de bug (divisão por zero)

int bar(int x, int y) {
    if (x > 5) {
        return y / (x - 6);
    }
    return 0;
}

No ramo x > 5, a expressão divide por (x - 6). A execução simbólica forma:

PC: α > 5
Condição potencial de crash: (α - 6) = 0 ou seja α = 6

É satisfatível? Sim: α = 6 satisfaz α > 5. O motor produz um contraexemplo concreto como (x=6, y=1) que dispara divisão por zero.

Essa é a essência da busca de bugs simbólica: reduzir “isso pode crashar?” a “esta restrição é satisfatível?”.

Como um motor de execução simbólica funciona (alto nível)

Um motor típico de execução simbólica para frente realiza:

Inicialização
- Marcar entradas escolhidas como simbólicas (argumentos de função, bytes de stdin, conteúdo de arquivo etc.)
- Definir PC = true
Execução passo a passo
- Interpretar instruções, atualizando expressões simbólicas para registradores/variáveis/memória
Tratamento de ramificações
- Em if (cond), computar a condição simbólica C
- Bifurcar estados:
  - adicionar C à PC para o estado “true”
  - adicionar ¬C à PC para o estado “false”
Checagem de viabilidade
- Consultar periodicamente o solucionador para descartar cedo estados inviáveis
Término
- Ao alcançar locais-alvo (por exemplo, falha de asserção), pedir ao solucionador um modelo para produzir entradas concretas

Modelagem de memória (por que é difícil)

Programas reais usam heaps, pilhas, ponteiros, arrays, structs e aliasing. A execução simbólica deve modelar memória com precisão suficiente para ser útil, comumente usando:

Vetores de bits (bit-vectors) para inteiros de máquina (para corresponder à semântica de overflow)
Teoria de arrays (array theory) para memória: tratar memória como um mapeamento de endereços para bytes/palavras
Aproximações ou modelos parciais para comportamento complexo de bibliotecas/sistema

Trade-off: modelos mais fiéis aumentam a carga sobre o solucionador.

Resolução de restrições na prática

SAT vs SMT na execução simbólica

Condições de execução simbólica frequentemente incluem:

aritmética em nível de bits ((x * 3) & 7 == 5)
comparações com sinal/sem sinal
leituras/escritas de memória em índices simbólicos
restrições de strings e caracteres

Isso é naturalmente expresso com teorias SMT como:

Vetores de bits (precisos para aritmética de máquina)
Arrays (para memória)
Funções não interpretadas (uninterpreted functions) (para abstrair código desconhecido)
Às vezes strings (em análises de nível mais alto)

Por isso, motores de execução simbólica geralmente geram consultas SMT em vez de SAT puro.

Otimizações comuns de solucionadores

Motores de execução simbólica dependem fortemente do desempenho do solucionador. Técnicas comuns incluem:

Resolução incremental (incremental solving): reutilizar um contexto do solucionador enquanto empilha/desempilha restrições conforme a condição de caminho muda.
Cache/memoização de restrições (constraint caching/memoization): se a mesma (ou similar) PC for checada repetidamente, reutilizar resultados.
Simplificação (simplification): propagação de constantes e simplificações algébricas antes de consultar o solucionador.
Adição preguiçosa de restrições (lazy constraint addition): adiar restrições caras até serem necessárias (por exemplo, checar contradições fáceis primeiro).

Estratégias de busca e gerenciamento de caminhos

A execução simbólica explora uma árvore de caminhos. Mesmo programas pequenos podem ter um número exponencial de caminhos, conhecido como o problema da explosão de caminhos (path explosion problem).

Estratégias de exploração

Motores escolhem qual estado explorar em seguida usando estratégias como:

Busca em profundidade (depth-first search, DFS): baixa memória, alcança bugs profundos rapidamente, mas pode ficar presa em laços profundos.
Busca em largura (breadth-first search, BFS): sistemática, mas pesada em memória.
Heurísticas guiadas por cobertura (coverage-guided heuristics): priorizar estados com maior chance de atingir código novo.
Busca direcionada (targeted search): guiar em direção a um local específico (por exemplo, um ponto de crash ou um sink sensível à segurança).

Poda de caminhos e técnicas de escalabilidade

Para lidar com explosão de caminhos, a execução simbólica prática usa muitas técnicas de poda:

Checagens precoces de inviabilidade (early infeasibility checks): consultar o solucionador nas ramificações para eliminar rapidamente caminhos impossíveis.
Mesclagem de estados (state merging): mesclar dois estados em pontos de junção usando expressões if-then-else:
- por exemplo, x = ite(c, x1, x2)
- reduz estados, mas torna restrições mais difíceis.
Subsunção / equivalência (subsumption / equivalence): se a PC de um novo estado implica a PC de um estado existente no mesmo ponto do programa, o novo estado pode ser redundante.
Sumarização de funções (function summarization): computar sumários para funções (relações entrada-saída) e reutilizá-los.
Limitação de laços (loop bounding): limitar iterações de laços (útil para busca de bugs e geração de testes limitada).
Fatiamento (slicing): focar restrições apenas em variáveis relevantes para a propriedade verificada (por exemplo, uma asserção).

Essas ideias se sobrepõem a tópicos mais amplos de verificação como Verificação de Modelos, onde a explosão de estados também é central.

Execução concolic (concreta + simbólica)

Execução concolic (concolic execution) (CONCrete + symbOLIC) é uma abordagem híbrida:

Executar o programa concretamente com entradas específicas (assim você sempre tem um rastro real).
Ao longo desse rastro, também construir restrições simbólicas para cada ramificação.
Para gerar um novo teste, negar uma condição de ramificação no prefixo da condição de caminho e resolver para novas entradas.

Isso tem vantagens importantes:

Lida com comportamento complexo de tempo de execução (chamadas de sistema, bibliotecas) de forma mais robusta porque a execução concreta “mostra o que realmente aconteceu”.
Ainda usa resolução de restrições para inverter ramificações de forma sistemática e explorar novos caminhos.

Fluxo de trabalho concolic simples

Suponha que uma execução tomou ramificações b1=true, b2=false, b3=true. As restrições coletadas podem ser:

C1 (para b1=true)
C2 (para b2=false, significando ¬C2_original)
C3 (para b3=true)

Para explorar um novo caminho, você pode inverter b2 e manter restrições anteriores:

Nova PC: C1 ∧ (C2_original)
Resolva para obter uma nova entrada concreta que force o ramo oposto em b2.

A execução concolic é uma base comum para geração automatizada de testes e frequentemente é combinada com mutação de entrada no estilo fuzzing em ferramentas modernas.

Para que a execução simbólica é usada

1) Busca de bugs e reprodução de crashes

A execução simbólica pode detectar:

violações de asserção (assert(x != 0))
divisão por zero
desreferenciação de ponteiro nulo (se modelado)
acessos fora dos limites (com modelos de memória adequados)
estouros de inteiro (particularmente com semântica de vetores de bits)

Um benefício-chave é entradas de reprodução acionáveis: o modelo gerado pelo solucionador vira um teste concreto que dispara o bug.

2) Geração automatizada de testes

Como toda condição de caminho viável corresponde a uma classe de entradas, a execução simbólica é um gerador natural de testes caixa-branca (white-box):

Gerar testes unitários que cobrem ramificações e condições
Produzir testes de regressão a partir de bugs descobertos
Explorar código de tratamento de erros que o fuzzing pode não alcançar

Na prática, metas de cobertura costumam ser usadas para interromper a exploração quando cobertura suficiente é atingida.

3) Análise de segurança

A execução simbólica é amplamente usada em segurança para tarefas como:

Encontrar entradas que alcancem estados perigosos (por exemplo, escritas em buffer com índices controlados pelo atacante)
Gerar exploits de prova de conceito (sob suposições/modelos adicionais)
Analisar binários em busca de padrões de vulnerabilidade

Um padrão comum é alcançabilidade (reachability): “Existe alguma entrada tal que a execução alcança esta instrução com estas condições?” Isso se torna uma consulta de satisfatibilidade.

4) Compreensão de programas e engenharia reversa

A execução simbólica pode ajudar a inferir:

restrições sobre entradas necessárias para alcançar certo código
formatos de protocolo/mensagem (bytes que devem satisfazer verificações)
equivalência/diferenças entre duas implementações (mais avançado, frequentemente combinado com outros métodos)

Limitações e considerações práticas

Explosão de caminhos (o principal gargalo)

Mesmo com poda, softwares reais podem gerar caminhos demais:

laços com condições simbólicas
condicionais aninhados
lógica de parsing complexa (muitas ramificações por byte de entrada)

Mitigações comuns:

limitar laços
restringir quais entradas são simbólicas (execução simbólica seletiva)
misturar com execução concolic e heurísticas

Restrições difíceis e timeouts do solucionador

Algumas restrições são caras:

aritmética não linear
muita manipulação de bits e código criptográfico
memória simbólica com muitas leituras/escritas em índices simbólicos

Motores podem:

aproximar partes do código (sumários, funções não interpretadas)
concretizar alguns valores oportunisticamente
impor timeouts ao solucionador e seguir em frente

Ambiente e chamadas externas

Programas interagem com APIs do SO, arquivos, rede e bibliotecas. Opções incluem:

modelagem (modeling): fornecer modelos simbólicos para funções comuns (por exemplo, strlen, memcmp)
stubbing: aproximar o comportamento (mais rápido, mas menos preciso)
execução concolic: depender da execução concreta para o comportamento real, enquanto ainda coleta restrições simbólicas

Solidez vs utilidade

A execução simbólica costuma ser precisa nos caminhos explorados, mas os resultados gerais dependem de:

o que foi modelado simbolicamente
se laços/recursão foram limitados
como chamadas externas foram tratadas

Muitas ferramentas são projetadas para busca de bugs (encontrar problemas reais rapidamente) em vez de prova completa de correção.

Relação com técnicas próximas

Execução simbólica vs verificação de modelos

Ambas exploram comportamentos do programa sistematicamente, mas diferem na ênfase:

Execução simbólica: baseada em caminhos; produz condições de caminho e entradas concretas; frequentemente usada para geração de testes e busca de bugs.
Verificação de modelos: baseada em estados; checa propriedades temporais/lógicas sobre um modelo; frequentemente foca em verificação exaustiva de abstrações de estados finitos.

Na prática, há sobreposição — técnicas limitadas e codificações baseadas em SMT são comuns em ambas. Veja Verificação de Modelos.

Execução simbólica vs interpretação abstrata

Interpretação abstrata (abstract interpretation) superaproxima conjuntos de estados para provar propriedades (buscando solidez).
Execução simbólica frequentemente enumera caminhos viáveis (pode ser muito precisa por caminho), mas pode ser incompleta devido à explosão de caminhos e limites.

Muitas ferramentas reais combinam ideias de ambas (por exemplo, usar interpretação abstrata para podar, ou usar execução simbólica seletivamente).

Ferramentas (o que você verá na prática)

Embora ferramentas específicas variem por linguagem e domínio, a maioria dos sistemas modernos de execução simbólica inclui:

um front-end que eleva o código (fonte, IR, ou binário) para uma representação intermediária
um motor de execução que mantém estado simbólico e PCs
um construtor de restrições que emite fórmulas SMT (frequentemente vetores de bits + arrays)
uma interface de solucionador (por exemplo, Z3/CVC5) com resolução incremental
heurísticas de busca, rastreamento de cobertura e limites de recursos

Se você está aprendendo execução simbólica, normalmente é mais fácil começar no nível de IR (IR level) (estilo LLVM) porque a semântica das instruções é explícita e consistente.

Quando usar execução simbólica (e quando não usar)

A execução simbólica é uma escolha forte quando você precisa de:

testes de alta cobertura para código com muitas ramificações difíceis
entradas reprodutíveis que causam crash para bugs
respostas de alcançabilidade para auditoria de segurança (“uma entrada do atacante pode chegar aqui?”)

É menos adequada quando:

o programa depende fortemente de ambientes complexos que você não consegue modelar
as restrições são dominadas por matemática/cripto difíceis
você precisa de provas completas sem limites (a menos que combinada com métodos de verificação mais fortes)

Resumo

A execução simbólica trata entradas como símbolos, executa código enquanto constrói condições de caminho, e usa resolução SAT/SMT para determinar quais caminhos são viáveis e para produzir entradas concretas. Motores práticos precisam combater a explosão de caminhos com heurísticas de busca, poda, mesclagem e abordagens híbridas como execução concolic. Apesar das limitações, a execução simbólica continua sendo uma das técnicas baseadas em restrições mais eficazes para busca de bugs, geração automatizada de testes e análise de segurança, e forma uma ponte prática entre o comportamento de software no mundo real e a maquinaria de resolução de restrições discutida em Resolução SAT e Resolução SMT.