# Symbolic execution

Symbolic execution runs a program with placeholders in place of real
inputs, and tracks the constraints each path puts on them. Those
placeholders are *symbolic* values; an SMT (satisfiability modulo
theories) solver then derives the concrete inputs that drive
execution down each feasible branch. Where the path-condition solver
finds a counterexample to an assertion, the technique reports a
concrete input that triggers the bug. It sits between testing and
formal methods: it runs the actual code (unlike model checking on a
spec) and gives an exhaustive verdict bounded by what the engine can
explore (unlike empirical testing).

This *whitebox* mode, driving the solver down every feasible path, is
one of two ways the technique is used. The other, *concolic
execution*, pairs the solver with a coverage-guided fuzzer, trading the
exhaustive-over-paths guarantee for an empirical one.

## What it catches

- **Reachability bugs.** Any assertion the engine can prove
  reachable by some input becomes a concrete crash with a
  reproducer.
- **Memory-safety violations at exact triggering inputs.** Buffer
  overflows, out-of-bounds reads, integer overflows that lead to
  unsafe pointer arithmetic.
- **Path-coverage gaps.** The engine surfaces feasible paths the
  test suite never exercised, naming the input class that gets
  there.
- **Equivalence and divergence between two programs.** Run both
  symbolically on the same constraints; any divergence is a
  concrete counterexample.

What symbolic execution does **not** catch: paths that exceed the
engine's exploration budget, code that depends on hardware behavior
the engine doesn't model, language features that resist symbolic
modeling (a dynamic language's `eval`, reflection, or host objects,
which force the engine to fall back to concrete values and lose path
coverage), and bugs that require interaction with non-deterministic
external state. The dominant practical limit is *path explosion*: a
loop with $n$ iterations spawns $2^n$ paths in the worst case.

## Tools

### Source-level

