Terminology update: There are multiple, consistent but conflicting uses of the term “symbolic execution” and “symbolic evaluation”. These terms are used by different groups of people in different ways so, if you use these terms without qualification, you are likely to cause misunderstandings. Much better to use precise terms like DSE, concolic execution, bounded model checking, etc. which seem to have much more agreement about what they mean.
Old attempt to find a consistently used terminology follows – use at your peril.
Following the terminology in section 3.1 of bornholt:oopsla:2018, symbolic execution is a form of symbolic evaluation where a single path is followed at a time.
Following a single path has the advantage that states do not need to be merged at join points and so many calculations involve concrete values and so can be evaluated directly and efficiently. The price paid for this advantage is that there can be an exponential number of paths.
See also bounded model checking and symbolic evaluation. and see kuznetsov:pldi:2012 for a unifying framework that describes the symbolic evaluation design space/spectrum in terms of how loop/recursion are handled, whether/how branches are tested for feasibility, whether/how states from different paths are merged and compositionality.
Types of symbolic execution include
(Pure) symbolic execution enumerates paths, collects path conditions along those paths and then checks which path conditions are satisfiable. (Checking path conditions can be done eagerly to prune infeasible paths early.)
I think this is mostly used in separation logic checkers such as the Smallfoot verifier and the VeriFast verifier.
Dynamic Symbolic Execution (DSE) mixes concrete and symbolic execution benefiting from the efficiency and decidability of concrete execution and the need to use concrete values when interacting with the program environment (libraries, OS, etc.) and from the stronger guarantees of symbolic execution.
“Offline” DSE (aka “concolic execution”) relies on concrete execution to drive symbolic execution using an instrumented interpreter/ simulator/… to build symbolic representations while executing with concrete values.
Used in the DART verifier.
“Online” DSE (aka “Execution Generated Testing” (EGT)) mixes concrete and symbolic execution by using concrete execution whenever the inputs to an operation are concrete and using symbolic execution if any inputs are symbolic.
Used in the KLEE verifier.
Static Symbolic Execution (SSE) avoids path explosion by generating a symbolic formula representing all paths through a piece of code. It does this by merging formulae at join points in a pre-execution pass.
This approach has significant overlap with bounded model checking and the term is mostly used in the context of hybrid approaches such as avgerinos:icse:2014.
Selective Symbolic Execution (SSE) interleaves concrete and symbolic execution with a focus on performing symbolic execution as much of the code you care about as possible.
(I think this may be a special case of DSE?)
Forward symbolic execution constructs paths in normal program order. [I have seen references to backward symbolic execution but I don’t think I have seen backward symbolic execution being used for software verification.]
[todo: it is probably less useful to have a tree-shaped taxonomy of this topic than to have a list of design choices that define an N-dimensional taxonomy where most dimensions include “yes”, “no” and “hybrid” on their axis. This would better capture how thoroughly the symbolic execution design space has been explored.]
In part because of the exponential path explosion of pure symbolic execution, it is rarely feasible to check all paths so there has been a lot of work on scheduling algorithms that try to maximize coverage, to cover some part of the code (e.g., code that is part of a recent commit), to execute enough iterations to overflow a buffer (avgerinos:cacm:2014), etc. These scheduling algorithms make [state merging] harder (but see kuznetsov:pldi:2012), make ranged analysis harder (siddiqui:oopsla:2012), and probably other impacts too.
(Note that even if you could explore all paths, you still can’t guarantee to find all bugs because things like external calls and syscalls require concretization and therefore lose completeness.)
Notes related to Symbolic execution
angr verifier, Bounded model-checking, Case splitting, CIVL verifier, Concolic execution, CUTE verifier, DART verifier, Driller verifier, EXE symbolic executor, Fuzz testing, Hybrid testing, KLEE verifier, Mayhem, S2E verifier, SAGE verifier, Search based test generation, Separation logic, State merging, Symbolic evaluation, Symbolic execution, Symbolic memory, SymCC, Test generation, Verification performance of code, Verification profiling of code, Verifier performance
Papers related to Symbolic execution
- Isla: Integrating full-scale ISA semantics and axiomatic concurrency models [armstrong:cav:2021]
- Automatic exploit generation [avgerinos:cacm:2014]
- Enhancing symbolic execution with veritesting [avgerinos:icse:2014]
- A survey of symbolic execution techniques [baldoni:compsurv:2018]
- Deconstructing dynamic symbolic execution [ball:dsse:2015]
- Symbolic execution with separation logic [berdine:aplas:2005]
- Smallfoot: Modular automatic assertion checking with separation logic [berdine:fmco:2005]
- Symbolic execution of multithreaded programs from arbitrary program contexts [bergan:oopsla:2014]
- Countermeasures optimization in multiple fault-injection context [boespflug:fdtc:2020]
- Finding code that explodes under symbolic evaluation [bornholt:oopsla:2018]
- SUSHI: A test generator for programs with complex structured inputs [braione:icse:2018]
- Sys: A static/symbolic tool for finding good bugs in good (browser) code [brown:sec:2020]
- A static analyzer for finding dynamic programming errors [bush:spe:2000]
- Running symbolic execution forever [busse:issta:2020]
- Symbolic execution for software testing: Three decades later [cadar:cacm:2013]
- Targeted program transformations for symbolic execution [cadar:fse:2015]
- KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs [cadar:osdi:2008]
- Unleashing Mayhem on binary code [cha:sandp:2012]
- Symbiotic 8: Beyond symbolic execution [chalupa:tacas:2021]
- SAVIOR: Towards bug-driven hybrid testing [chen:sp:2020]
- S2E: A platform for in-vivo multi-path analysis of software systems [chipounov:asplos:2011]
- Selective symbolic execution [chipounov:hotdep:2009]
- The S2E platform: Design, implementation, and applications [chipounov:tcs:2012]
- Rethinking pointer reasoning in symbolic execution [coppa:ase:2017]
- Verifying systems rules using rule-directed symbolic execution [cui:asplos:2013]
- Binsec/Rel: Efficient relational symbolic execution for constant-time at binary-level [daniel:sandp:2020]
- Specification of concretization and symbolization policies in symbolic execution [david:issta:2016]
- Study of integrating random and symbolic testing for object-oriented software [dimjasevic:ifm:2018]
- A local shape analysis based on separation logic [distefano:tacas:2006]
- Evaluating manual intervention to address the challenges of bug finding with KLEE [galea:arxiv:2018]
- Feedback-directed unit test generation for C/C++ using concolic execution [garg:icse:2013]
- SAGE: Whitebox fuzzing for security testing [godefroid:acmq:2012]
- The soundness of bugs is what matters (position statement) [godefroid:bugs:2005]
- Fuzzing: Hack, art, and science [godefroid:cacm:2020]
- DART: Directed automated random testing [godefroid:pldi:2005]
- DeepState: Symbolic unit testing for C and C++ [goodman:ndss:2018]
- Spectector: Principled detection of speculative information flows [guarnieri:sandp:2020]
- TracerX: Dynamic symbolic execution with interpolation [jaffar:arxiv:2020]
- Software model checking [jhala:compsurv:2009]
- A segmented memory model for symbolic execution [kapus:fse:2019]
- Generalized symbolic execution for model checking and testing [khurshid:tacas:2003]
- On symbolic execution of decompiled programs [korencik:qrs:2020]
- Efficient state merging in symbolic execution [kuznetsov:pldi:2012]
- No panic! Verification of Rust programs by symbolic execution [lindner:indin:2018]
- Verification of safety functions implemented in Rust: A symbolic execution based approach [lindner:indin:2019]
- Hybrid concolic testing [majumdar:icse:2007]
- The art, science, and engineering of fuzzing: A survey [manes:ieeetse:2019]
- Formal specification and testing of QUIC [mcmillan:sigcomm:2019]
- Symbolic execution with existential second-order constraints [mechtaev:fse:2018]
- Noninterference via symbolic execution [milushev:forte:2012]
- Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
- Design of a symbolically executable embedded hypervisor [nordholz:eurosys:2020]
- Deferred concretization in symbolic execution via fuzzing [pandey:issta:2019]
- Differential symbolic execution [person:fse:2008]
- Systematic comparison of symbolic execution systems: Intermediate representation and its generation [poeplau:acsac:2019]
- Symbolic execution with SymCC: Don't interpret, compile! [poeplau:usenix:2020]
- A synergistic approach for distributed symbolic execution using test ranges [qiu:icse:2017]
- Using test ranges to improve symbolic execution [qiu:nfm:2018]
- Practical, low-effort equivalence verification of real code [ramos:cav:2011]
- Under-constrained symbolic execution: Correctness checking for real code [ramos:sec:2015]
- Interoperability-guided testing of QUIC implementations using symbolic execution [rath:epiq:2018]
- Towards making formal methods normal: meeting developers where they are [reid:hatra:2020]
- Methods for binary symbolic execution [romano:phd:2014]
- Bug synthesis: Challenging bug-finding tools with deep faults [roy:fse:2018]
- Zero-overhead path prediction with progressive symbolic execution [rutledge:icse:2019]
- PG-KLEE: Trading soundness for coverage [rutledge:icse:2020]
- All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask) [schwartz:sp:2010]
- CUTE: A concolic unit testing engine for C [sen:fse:2005]
- Scaling symbolic execution using ranged analysis [siddiqui:oopsla:2012]
- Driller: Augmenting fuzzing through selective symbolic execution [stephens:ndss:2016]
- Parameterized unit tests [tillmann:fse:2005]
- A lightweight symbolic virtual machine for solver-aided host languages [torlak:pldi:2014]
- Chopped symbolic execution [trabish:icse:2018]
- Relocatable addressing model for symbolic execution [trabish:issta:2020]
- Symbolic memory with pointers [trtik:atva:2014]
- COASTAL: Combining concolic and fuzzing for Java (competition contribution) [visser:tacas:2020]
- Memoized symbolic execution [yang:issta:2012]
- QSYM: A practical concolic execution engine tailored for hybrid fuzzing [yun:usenix:2018]
- Verifying software network functions with no verification expertise [zaostrovnykh:sosp:2019]
- Boost symbolic execution using dynamic state merging and forking [zhang:apsec:2018]