Automatic Testing of Symbolic Execution Engines via Program Generation and Differential Testing

Symbolic execution has attracted significant attention in recent years, with applications in software testing, security, networking and more. Symbolic execution tools, like CREST, KLEE, FuzzBALL, and Symbolic PathFinder, have enabled researchers and practitioners to experiment with new ideas, scale the technique to larger applications and apply it to new application domains. Therefore, the correctness of these tools is of critical importance.

In this paper, we present our experience extending compiler testing techniques to find errors in both the concrete and symbolic execution components of symbolic execution engines. The approach used relies on a novel way to create program versions, in three different testing modes — concrete, single-path and multi-path — each exercising different features of symbolic execution engines. When combined with existing program generation techniques and appropriate oracles, this approach enables differential testing within a single symbolic execution engine.

We have applied our approach to the KLEE, CREST and FuzzBALL symbolic execution engines, where it has discovered 20 different bugs exposing a variety of important errors having to do with the handling of structures, division, modulo, casting, vector instructions and more, as well as issues related to constraint solving, compiler optimisations and test input replay.

Please click here for more details about this work.

Timotej Kapus is a Doctoral Student in the Software Reliability Group at Imperial College London, where he also received his MEng undergraduate degree. He started in the group in the summer 2015 as an UROP student and then expanded his work into an MEng thesis. His research interests include software analysis and testing, more specifically he is currently focusing on symbolic execution.