- **[KLEE](https://klee-se.org/)** — LLVM-based; used on coreutils, busybox, and
  dozens of libraries.
- **[SymCC](https://github.com/eurecom-s3/symcc)** — compile-time instrumentation; faster than
  interpreter-based engines for some workloads.

**[Bounded model checking](https://quality.stereobooster.com/bounded-model-checking.md)** ([CBMC](https://www.cprover.org/cbmc/) for
C/C++, [JBMC](https://www.cprover.org/jbmc/) for Java) is the close sibling, *not* a
symbolic-execution engine: instead of exploring paths one at a time, it unrolls
the whole program to a fixed depth and discharges a single SMT query.

### Binary / firmware

- **[angr](https://angr.io/)** — Python framework for binary-level security
  research; symbolic execution, control-flow analysis, decompilation.
- **[Manticore](https://github.com/trailofbits/manticore)** — Trail of Bits; binaries and EVM smart contracts.
- **[Triton](https://triton-library.github.io/)** — dynamic binary analysis with concolic execution.
- **[S2E](https://s2e.systems/)** — Symbolic + concrete execution, OS-level.

### Concolic (mixed concrete + symbolic)

The empirical sibling: a coverage-guided fuzzer supplies the concrete
inputs, calls the solver only when it stalls on a branch, and then
resumes.

- **SAGE** (Microsoft, internal) — concolic fuzzing of Windows
  file-format parsers.
- **[QSYM](https://github.com/sslab-gatech/qsym)**, **[Driller](https://github.com/shellphish/driller)**, **[Angora](https://github.com/AngoraFuzzer/Angora)** —
  concolic engines that pair with a coverage-guided fuzzer; SymCC can
  be driven the same way.

### Dynamic languages (JavaScript)

Dynamic languages resist symbolic modeling: dynamic typing, prototype
mutation, and string-heavy logic leave the solver little to reason
about, so JavaScript engines stay research-grade.

- **ExpoSE** (Loring et al. 2017)[^loring2017]: dynamic symbolic execution for Node.js,
  built on Jalangi2 and Z3; notable for modeling regular expressions
  symbolically (capture groups, backreferences, greediness), where much
  of JavaScript's string logic lives.
- **Aratha** (Amadini et al. 2019)[^amadini2019]: dynamic symbolic execution for JavaScript
  that discharges path conditions with constraint programming (MiniZinc
  / G-Strings) rather than an SMT back-end; it does not yet handle
  backreferences or greedy matching.

### SMT solvers (the engine underneath)

- **[Z3](https://github.com/Z3Prover/z3)** (Microsoft Research) — the dominant SMT solver; powers
  KLEE, CBMC, Manticore, [Dafny](https://dafny.org/), F\*.
- **[CVC5](https://cvc5.github.io/)**, **[Yices2](https://yices.csl.sri.com/)**, **[Boolector](https://boolector.github.io/)**, **[MathSAT](https://mathsat.fbk.eu/)** — strong
  alternatives.

The same SMT engines power automated reasoning beyond program analysis.
AWS's Provable Security ships SMT-based reasoning over resource
policies in customer-facing services, including Amazon Macie;
network-reachability analysis in that effort uses datalog constraint
solvers rather than SMT (Cook 2018)[^cook2018].

## When to use, when not

**Use:**

- Library code with high reachability cost: parsers, decoders,
  validators, kernel-syscall handlers. Symbolic execution returns the
  concrete input that reaches a given branch.
- Security research on binaries where source is unavailable — malware
  analysis and capture-the-flag (CTF) work. angr and Manticore are the
  dominant tools.
- Closing the gap between [fuzzing](https://quality.stereobooster.com/fuzzing.md) and exhaustive
  exploration, with a concolic engine (Driller, QSYM).
- Bounded verification of small C/Java functions, though the sibling
  [bounded model checking](https://quality.stereobooster.com/bounded-model-checking.md) is usually the
  better fit there.

**Don't:**

- For whole-application analysis. Path explosion is fatal; the
  technique is most effective on functions and small modules.
- As a substitute for [fuzzing](https://quality.stereobooster.com/fuzzing.md). Fuzzing scales to
  much larger surfaces with no spec; symbolic execution reaches
  paths fuzzing can't but at much higher per-path cost.
- When the required SMT theory is undecidable or too expensive to
  discharge: floating-point, nonlinear arithmetic, unbounded loops.

## Evidence

- **KLEE on coreutils.** Across 452 applications KLEE found 56
  serious bugs; on the 89 GNU coreutils tools it averaged over 90%
  line coverage (beating the maintainers' own hand-written test
  suites) and surfaced defects in heavily-tested code that had
  escaped detection across roughly 15 years of development
  (Cadar et al. 2008)[^cadar2008].
- **SAGE at Microsoft.** Microsoft's concolic (whitebox-fuzzing)
  engine. Introduced in 2008, it found the MS07-017 ANI parsing
  vulnerability with no format-specific knowledge, a bug that
  extensive blackbox fuzzing and static analysis had missed
  (Godefroid et al. 2008)[^godefroid2008]. A later retrospective
  reports SAGE finding a substantial share of the file-fuzzing
  bugs caught during Windows 7 development (Godefroid et al. 2012)[^godefroid2012].

## Related

**Exploring the program's behavior space**

All explore many program behaviors; they differ in what they run and what they
guarantee. [Model checking](https://quality.stereobooster.com/model-checking.md) works on a spec or
model and is exhaustive over it. Symbolic
execution runs the *actual code*, solving
path constraints to reach branches a fuzzer can't, with a bounded-exhaustive
verdict; [bounded model checking](https://quality.stereobooster.com/bounded-model-checking.md) runs
the actual code too, but poses a single SMT query over the whole program unrolled
to a fixed depth rather than exploring paths one at a time.
[Fuzzing](https://quality.stereobooster.com/fuzzing.md) runs the actual code too but samples inputs
empirically: cheaper per case, no exhaustiveness claim.

**Generative testing**

These methods blur together because they all run the code and check the result
without a hand-written expected value. Two roles pull them apart, and a single test
picks one of each.

**Input generators** choose the input, and differ by the steering signal (the
Generative subtree of the [input axis](https://quality.stereobooster.com/input.md)):

- Random: [property-based testing](https://quality.stereobooster.com/property-based-testing.md) samples
  from a generator or schema.
- Coverage feedback: [fuzzing](https://quality.stereobooster.com/fuzzing.md) mutates inputs steered by
  coverage (raw bytes); [automated test generation](https://quality.stereobooster.com/automated-test-generation.md)
  runs the same feedback loop as a fitness-guided search over structured call sequences.
- Solver: symbolic execution derives an input
  that reaches a chosen path.
- Systematic: [combinatorial testing](https://quality.stereobooster.com/combinatorial-testing.md) builds a
  covering array over every t-way combination.

**Oracle suppliers** provide the verdict when no expected value is written:

- [Metamorphic testing](https://quality.stereobooster.com/metamorphic-testing.md) checks a relation between
  the outputs of two related inputs.
- [Differential testing](https://quality.stereobooster.com/differential-testing.md) compares against a
  trusted second implementation.

Pick one generator and one oracle: they compose. A coverage-guided fuzzer that checks a
metamorphic relation is fuzzing and metamorphic at once. (The written-answer end, where
the author picks rows and answers by hand, is [example / parameterized
tests](https://quality.stereobooster.com/example-tests.md).)

## Classification

- **Quality dimensions:** Functionality, Security.
- **Area:** OS and library testing, binary and firmware analysis, security research, vulnerability discovery, exploit synthesis.
- **Guarantee:** Exhaustive, Empirical (concolic).

## Referenced by

- [Abstract interpretation](https://quality.stereobooster.com/abstract-interpretation.md) · Methods
- [Bounded model checking](https://quality.stereobooster.com/bounded-model-checking.md) · Methods
- [Dead-code detection](https://quality.stereobooster.com/dead-code-detection.md) · Methods
- [Equivalence checking](https://quality.stereobooster.com/equivalence-checking.md) · Methods
- [Formal methods](https://quality.stereobooster.com/formal.md) · Methods
- [Verifying memory safety](https://quality.stereobooster.com/memory.md) · Methods
- [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI
- [Conventional terminology](https://quality.stereobooster.com/terminology.md) · Conventional

## References

[^loring2017]: Loring, Blake, Duncan Mitchell, and Johannes Kinder. 2017. "[ExpoSE: Practical Symbolic Execution of Standalone JavaScript](https://www.cs.rhul.ac.uk/home/uaac003/papers/spin17-expose.pdf)." *Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software (SPIN 2017)*, 196–99. <https://doi.org/10.1145/3092282.3092295>.
[^amadini2019]: Amadini, Roberto, Mak Andrlon, Graeme Gange, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2019. "[Constraint Programming for Dynamic Symbolic Execution of JavaScript](https://minerva-access.unimelb.edu.au/server/api/core/bitstreams/b999c802-90f6-5ce4-8b79-c298bfc62afa/content)." *Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR 2019)*, Lecture notes in computer science, vol. 11494: 1–19. [https://doi.org/10.1007/978-3-030-19212-9\\\_1](https://doi.org/10.1007/978-3-030-19212-9\_1).
[^cook2018]: Cook, Byron. 2018. "[Formal Reasoning About the Security of Amazon Web Services](https://link.springer.com/content/pdf/10.1007%2F978-3-319-96145-3_3.pdf)." *Computer Aided Verification (CAV 2018)*, 38–47. [https://doi.org/10.1007/978-3-319-96145-3\\\_3](https://doi.org/10.1007/978-3-319-96145-3\_3).
[^cadar2008]: Cadar, Cristian, Daniel Dunbar, and Dawson Engler. 2008. "[KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs](https://www.usenix.org/legacy/event/osdi08/tech/full_papers/cadar/cadar.pdf)." *Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI '08)* (Berkeley, CA), 209–24. [https://www.usenix.org/legacy/event/osdi08/tech/full\\\_papers/cadar/cadar.pdf](https://www.usenix.org/legacy/event/osdi08/tech/full\_papers/cadar/cadar.pdf).
[^godefroid2008]: Godefroid, Patrice, Michael Y. Levin, and David Molnar. 2008. "[Automated Whitebox Fuzz Testing](https://www.ndss-symposium.org/wp-content/uploads/2017/09/Automated-Whitebox-Fuzz-Testing-paper-Patrice-Godefroid.pdf)." *Proceedings of the Network and Distributed System Security Symposium (NDSS '08)*. <https://www.ndss-symposium.org/wp-content/uploads/2017/09/Automated-Whitebox-Fuzz-Testing-paper-Patrice-Godefroid.pdf>.
[^godefroid2012]: Godefroid, Patrice, Michael Y. Levin, and David Molnar. 2012. "[SAGE: Whitebox Fuzzing for Security Testing](https://patricegodefroid.github.io/public_psfiles/cacm2012.pdf)." *Communications of the ACM* 55 (3): 40–44. <https://doi.org/10.1145/2093548.2093564>.

## Acronyms

- CTF — capture the flag
- EVM — Ethereum Virtual Machine
- SMT — satisfiability modulo theories