A technique for testing symbolic execution engines based on program generation and differential testing of compilers, together with a case study on CREST, KLEE and FuzzBall.
Overview
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 work, we adapt 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.
Artifact
Please go to this page for the artifact.
Research Support
This research project is generously sponsored by the UK EPSRC through an Early-Career Fellowship.
Publications
-
Automatic Testing of Symbolic Execution Engines via Program Generation and Differential Testing
IEEE/ACM International Conference on Automated Software Engineering (ASE 2017)
Talks
-
A Segmented Memory Model for Symbolic Execution
Talk @ ASE 2017