Improving The Scalability And Feasibility Of Symbolic Execution

Software quality is of paramount importance for modern computing systems, especially in safety-critical applications. Software verification and validation(V&V) is one software engineering discipline aiming to improve the software quality. Symbolic execution is proposed by King in 1970 s and has been used as a basic program analysis technique in V&V activities. Recently, symbolic execution draws renewed interests both from academia and industry, partly due to the impressive progress in constraint solving, related algorithms and computation power. Symbolic execution feeds programs with symbolic inputs and executes programs symbolically. The feasibility of program paths is determined by a constraint solver. In the past years, symbolic execution has shown a great promise in many areas, such as automated test generation, proving program properties and bug detection.However, in practice, symbolic execution is still facing the scalability and feasiblity problems due to path explosion, constraint solving overhead and the complexity of domain-specific applications. In this thesis, we focus on how to improve the scalability and feasiblity of symbolic execution.The contributions of this thesis are listed as follows.1) We propose a new fashion of symbolic execution, named Speculative Symbolic Execution(SSE), to speed up symbolic execution by reducing the invocation times of constraint solver. In practice, constraint solving is almost always the most dominative in symbolic execution. In SSE, when encountering a branch statement, the search procedure may speculatively explore the branch without regard to the feasibility. Constraint solver is invoked only when the speculated branches are accumulated to a specified number or the end of the path is reached. If the current path is feasible, the procedure continues;otherwise, it backtracks. In addition, we propose three key optimization techniques that enhance SSE greatly. We present S2 PF, which integrates SSE with the general heuristic search framework in Symbolic Pathfinder(SPF). Experimental results on six programs show that, S2 PF can reduce the solver invocations by 36.4% to 48.7%(with an average of 40.3%), and save the search time by 30.6% to 43.5%(with an average of 35%).2) We propose regular property guided dynamic symbolic execution, a novel technique for checking programs against regular properties that can be described by finite state machines(FSM). Symbolic execution can be naturally applied to check programs against regular properties. However, symbolic execution is heavily confined by the path explosion problem. Our approach is based on the following observation: only the paths with specific event sequences can be accepted by the FSM. The main procedure of our approach is a dynamic symbolic execution(DSE) procedure. The key is that, after each execution, we evaluate each off-path-branch according to its history and future, and select the most hopeful off-path-branch to cover a path that can be accepted by the FSM. In our approach, the history and future of an off-path-branch are both represented by a set of states of the FSM. We use call strings context sensitive, flow sensitive interprocedural dataflow analysis to evaluate the future of off-path-branches. Our approach is a synergy of static analysis, dynamic symbolic execution and runtime verification, making different techniques to complement each others. We also propose an optimization technique to improve the precision of call strings(bounded) context sensitive dataflow analysis. We have implemented the regular property guided dynamic symbolic execution based on SPF and WALA. Experimental results on six real-world programs show that, our approach can improve the efficiency of dynamic symbolic execution by at least 1 to 2 orders of magnitude in checking programs against regular properties.3) We present a collaborative testing framework for applying symbolic execution in testing Web Services(WS). The distributed nature of service-oriented applications brings many difficulties to service testing, and also makes it infeasible to apply symbolic execution. We present a collaborative framework for testing WS, which makes it feasible to apply symbolic execution in service testing. The framework is based on the following three principles. 1. We use Testing Service to bring white-box testing to service-oriented architectures and to avoid the disturbance of testing to normal service. 2. We wrap symbolic execution tools as services to help to automatize the testing of WS. 3. We use test broker to automatize the testing procedure of WS. The framework provides necessary mechanism to make it feasible to apply symbolic execution in testing of WS. We have also shown the generality and scalability of the framework.