DeepState: Symbolic unit testing for C and C++

Peter Goodman, Alex Groce
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 04 September 2020

NDSS Workshop on Binary Analysis Research
San Diego, California, USA
Pages 7
18 February 2018
Note(s): fuzz testing, symbolic execution, binary analysis, property-based testing, unit tests, verification performance, swarm verification, angr verifier
Papers: holzmann:ieeetse:2011, ramos:sec:2015

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.


Case splitting, Swarm verification, Verification performance of code, Verifier performance