PaperlayerView exact revision on arXiv

Source-linked AI summary

A Survey of Symbolic Execution Techniques

Roberto Baldoni, Emilio Coppa, Daniele Cono D'Elia, Camil Demetrescu, Irene Finocchi

arXiv:1610.00502v3cs.SEcs.PL

TL;DR

Software analysis needs to determine whether program properties can fail across possible inputs, but concrete testing explores only selected executions. This survey synthesizes symbolic execution techniques that represent inputs symbolically and explore program paths, covering their applications, optimizations, and challenges. The survey reports major practical advances, including tools finding nearly 30% of bugs discovered by file fuzzing during Windows 7 development.

  • Problem

    Testing selected concrete inputs may miss behaviors on other paths, motivating systematic analysis of possible executions.

  • Method

    The survey explains symbolic execution and its prominent techniques, focusing on forward exploration from a program's entry point and associated optimizations.

  • Results

    Nearly 30% of bugs discovered by file fuzzing during Windows 7 development were revealed by symbolic execution tools that other analyses and black-box testing missed.

  • Takeaways & Limitations

    Symbolic execution has supported practical advances in software testing, security, and code analysis, including automated vulnerability detection and fixing.

  • Takeaways & Limitations

    Computing loop invariants remains difficult and often requires manual intervention from domain experts.

Abstract

from arXiv · show

Many security and software testing applications require checking whether certain properties of a program hold for any possible usage scenario. For instance, a tool for identifying software vulnerabilities may need to rule out the existence of any backdoor to bypass a program's authentication. One approach would be to test the program using different, possibly random inputs. As the backdoor may only be hit for very specific program workloads, automated exploration of the space of possible inputs is of the essence. Symbolic execution provides an elegant solution to the problem, by systematically exploring many possible execution paths at the same time without necessarily requiring concrete inputs. Rather than taking on fully specified input values, the technique abstractly represents them as symbols, resorting to constraint solvers to construct actual instances that would cause property violations. Symbolic execution has been incubated in dozens of tools developed over the last four decades, leading to major practical breakthroughs in a number of prominent software reliability applications. The goal of this survey is to provide an overview of the main ideas, challenges, and solutions developed in the area, distilling them for a broad audience. The present survey has been accepted for publication at ACM Computing Surveys. If you are considering citing this survey, we would appreciate if you could use the following BibTeX entry: http://goo.gl/Hf5Fvc

1 INTRODUCTION

Symbolic execution analyzes whether program properties can be violated by representing uncertain inputs symbolically and exploring multiple paths. This survey introduces its foundations, practical applications, and central challenges, including path explosion, complex state, environments, and constraint solving.

  • Symbolic execution tests whether program properties such as memory safety or authentication can be violated.It supports security and mission-critical applications, although some properties require heuristics or approximate analyses.
  • Unlike concrete execution, symbolic execution can explore multiple input-dependent paths simultaneously and support stronger guarantees.Concrete execution follows one path for one input, while symbolic execution reasons about classes of inputs.
  • Symbolic execution has produced practical breakthroughs, including nearly 30% of bugs found by file fuzzing during Windows 7 development.The tools ran continuously in Microsoft application testing and found bugs missed by other analyses and black-box testing.
  • The symbolic engine represents unknown values with symbols and maintains a symbolic store plus path constraints while executing program statements.Branches fork execution states with different path constraints, and constraint solving can produce concrete inputs that violate an assertion.
  • Exhaustive symbolic execution is theoretically sound and complete for decidable analyses but is unlikely to scale beyond small applications.Practical systems may trade soundness for performance or explore only part of the state space within a time budget.
  • Real-world symbolic execution must address memory objects, software-environment interactions, path explosion, and difficult constraint classes.Loops can increase execution states exponentially, while non-linear arithmetic can impede solver efficiency.

2 SYMBOLIC EXECUTION ENGINES

