Combining static analysis and targeted symbolic execution for scalable bug-finding in application binaries
Riyad Parvez, Paul A. S. Ward, Vijay S Ganesh · Computer Science and Software Engineering · 2016
Symbolic execution is an automated technique for program analysis that has recently become practical due to advances in constraint solvers. Symbolic execution eventually enumerates all feasible program executions, check assertions on all values of varaibles in a program path, and can prioritize executions of interest. However, path explosion, the fact that the number of program executions is typically at least exponential in the size of the program, hinders the adoption of symbolic execution in the real world. In this paper, we present a method for generating test-cases using symbolic execution which reach a given potentially buggy target statement. Such a potentially buggy program statement can be found by static program analysis or from crash-reports given by the users. The test-case generated by our technique serves as a proof of the bug. Generating crashes at the target statement have many applications including re-producing crashes, checking warnings generated by static program analysis tools, or analysis of source code patches in code review process. By constantly steering the symbolic execution along the branches that are most likely to lead to the target program statement and pruning the search space that are unlikely to reach the target, we were able to detect deep bugs in real programs. To tackle the memory requirement due to the exponential growth of program paths, we propose a new scheme to manage program execution paths without exhausting system memory. Experiments on real-life programs demonstrate that our tool WatSym, built on selective symbolic execution engine S2E, can generate crashing inputs in feasible time and order of magnitude better than symbolic approaches (as embodied by S2E) failed.