Sua test suite tem 94% de cobertura e zero falhas. Um motor de execução simbólica encontra um crash no seu código em menos de três segundos.

O teste não está quebrado. A metric de cobertura não está mentindo. O problema é que testes verificam comportamento em pontos específicos. Execução simbólica verifica comportamento em regiões inteiras do espaço de entrada. Não importa quantos exemplos você escreva se o bug vive no gap entre dois deles.

O Que a Execução Simbólica Realmente Faz

Execução simbólica é uma técnica de análise de programa que executa seu código com variáveis simbólicas em vez de valores concretos. Um teste normal passa x = 5 para uma função. Um motor de execução simbólica passa x = α, onde α representa todo inteiro possível.

À medida que o código roda, o motor rastreia constraints. Quando ele encontra um branch como if (x > 0), ele não escolhe uma direção. Ele bifurca a execução. Um caminho carrega a constraint α > 0. O outro carrega α ≤ 0. Ambos os caminhos continuam independentemente.

Quando um caminho alcança uma asserção, um acesso à memória ou um possível site de crash, o motor pergunta a um SMT solver uma pergunta simples: “Existe algum valor de α que satisfaça todas as constraints neste caminho e também viole esta propriedade de segurança?” Se o solver disser sim, ele devolve um contra-exemplo concreto. Você agora tem uma entrada específica que dispara um bug para o qual nunca escreveu um teste.

O Bug que Seus Unit Tests Não Vão Pegar

Considere uma função que valida limites de array antes de copiar:

int copy_slice(const char *src, size_t src_len,
               size_t offset, size_t count) {
    if (offset > src_len) return -1;
    if (count > 1024) return -1;

    size_t end = offset + count;
    if (end > src_len) return -1;

    char dst[1024];
    memcpy(dst, src + offset, count);
    return 0;
}

Sua test suite parece razoável:

void test_copy_slice_normal() {
    assert(copy_slice("hello", 5, 1, 3) == 0);
}

void test_copy_slice_too_long() {
    assert(copy_slice("hi", 2, 0, 1025) == -1);
}

void test_copy_slice_bad_offset() {
    assert(copy_slice("hi", 2, 5, 1) == -1);
}

Tudo verde. Mas offset e count são size_t, inteiros sem sinal. Em um sistema 64-bit, offset + count pode dar a volta (wrap around) para um número pequeno se ambos forem grandes. Se offset = 0xFFFFFFFFFFFFFFFF e count = 1, então end = 0, que não é maior que src_len. A verificação de limites passa. O memcpy lê de um endereço inválido.

Nenhum desenvolvedor razoável escreve um caso de teste com offset = 2^64 - 1. O espaço de entrada é incompreensivelmente grande. Execução simbólica não precisa que você adivinhe a entrada ruim. Ela explora o caminho onde o wraparound ocorre e pede ao solver para encontrar valores que satisfaçam a constraint end ≤ src_len enquanto offset + count overflow. O solver retorna o contra-exemplo em milissegundos.

Como o Motor Explora Caminhos

O mecanismo central é coleta de constraints e bifurcação de caminhos. Cada instrução condicional no seu código se torna um branch point. O motor mantém uma path constraint, uma fórmula booleana representando todas as condições que devem ser verdadeiras para a execução alcançar o ponto atual.

Em cada branch, o motor query o solver:

  1. A path constraint atual mais a condição do branch true é satisfatível?
  2. A path constraint atual mais a condição do branch false é satisfatível?

Se ambas são satisfatíveis, o motor bifurca. Ele enfileira ambos os caminhos para exploração. É assim que a execução simbólica alcança path coverage exaustiva para programas limitados.

Quando um caminho alcança um crash, um acesso out-of-bounds ou uma asserção falha, o motor pede ao solver uma atribuição satisfatória para as entradas simbólicas sob a path constraint atual. Essa atribuição é sua entrada que dispara o bug.

Você pode ver o passo de constraint solving diretamente com Z3, o SMT solver que alimenta muitos motores de execução simbólica:

from z3 import Solver, BitVec, UGT, ULT, ULE, simplify

solver = Solver()

# Model 32-bit unsigned size_t values
offset = BitVec('offset', 32)
count = BitVec('count', 32)
src_len = BitVec('src_len', 32)

# Path constraints: offset <= src_len, count <= 1024
solver.add(ULE(offset, src_len))
solver.add(ULE(count, 1024))

# We want to find a case where offset + count wraps around
# and the end check passes incorrectly
end = offset + count
solver.add(UGT(end, src_len))  # This should trigger the return -1

# But what if we look for the overflow case where end wraps?
solver2 = Solver()
solver2.add(ULE(offset, src_len))
solver2.add(ULE(count, 1024))
solver2.add(ULT(offset + count, offset))  # unsigned overflow
solver2.add(ULE(offset + count, src_len))  # bogus check passes

if solver2.check() == solver2.sat:
    model = solver2.model()
    print(f"offset={model[offset]}, count={model[count]}")
    # offset=4294967295, count=1 on a 32-bit model

O solver retorna valores concretos que satisfazem a constraint de overflow. Esse é o núcleo matemático da execução simbólica. O motor faz isso automaticamente por cada branch no seu programa.

