CyberGlossary

Application Security

Symbolic Execution

Also known as: Symbolic analysis, Concolic execution

Definition

A program analysis technique that executes code with symbolic inputs rather than concrete values, building path constraints solved by an SMT solver to find bugs.

A symbolic execution engine treats program inputs as mathematical variables and explores execution paths by branching on conditional statements. Each path accumulates constraints expressed in first-order logic; an SMT solver such as Z3 then determines whether the constraints are satisfiable and, if so, produces a concrete input that drives the program down that path. This makes symbolic execution powerful for proving the reachability of bug conditions (overflow, divide-by-zero, taint reaching a sink), but it suffers from path explosion and constraint complexity. Tools like KLEE, angr and Manticore are used to assist fuzzers, find deep vulnerabilities and verify safety properties of binaries.

Examples

  • Using KLEE on a C library to generate inputs that hit each branch and trigger asserts.
  • Combining angr with AFL++ to solve constraints fuzzing alone cannot.

Related terms