Symbolic execution with over-approximation

Abstract

Program verification is difficult but crucial in establishing software's reliability and security. As the software industry grows rapidly, traditional verification methods, such as code reviewing, inspection, and manual testing, become laborious and less effective. Symbolic Execution (SE) is an important automation technique in program verification. SE can analyse a program automatically and obtain information about the feasible paths in the program. For each such path SE captures the condition on the inputs to reach the path, as well as the corresponding program behaviour. SE has received much attention from researchers in the last decade, and is used effectively in the software industry.

The biggest problems with symbolic execution are path explosion (efficiency) and the sophistication of program semantics or software systems (precision). In order to make SE scalable, existing SE approaches frequently use under-approximation---a class of techniques that narrow the search space of SE, such as concretisation and aggressive path pruning. This thesis shows that over-approximation can be more advantageous in some cases, especially when we can differentiate unimportant or irrelevant code from the more critical or interesting code.

In our research, we study the strengths and weaknesses of over-approximation adaptations in SE. We introduce novel techniques based on two types of over-approximation, namely ``contextual'' and ``regional'' over-approximation. Contextual over-approximation focuses on symbolically executing specific parts of a program, while disregarding the context information; this particular feature makes results reusable, thus reducing SE redundancy. Regional over-approximation (over-approximating the details) can focus SE on program parts that are the most beneficial (e.g., implying the most code coverage), while disregarding irrelevant details. This saves the cost of SE when the code can be better differentiated, and shows great promise in targeted SE or proof-oriented applications. A drawback of techniques that use over-approximation is that they introduce infeasible program states which could mean false positives. The cost of eliminating such false positives is substantial. We show how incremental constraint solving techniques, in particular, assumption checking is a potential solution in this case. We base our discussion in this thesis on three innovative implementations of SE that centre around the above ideas.