Testing concolic execution through consistency checks

Symbolic execution is a well-known software testing technique that evaluates how a program runs when considering a symbolic input, i.e., an input that can initially assume any concrete value admissible for its data type. The dynamic twist of this technique is dubbed concolic execution and has been demonstrated to be a practical technique for testing even complex real-world programs. Unfortunately, developing concolic engines is hard. Indeed, an engine has to correctly instrument the program to build accurate symbolic expressions, which represent the program computation. Furthermore, to reason over such expressions, it has to interact with an SMT solver. Hence, several implementation bugs may emerge within the different layers of an engine. In this article, we consider the problem of testing concolic engines. In particular, we propose several testing strategies whose main intuition is to exploit the concrete state kept by the executor to identify inconsistencies within the symbolic state. We integrated our strategies into three state-of-the-art concolic executors (SymCC, SymQEMU, and Fuzzolic, respectively) and then performed several experiments to show that our ideas can find bugs in these frameworks. Overall, our approach was able to discover more than 12 bugs across these engines.