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. 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. Buffer overflows, out-of-bounds reads, and integer overflows feeding unsafe pointer arithmetic come back with the exact input that triggers them.
  • 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. The engine runs both on the same constraints, and 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, bugs that require interaction with non-deterministic external state, and language features that resist symbolic modeling — a dynamic language's eval, reflection, or host objects force the engine to fall back to concrete values and lose path coverage. 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 rather than an interpreter.

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 poses a single query to a SAT or SMT solver.

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)

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

  • 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; it models 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 run on the binary itself.
  • 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 constraints the solver must discharge are undecidable or too expensive: 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 for over 15 years of development (Cadar et al. 2008)4.
  • SAGE at Microsoft. Microsoft's internal concolic engine found the MS07-017 ANI parsing vulnerability with no format-specific knowledge, a bug that extensive black-box fuzzing and static analysis had missed (Godefroid et al. 2008)5. SAGE went on to find roughly one-third of the bugs discovered by file fuzzing during the development of Windows 7 (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. ↩