DeepState seeks to narrow the gap between techniques that programmers are familiar with (e.g., testing) and symbolic execution / binary analysis tools by enabling the use of parameterized unit tests with a variety of symbolic execution backends (angr, Manticore and Dr. Fuzz) and fuzzers and making it easy to switch between backends.
The interface is a DSL that extends GoogleTest.
A key challenge is handling “debug printfs” in the code being tested since that causes a path explosion. Their solution is to provide a streaming log interface that defers printing log output until the end of the test.
They enable “swarm testing” in their DSL by providing constructs like “OneOf” that select one of several code blocks to execute. Each member of the swarm can disable some subset of the code blocks or change their relative probability to increase the diversity of testing. (I have seen a similar approach in hardware model checking before.)
They tackle problems around symbolic loop bounds and symbolic array accesses by forking particular concrete values to reduce the state (path?) explosion problem. They call this “pumping”. (I want to know more about this.) (See also ramos:sec:2015 for more on useful macros/operations in a DSE tools.)
The code is available on github under an open-source license; and there are blog articles about DeepState.
Notes related to DeepState: Symbolic unit testing for C and C++
Case splitting, Swarm verification, Verification performance of code, Verifier performance
Papers related to DeepState: Symbolic unit testing for C and C++
- Swarm verification techniques [holzmann:ieeetse:2011]
- Under-constrained symbolic execution: Correctness checking for real code [ramos:sec:2015]