Symbolic executors mix symbolic and concrete execution to make path exploration feasible despite external code, difficult constraints, and resource limits. The section contrasts dynamic and selective approaches, while highlighting false negatives, path divergences, and search prioritization as practical concerns.

  • 2.2 Path Selection: Because enumerating all paths is prohibitively expensive, symbolic engines prioritize exploration using heuristics tailored to goals such as code coverage or overflow detection.Search strategies select promising paths first rather than attempting exhaustive exploration.
  • 2.1 Mixing Symbolic and Concrete Execution: Concolic execution mixes concrete and symbolic execution to address infeasible-to-solve constraints and untraceable external code.This combination is intended to make symbolic execution feasible in practical, non-self-contained programs.
  • 2.1 Mixing Symbolic and Concrete Execution: Dynamic symbolic execution follows a concrete run while maintaining symbolic stores and path constraints, then negates selected branches to generate new inputs.The engine updates concrete and symbolic state together and uses a solver to satisfy negated path constraints.
  • 2.1 Mixing Symbolic and Concrete Execution: Concolic execution can explore paths in a function even when called external code is not symbolically tracked.Concrete values from the external call guide execution, while symbolic constraints in the tracked function support exploration of an alternative path.
  • 2.1 Mixing Symbolic and Concrete Execution: Untracked relationships and side effects can cause false negatives or path divergences, including missed paths and generated inputs that follow a different execution path.Dynamic symbolic execution therefore trades soundness for performance and implementation effort; one cited report observes path-divergence rates over 60%.
  • 2.1 Mixing Symbolic and Concrete Execution: Selective symbolic execution interleaves concrete and symbolic execution while fully exploring only selected software components.The approach keeps the overall exploration meaningful without requiring every component of the software stack to be symbolically analyzed.
  • 2.3 Symbolic Backward Execution: Symbolic backward execution starts at a target point and proceeds toward the program entry point to identify inputs that trigger specific code.It collects path constraints during reverse traversal and discards infeasible paths when constraint solving proves them unsatisfiable.

3 MEMORY MODEL

Symbolic memory must represent both symbolic data and symbolic addresses, balancing accurate memory behavior against state-space and solver scalability. The survey describes fully symbolic memory, state forking, if-then-else formulas, concretization, and hybrid or heap-focused alternatives.

  • Memory representation: Memory modeling maps variables and memory addresses to symbolic expressions or concrete values, enabling symbolic execution of pointers and arrays.The memory store explicitly represents addresses rather than only scalar variables.
  • State forking: State forking handles symbolic reads and writes by creating states for all possible referenced addresses and adding corresponding assumptions to their path constraints.In the example, a[i]=5 produces two states for a[0] and a[1], while a[j] subsequently branches each outcome again.
  • If-then-else formulas: If-then-else formulas encode uncertainty in the symbolic store without creating new states, using ite conditions to represent alternative reads and writes.Each memory operation introduces ite expressions for the possible values of the symbolic address.
  • Fully symbolic memory: Fully symbolic memory provides the most accurate account of possible memory manipulations but can cause an intractable explosion in states when symbolic addresses range broadly.Small bounded address sets can remain tractable, whereas unrestricted addresses may reference any memory cell.
  • Concretization and hybrid models: Address concretization reduces states and solver-formula complexity by choosing one concrete address, but it may miss paths depending on other pointer values.Hybrid partial memory models, such as Mayhem’s, retain symbolic reads for sufficiently small intervals while concretizing written addresses.

4 INTERACTION WITH THE ENVIRONMENT

Symbolic execution must model interactions with operating systems, libraries, frameworks, and managed runtimes, whose side effects and callbacks cross analysis boundaries. The survey presents concrete execution, abstract models, automatic model generation, virtualization, and selective exploration as alternative responses.

  • Environment interactions: Real-world programs interact with system and application environments through files, networks, variables, callbacks, and other software-stack components.Frameworks such as Swing and Android can invoke application code through user interaction.
  • Concrete external calls: Concrete execution of external calls can limit explored behaviors and, in online execution, allow distinct paths to interfere through shared side effects.This approach may be practical when fully symbolic modeling is infeasible, but it can produce incomplete exploration.
  • Abstract models: Abstract environment models capture interactions symbolically, such as KLEE’s per-state symbolic file systems that fork for each possible file and an optional error branch.Other systems model broader environments, including file systems, network sockets, environment variables, and library or system calls.
  • Virtualized execution: S2E uses virtualization to let programs interact with the real environment while preventing side effects from propagating across independent execution paths.Selective symbolic execution limits exploration across the software stack to mitigate the cost of emulating a full stack.
  • Modeling limitations: Manually written component models are difficult to construct, may be unavailable for closed-source components, and can leave applications using unsupported models out of reach.Model accuracy and maintenance are also concerns when the surrounding system changes.
  • Automatic modeling: Automatic model-generation techniques use program slicing to extract code manipulating fields relevant to the symbolic analysis.This line of work targets components for which manual modeling is impractical.

5 PATH EXPLOSION

