Symbolic execution by compiling symbolic handling into binaries with SymCC and SymQEMU

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. In this talk, we present the benefits of 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 (SymCC) 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 (SymQEMU); 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.