Tu test suite tiene un 94% de cobertura y cero fallos. Un motor de ejecución simbólica encuentra un crash en tu código en menos de tres segundos.

El test no está roto. La metric de cobertura no miente. El problema es que probar verifica el comportamiento en puntos específicos. La ejecución simbólica verifica el comportamiento a través de regiones enteras del espacio de entrada. No importa cuántos ejemplos escribas si el bug vive en el hueco entre dos de ellos.

Qué hace realmente la ejecución simbólica

La ejecución simbólica es una técnica de análisis de programas que ejecuta tu código con variables simbólicas en lugar de valores concretos. Un test normal pasa x = 5 a una función. Un motor de ejecución simbólica pasa x = α, donde α representa cada entero posible.

A medida que el código se ejecuta, el motor rastrea constraints. Cuando llega a una branch como if (x > 0), no elige una dirección. Hace fork de la ejecución. Un path lleva el constraint α > 0. El otro lleva α ≤ 0. Ambos paths continúan independientemente.

Cuando un path llega a una assertion, un acceso a memoria o un sitio de crash potencial, el motor le pregunta a un SMT solver una pregunta simple: “¿Existe algún valor de α que satisfaga todos los constraints en este path y también viole esta safety property?” Si el solver dice sí, devuelve un contraejemplo concreto. Ahora tienes una entrada específica que desencadena un bug para el que nunca escribiste un test.

El bug que tus unit tests no atraparán

Considera una función que valida los límites de un 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;
}

Tu test suite parece razonable:

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);
}

Todo verde. Pero offset y count son size_t, enteros sin signo. En un sistema de 64 bits, offset + count puede hacer wrap around a un número pequeño si ambos son grandes. Si offset = 0xFFFFFFFFFFFFFFFF y count = 1, entonces end = 0, que no es mayor que src_len. El bounds check pasa. memcpy lee desde una dirección inválida.

Ningún desarrollador razonable escribe un test case con offset = 2^64 - 1. El espacio de entrada es incomprensiblemente grande. La ejecución simbólica no necesita que adivines la entrada mala. Explora el path donde ocurre el wraparound y le pide al solver que encuentre valores que satisfagan el constraint end ≤ src_len mientras offset + count hace overflow. El solver devuelve el contraejemplo en milisegundos.

Cómo el motor explora paths

El mecanismo central es la recolección de constraints y el fork de paths. Cada sentencia condicional en tu código se convierte en un punto de branch. El motor mantiene un path constraint, una fórmula booleana que representa todas las condiciones que deben ser verdaderas para que la ejecución llegue al punto actual.

En cada branch, el motor query al solver:

  1. ¿Es satisfiable el path constraint actual más la condición de la branch verdadera?
  2. ¿Es satisfiable el path constraint actual más la condición de la branch falsa?

Si ambas son satisfiables, el motor hace fork. Encola ambos paths para exploración. Así es como la ejecución simbólica logra cobertura exhaustiva de paths para programas bounded.

Cuando un path llega a un crash, un acceso out-of-bounds o una assertion fallida, el motor le pide al solver una asignación satisfactoria de las entradas simbólicas bajo el path constraint actual. Esa asignación es tu entrada que desencadena el bug.

Puedes ver el paso de constraint-solving directamente con Z3, el SMT solver que potencia muchos motores de ejecución 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

El solver devuelve valores concretos que satisfacen el constraint de overflow. Este es el núcleo matemático de la ejecución simbólica. El motor hace esto automáticamente a través de cada branch en tu programa.

Los trade-offs que evitan que reemplace tu test suite

La ejecución simbólica no es gratis. Hay tres costos que limitan dónde es práctica.

Path explosion. Cada sentencia if duplica el número de paths. Una función con 20 branches independientes tiene más de un millón de paths. La mayoría de los motores se rinden después de un timeout o un presupuesto de paths. Los loops empeoran esto. Un loop que itera simbólicamente sobre un rango unbounded crea infinitos paths. Los motores típicamente desenrollan loops un número fijo de veces y siguen adelante.

