Symbolic Execution

Foundations

Concrete vs. Symbolic Execution

In concrete execution, the program runs with specific input values, exploring a single path. In symbolic execution (King, 1976), input values are replaced by symbolic variables (e.g., α, β), and the program manipulates symbolic expressions rather than concrete values. Each variable holds a symbolic expression over the inputs, and each branch condition generates a constraint on those inputs.

Path Conditions

A path condition (PC) is a conjunction of constraints accumulated along an execution path. At each conditional branch if (cond):

The true branch appends cond to the PC
The false branch appends ¬cond to the PC

A path is feasible if its path condition is satisfiable (has a solution). The symbolic executor queries an SMT solver to check satisfiability. If the PC is unsatisfiable, the path is infeasible and can be pruned.

Symbolic State

A symbolic state consists of:

Program counter: current instruction
Symbolic store: mapping from variables to symbolic expressions
Path condition: conjunction of branch constraints
Execution tree: the tree of all explored paths

At each branch, the state forks into two children (or more, for switch statements). The execution tree grows exponentially with the number of branches.

Path Explosion

The fundamental scalability challenge: a program with n sequential branches has 2ⁿ paths. Loops with symbolic bounds create infinitely many paths. This path explosion problem limits pure symbolic execution to small programs or bounded exploration.

Mitigation Strategies

Bounded exploration: Limit loop iterations, recursion depth, or total path count. Sound for underapproximation (bug finding) but incomplete for verification.

Path merging: At join points, merge symbolic states from different paths. If-then-else becomes a conditional expression: x = ite(cond, e₁, e₂). Reduces path count but creates larger, harder SMT queries. Veritesting (Avgerinos et al., 2014) selectively merges paths through straight-line code while forking at complex control flow.

State pruning: Discard states that cannot reach interesting targets (guided by static analysis or heuristics). Reduce redundant exploration.

Function summaries: Compute a symbolic summary of a function's effect (input-output relation as a formula). Reuse the summary at subsequent call sites instead of re-exploring the function body.

Compositional symbolic execution: Analyze functions bottom-up, computing summaries lazily. When a summary is insufficient for a calling context, refine it. Reduces redundant exploration across call sites.

Concolic Execution

DART and Directed Automated Random Testing

Concolic (concrete + symbolic) execution (Godefroid, Klumpp, and Leino, 2005; Sen, Marinov, and Agha, 2005) runs the program concretely while maintaining a symbolic shadow state. The concrete execution drives the exploration through one specific path. After completing a path, the system negates the last unexplored branch constraint in the path condition and solves for a new input that takes the alternative branch.

Advantages over pure symbolic execution:

Concrete execution handles operations the symbolic engine cannot model (system calls, library functions, floating-point).
When symbolic reasoning fails, the concrete value provides a fallback — the analysis degrades gracefully rather than halting.
No need to model the entire environment symbolically.

Systematic exploration: By iteratively negating branch constraints in a depth-first (or other) order, concolic execution systematically covers new paths. The process terminates when all feasible paths are explored or a budget is exhausted.

Search Strategies

The order in which paths are explored dramatically affects coverage and bug-finding efficiency:

Depth-first search (DFS): Simple but can get stuck in deep paths (long loops).
Breadth-first search (BFS): Better coverage distribution but high memory usage.
Coverage-optimized search: Prioritize states closest to uncovered code. KLEE uses heuristics combining coverage, instruction count, and minimum distance to uncovered code.
Generational search (SAGE): Negate all unexplored branches from the current path, not just the last one. Each "generation" explores many new paths simultaneously. Used in Microsoft's SAGE whitebox fuzzer.
Random path selection: Avoids bias toward any particular region. Effective in combination with other strategies.

KLEE

KLEE (Cadar, Dunbar, and Engler, 2008) is a symbolic execution engine built on LLVM. Programs are compiled to LLVM bitcode, and KLEE interprets the bitcode symbolically.

Key design decisions:

Compact state representation: States sharing common prefixes use copy-on-write memory objects.
Environment modeling: Symbolic models for POSIX file system, standard library, environment variables. ~2500 lines of models enable testing of real Unix utilities.
Constraint optimization: Counterexample caching (reuse satisfying assignments), query independence (split constraints into independent subsets), incremental solving.
Seeding: Start with concrete inputs from existing test suites, then explore nearby paths symbolically.

Results: KLEE achieved over 90% line coverage on GNU Coreutils (89 tools), finding 56 serious bugs including in heavily tested utilities like ls and sort. Generated test suites outperformed manually written ones.