Os Trade-offs que a Impedem de Substituir Sua test suite

Execução simbólica não é de graça. Há três custos que limitam onde ela é prática.

Path explosion. Cada instrução if dobra o número de caminhos. Uma função com 20 branches independentes tem mais de um milhão de caminhos. A maioria dos motores desiste após um timeout ou um path budget. Loops pioram isso. Um loop que itera simbolicamente sobre uma faixa ilimitada cria infinitos caminhos. Motores tipicamente desenrolam loops um número fixo de vezes e seguem em frente.

Estado externo e system calls. Execução simbólica funciona melhor em pure functions. Quando seu código lê de um arquivo, faz uma requisição de rede ou query um banco de dados, o motor não faz ideia de qual valor vai retornar. Algumas ferramentas modelam chamadas de biblioteca comuns heuristicamente. Outras exigem que você escreva mock models. Isso é tedioso e propenso a erros.

Timeouts do solver. As fórmulas de constraint para código real são complexas. Arrays, bitvectors, aritmética de ponto flutuante e matemática não-linear podem empurrar um SMT solver para tempo exponencial. Um caminho que leva microssegundos para executar concretamente pode levar minutos para resolver simbolicamente. Motores descartam esses caminhos e os reportam como unresolved.

Por causa desses limites, execução simbólica é um complemento para testes, não um substituto. Ela encontra os casos extremos profundos. Seus testes verificam os casos comuns e o comportamento de integração.

Três Maneiras de Experimentar em Código Real

Você não precisa de um PhD para rodar execução simbólica. Ferramentas modernas escondem a maior parte da complexidade.

Para C/C++: KLEE. KLEE é o motor de execução simbólica open-source clássico construído sobre LLVM. Você compila seu código para LLVM bitcode com clang -emit-llvm, depois roda klee no resultado. KLEE encontrou bugs sérios no GNU coreutils, SQLite e outros codebases C amplamente usados.

clang -emit-llvm -c -g copy_slice.c -o copy_slice.bc
klee --max-time=60 copy_slice.bc

KLEE gera arquivos .ktest para cada bug que encontra. Você pode reproduzi-los com um pequeno runtime para ver as entradas exatas.

Para Python e binários: angr. angr é um framework Python para execução simbólica, análise binária e engenharia reversa. Ele funciona em binários compilados, então você não precisa de código-fonte. Você escreve um script Python para configurar registradores e memória simbólicos, depois deixa o angr explorar.

import angr

proj = angr.Project("./copy_slice")
state = proj.factory.entry_state()
sm = proj.factory.simulation_manager(state)
sm.explore(find=lambda s: b"crash" in s.posix.dumps(1))

angr é mais lento que KLEE, mas lida com binários do mundo real com todas suas convenções de chamada confusas e dependencies de biblioteca.

Para Rust: Kani. Kani é um verificador específico para Rust construído sobre CBMC. Você anota uma função com #[kani::proof] e roda cargo kani. Ele verifica overflows aritméticos, acessos out-of-bounds e falhas de asserção usando execução simbólica por baixo dos panos.

#[kani::proof]
fn check_copy_slice() {
    let src = kani::any_slice::<u8, 1024>();
    let offset: usize = kani::any();
    let count: usize = kani::any();
    kani::assume(count <= 1024);
    let _ = copy_slice(src, src.len(), offset, count);
}

Kani é a rampa de acesso mais fácil se você já está no ecossistema Rust. Ele integra com cargo e te dá traces de erro em formato familiar.

Perguntas Frequentes

A execução simbólica substitui fuzzing?

Não. Fuzzing gera entradas aleatórias e observa crashes. Execução simbólica raciocina sobre caminhos e encontra entradas que satisfazem constraints específicas. Fuzzing escala para programas grandes e execuções longas. Execução simbólica encontra bugs mais profundos em regiões menores. As duas técnicas funcionam bem juntas. Ferramentas como Driller e QSYM as combinam, usando fuzzing para cobertura e execução simbólica para branches de difícil alcance.

A execução simbólica pode provar que meu código não tem bugs?

Apenas para programas limitados sem loops ilimitados e sem dependencies externas. Para a maioria do código de produção, execução simbólica pode provar a ausência de certas classes de bugs até um limite de profundidade de caminho. Ela não pode provar correção total.

Quanto tempo leva para rodar?

Minutos a horas para funções pequenas. Execução simbólica não é um speed demon de CI. Rode-a em funções críticas de segurança, parsers e código de verificação de limites. Não tente executar simbolicamente seu framework web inteiro.

Comece com Uma Função

Você não precisa executar simbolicamente seu codebase inteiro. Escolha uma função onde um bug doeria. Um parser. Uma verificação de autorização. Uma cópia de buffer.

Escreva um harness KLEE, um script angr ou uma proof Kani. Execute. Veja ela encontrar uma entrada que você nunca teria escrito um teste para. Corrija o bug. Durma melhor.

O objetivo não é substituir seus testes. O objetivo é parar de fingir que 94% de cobertura significa 94% de segurança. Execução simbólica encontra os gaps. Seus testes nunca vão.