Estado externo y system calls. La ejecución simbólica funciona mejor en funciones puras. Cuando tu código lee de un archivo, hace una network request o query una base de datos, el motor no tiene idea de qué valor volverá. Algunas herramientas modelan llamadas comunes de biblioteca heurísticamente. Otras requieren que escribas mock models. Esto es tedioso y propenso a errores.

Timeouts del solver. Las fórmulas de constraint para código real son complejas. Arrays, bitvectors, aritmética de punto flotante y matemáticas no lineales pueden empujar a un SMT solver a tiempo exponencial. Un path que toma microsegundos para ejecutarse concretamente podría tomar minutos para resolverse simbólicamente. Los motores descartan estos paths y los reportan como unresolved.

Debido a estos límites, la ejecución simbólica es un plugin de las pruebas, no un reemplazo. Encuentra los casos esquina profundos. Tus tests verifican los casos comunes y el comportamiento de integración.

Tres formas de probarlo en código real

No necesitas un doctorado para ejecutar ejecución simbólica. Las herramientas modernas ocultan la mayor parte de la complejidad.

Para C/C++: KLEE. KLEE es el motor clásico de ejecución simbólica de código abierto construido sobre LLVM. Compilas tu código a bitcode de LLVM con clang -emit-llvm, luego ejecutas klee sobre el resultado. KLEE ha encontrado bugs graves en GNU coreutils, SQLite y otros codebases de C ampliamente usados.

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

KLEE genera archivos .ktest para cada bug que encuentra. Puedes reproducirlos con un pequeño runtime para ver las entradas exactas.

Para Python y binarios: angr. angr es un framework de Python para ejecución simbólica, análisis de binarios e ingeniería inversa. Funciona en binarios compilados, así que no necesitas código fuente. Escribes un script de Python para configurar registries simbólicos y memoria, luego dejas que angr explore.

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 es más lento que KLEE pero maneja binarios del mundo real con todas sus convenciones de llamada desordenadas y dependencias de bibliotecas.

Para Rust: Kani. Kani es un verificador específico de Rust construido sobre CBMC. Anotas una función con #[kani::proof] y ejecutas cargo kani. Comprueba arithmetic overflows, accesos out-of-bounds y fallos de assertion usando ejecución simbólica bajo el capó.

#[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 es la rampa de acceso más fácil si ya estás en el ecosistema de Rust. Se integra con cargo y te da trazas de error en un formato familiar.

Preguntas frecuentes

¿Reemplaza la ejecución simbólica al fuzzing?

No. Fuzzing genera entradas aleatorias y observa crashes. La ejecución simbólica razona sobre paths y encuentra entradas que satisfacen constraints específicos. Fuzzing escala a programas grandes y ejecuciones largas. La ejecución simbólica encuentra bugs más profundos en regiones más pequeñas. Las dos técnicas funcionan bien juntas. Herramientas como Driller y QSYM las combinan, usando fuzzing para cobertura y ejecución simbólica para branches difíciles de alcanzar.

¿Puede la ejecución simbólica probar que mi código no tiene bugs?

Solo para programas bounded sin loops unbounded y sin dependencias externas. Para la mayoría del código de producción, la ejecución simbólica puede probar la ausencia de ciertas clases de bugs hasta un límite de profundidad de path. No puede probar corrección total.

¿Cuánto tarda en ejecutarse?

Minutos a horas para funciones pequeñas. La ejecución simbólica no es un demonio de velocidad de CI. Ejecútala en funciones críticas de seguridad, parsers y código de boundary-checking. No intentes ejecutar simbólicamente todo tu web framework.

Empieza con una función

No necesitas ejecutar simbólicamente todo tu codebase. Elige una función donde un bug dolería. Un parser. Un chequeo de autorización. Una copia de buffer.

Escribe un harness de KLEE, un script de angr o una prueba de Kani. Ejecútalo. Míralo encontrar una entrada para la que nunca habrías escrito un test. Arregla el bug. Duerme mejor.

El objetivo no es reemplazar tus tests. El objetivo es dejar de pretender que un 94% de cobertura significa un 94% de seguridad. La ejecución simbólica encuentra los huecos. Tus tests nunca lo harán.