Skip to content

Software Quality

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 nn iterations spawns 2n2^n paths in the worst case.

Tools

Source-level

  • KLEE — LLVM-based; used on coreutils, busybox, and dozens of libraries.
  • SymCC — compile-time instrumentation; faster than interpreter-based engines for some workloads.

Bounded model checking (CBMC for C/C++, 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 — Python framework for binary-level security research; symbolic execution, control-flow analysis, decompilation.
  • Manticore — Trail of Bits; binaries and EVM smart contracts.
  • Triton — dynamic binary analysis with concolic execution.
  • S2E — 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, Driller, 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)1: 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)2: 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)

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)3.

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 and exhaustive exploration, with a concolic engine (Driller, QSYM).
  • Bounded verification of small C/Java functions, though the sibling bounded model checking 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. 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)4.
  • 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)5. A later retrospective reports SAGE finding a substantial share of the file-fuzzing bugs caught during Windows 7 development (Godefroid et al. 2012)6.

Exploring the program's behavior space

All explore many program behaviors; they differ in what they run and what they guarantee. Model checking 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 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 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):

  • Random: property-based testing samples from a generator or schema.
  • Coverage feedback: fuzzing mutates inputs steered by coverage (raw bytes); automated test generation 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 builds a covering array over every t-way combination.

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

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.)

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

References

  1. Loring, Blake, Duncan Mitchell, and Johannes Kinder. 2017. "ExpoSE: Practical Symbolic Execution of Standalone JavaScript." 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. ↩

  2. Amadini, Roberto, Mak Andrlon, Graeme Gange, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2019. "Constraint Programming for Dynamic Symbolic Execution of JavaScript." 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. ↩

  3. Cook, Byron. 2018. "Formal Reasoning About the Security of Amazon Web Services." Computer Aided Verification (CAV 2018), 38–47. https://doi.org/10.1007/978-3-319-96145-3_3. ↩

  4. Cadar, Cristian, Daniel Dunbar, and Dawson Engler. 2008. "KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs." 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. ↩

  5. Godefroid, Patrice, Michael Y. Levin, and David Molnar. 2008. "Automated Whitebox Fuzz Testing." 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. ↩

  6. Godefroid, Patrice, Michael Y. Levin, and David Molnar. 2012. "SAGE: Whitebox Fuzzing for Security Testing." Communications of the ACM 55 (3): 40–44. https://doi.org/10.1145/2093548.2093564. ↩