Path explosion is a central scalability challenge because branching, loops, and function calls can generate exponentially or infinitely many states. The survey presents pruning, summarization, compaction, and interpolation techniques to reduce redundant exploration while preserving useful guarantees.

  • Challenge: Path explosion can make the number of symbolic-execution states exponential in the number of branches, increasing both runtime and memory requirements.Loops and function calls are major sources of this growth; symbolic loop conditions can even generate potentially infinite branches.
  • Pruning: Solver checks can safely prune branches whose path constraints are unsatisfiable, because no concrete input can reach them.This eager evaluation strategy is commonly the default in symbolic engines.
  • Summarization: Summaries for functions and loops let symbolic executors reuse prior results and avoid repeatedly exploring the same code.Loop summaries can generalize across program states, while function summaries capture invocation effects for reuse.
  • Summarization: Early loop-summarization methods are limited to simple updates and do not handle nested or multi-path loops, motivating more general frameworks such as Proteus.These limitations constrain which loop structures can be summarized directly.
  • Abstraction and subsumption: Compaction reduces explored states with symbolic execution-tree templates, but the resulting quantified constraints can substantially burden the solver.Interpolation offers another way to avoid similar paths; its overhead may initially slow exploration before benefits emerge.

6 CONSTRAINT SOLVING

Constraint solving determines path feasibility, generates symbolic inputs, and checks assertions, but remains a major scalability obstacle. The survey reviews solver capabilities and optimizations that simplify, defer, cache, or otherwise reduce constraint queries.

  • Role and capabilities: Constraint solvers decide logical formulas used to analyze, test, and verify software, including SAT and richer SMT theories.SMT extends SAT with theories such as linear arithmetic and arrays.
  • Role and capabilities: SMT solvers combine generic algorithms, incremental solving, backtracking, inconsistency explanations, and multiple theories, including arrays and arithmetic.Z3 additionally supports quantifiers, uninterpreted functions, nonlinear arithmetic, and strings through Z3-str.
  • Scalability: Constraint solving remains a principal scalability barrier, especially for expensive theories such as nonlinear arithmetic and opaque library calls.The survey groups responses into constraint reduction, solver unburdening, and extensions for problematic constraints.
  • Optimization: Constraint reduction simplifies solver queries through rewriting, independence analysis, propagation of newly specific values, and bitfield-theory simplification.These methods include compiler-style simplifications and removal of irrelevant independent constraints.
  • Optimization: Caching reuses prior solutions and satisfiability results to reduce repeated solver calls within and across symbolic-execution runs.Examples include EXE query caching, KLEE counterexample caching, memoized executions, and Green’s cross-run reuse.

7 FURTHER DIRECTIONS

The survey identifies opportunities to combine symbolic execution with separation logic, invariant inference, abstract interpretation, termination analysis, function summaries, and program synthesis. These directions target memory reasoning, loop handling, scalability, and compact models of external behavior.

  • Separation logic: Separation logic could let symbolic executors reason inductively about pointer-manipulating code and structures such as lists and trees.Its symbolic-heap semantics support heap reasoning, entailment, framing, and abstraction for termination.
  • Invariants and loops: Symbolic executors could use loop invariants to compactly capture loop effects, but automatically computing suitable invariants remains difficult.The survey notes that existing symbolic executors were not known to exploit this approach and that manual invariant provision is hard.
  • Invariants and loops: Abstract interpretation, predicate abstraction, termination analysis, and loop transformers offer potential ways to summarize or conservatively reason about loops.These approaches can infer invariants, construct ranking functions, or produce loop-free summaries for model checking.
  • Function summaries: Function-summary techniques from static analysis and model checking could provide reusable, compact representations of function effects, though bounded loop unrolling may sacrifice soundness.Interpolation-based summaries can over-approximate executions and be refined across verification runs.
  • Program synthesis: Program synthesis could produce concise models of standard libraries that abstract external behavior and make path-space exploration more scalable.The proposed direction applies synthesis to modules whose implementation entanglements complicate symbolic exploration.

8 CONCLUSIONS

Symbolic execution has evolved into a practical technique across software testing, security, and code analysis. The survey distills its design principles, challenges, and optimization techniques for a broad audience.

  • Applications: Symbolic execution supports applications including test generation, regression testing, exploit generation, authentication-bypass analysis, deobfuscation, and dynamic software updating.The survey links this evolution to major practical breakthroughs and security automation efforts such as the DARPA Cyber Grand Challenge.
  • Survey contribution: The survey presents basic symbolic-executor design principles and key optimization techniques while explaining the field’s main challenges to non-experts.Its stated aim is to support further work and new ideas.

ELECTRONIC APPENDIX

The electronic appendix supplements the manuscript with selected applications of symbolic execution, binary-program analysis challenges, and a list of popular symbolic engines.

  • The appendix covers prominent symbolic execution applications, challenges in analyzing binary programs, and popular symbolic engines.
Loading 1610.00502v3…