Increasing the performance of symbolic execution by compiling symbolic handling into binaries

Symbolic execution has the potential to make software more secure by significantly improving automated vulnerability search. Its principled reasoning can automatically explore parts of the program under test that would otherwise be hard to reach. However, many current implementations face challenges in scalability and usability: The power of symbolic execution comes at a cost, and the community is exploring different approaches to make symbolic executors both efficient and easy to use. In this thesis, we propose a general technique that allows for more efficient implementations of the execution component in symbolic executors. We first examine the state of the art and analyze the strengths and weaknesses of current systems. From the results of this comparison, we derive the idea of accelerating execution by embedding symbolic handling into compiled programs instead of symbolically interpreting a higher-level representation of the program under test. Using this approach, we develop a compiler-based symbolic executor and show that it indeed achieves high execution speed in comparison with state-of-the-art systems. Since the compiler is limited to scenarios

where source code of the program under test is available, we then design and implement a complementary solution for symbolic execution of binaries; it uses the same basic idea of embedding symbolic execution into fast machine code but combines the approach with binary translation to handle the challenges of binary-only analysis.

Both systems, the compiler-based symbolic executor as well as the binary translator, put a strong focus on ease of use with the goal of emphasizing that symbolic execution can benefit software developers and analysts in various fields. We conclude by discussing research directions that could lead to even more practical systems and ultimately enable the use of symbolic execution in mainstream software testing.