Selective Symbolic Execution

S2E (Selective Symbolic Execution)

S2E (Chipounov, Kuznetsov, and Candea, 2011) combines full-system emulation (QEMU) with selective symbolic execution. The user selects which components to analyze symbolically; everything else runs concretely.

Consistency models control how symbolic and concrete worlds interact:

Strict consistency: Convert symbolic to concrete at boundary (lose coverage).
Relaxed consistency: Inject symbolic values from concrete returns (may explore infeasible paths but finds more bugs).
Overconstrained execution: Track constraints from concretization choices, can backtrack.

S2E can analyze kernel code, drivers, firmware — anything that runs in the VM — without source code or models.

Other Engines

angr

Binary analysis framework combining static and dynamic techniques. Symbolic execution engine (Claripy) operates on VEX IR (lifted from multiple architectures). Supports value-set analysis, CFG recovery, and symbolic execution of stripped binaries. Widely used in CTF competitions and security research.

Manticore

Trail of Bits' symbolic execution tool for binaries and smart contracts (EVM bytecode). Native support for x86/x86-64/ARM/AArch64 binaries. Notable for Ethereum smart contract analysis — explores all execution paths through contracts to find vulnerabilities (reentrancy, integer overflow).

SAGE (Scalable Automated Guided Execution)

Microsoft's whitebox fuzzer for Windows applications. Uses generational search with concolic execution. Targets file parsers and protocol handlers. Found roughly one-third of all security bugs discovered by file fuzzing during Windows 7 development. Runs on x86 binaries without source.

Triton

Dynamic binary analysis framework with symbolic execution capabilities. Built on Pin (Intel's DBI framework) and Z3. Provides fine-grained taint analysis and symbolic execution APIs for binary analysis automation.

Applications

Test Generation

Symbolic execution naturally produces test inputs: solve the path condition to obtain concrete inputs that exercise each explored path. This achieves high structural coverage (branch, path) systematically. Generated tests include the concrete input values and expected outputs.

Limitations: Path explosion limits the achievable coverage. Symbolic execution excels for unit testing and small modules but struggles with whole-application testing.

Vulnerability Finding

Buffer overflows: Symbolically track buffer sizes and access indices. If index ≥ buffer_size is satisfiable, report a potential overflow with a concrete triggering input.

Integer overflows: Track arithmetic operations symbolically. Check if intermediate values can exceed type bounds.

Use-after-free: Track allocation/deallocation symbolically. If a freed pointer is dereferenced on a feasible path, report with concrete input.

Format string vulnerabilities: Track format string arguments symbolically. If user-controlled input reaches a format specifier position, flag it.

Exploit Generation

AEG (Automatic Exploit Generation, Avgerinos et al., 2011): Combine symbolic execution with exploit payload construction. Solve for inputs that not only trigger a vulnerability but also redirect control flow to attacker-controlled code. Demonstrated automatic generation of working exploits for real software.

Equivalence Checking

Symbolically execute two versions of a function and check whether their outputs differ for any input. If the symbolic output expressions are equivalent (modulo an SMT query), the functions are equivalent. Used for translation validation (compiler correctness) and regression testing.

Protocol Analysis

Symbolically execute protocol implementations to explore all message sequences. Discover unexpected state transitions, authentication bypasses, or crashes triggered by malformed messages.

Challenges and Limitations

Environment Modeling

Programs interact with the OS, network, file system, and hardware. Each interaction requires either a symbolic model (expensive to build) or concretization (loses coverage). Library functions (libc, STL) pose the same problem — either model symbolically or execute concretely.

Floating-Point Constraints

SMT solvers have limited support for floating-point arithmetic. Most symbolic execution engines either concretize floating-point operations or use approximate theories. This limits analysis of numerical code.

Constraint Solving Bottleneck

SMT queries generated by symbolic execution can be extremely complex — large formulas with non-linear arithmetic, bit-vector operations, and array accesses. Solver timeouts are common. Caching, simplification, and constraint independence analysis are essential optimizations.

Symbolic Memory

When a memory access index is symbolic (e.g., a[sym_idx]), the executor must consider all possible concrete indices. Strategies:

Fully symbolic memory: Model memory as an SMT array. Precise but creates complex queries.
Address concretization: Pick a concrete index value. Fast but misses many paths.
Partial concretization: Enumerate a bounded set of possible indices. Compromise between precision and performance.