Guided Symbolic Execution Technology And Its Application

With the rapid development of computer technology and information engineer-ing, software is becoming more and more important in people’s daily life. However, with the continuous increasement of software functionality and complexity, software defects are more likely to occur in the software life cycle. How to ensure the quality of software is an important issue. Software testing, static analysis and program verifica-tion are existing techniques to ensure the quality of software. Symbolic execution is a very promising program analysis technique. The basic idea of this technique is dynam-ic execution using symbol instead of specific input, analysis and collect branch path constraints and generate test cases through the constraint solver. It can systematical-ly explores the program’s execution space and generate test cases with high coverage. However, when the program structure is complex, or there are a lot of branches or the loop structure in large real programs and systems, symbolic execution may easily causes path explosion problem.Some research work aims to handle the path explosion problem, such as various path guidance technologies, path pruning and loop optimization. Existing guided sym-bolic execution technology and path pruning are concerned about proposing new path selection strategy or pruning explored path to explore new path, which can improve the efficiency of the symbolic execution. As far as loop optimization is concerned, there is no uniform standard for execution times of loop, and execution times of loop may not reach a certain value, which will affect coverage accuracy or test accuracy.In this thesis, we present new kinds of guided technologies, which are based on pruning and merging path. We use them to alleviate the path explosion problem in symbolic execution process. Based on guided symbolic execution technologies pro-posed, we validate the buffer overflow warnings to improve the validating efficiency. The main work of this paper is as follows:(1)We propose specific target guided and loop reachable upper bound guided sym-bolic execution technologies. The target in the program can be the result of static anal-ysis or a specific statement location appointed by the programmer. Our approach can guide symbolic execution to cover target statement as soon as possible through prun-ing useless path. Loop guided technology means when defects trigging is depended on loop iteration times, we guide the symbolic execution to explore deepest loop un-rolling path. Different from the existing loop optimization schemes, we can have a unified standard for execution times of loop.(2)We propose a approach to validate static buffer overflow warnings based on guided symbolic execution. Firstly we construct the buffer overflow model and ex-tract the defect constraints. Secondly we add defect constraint to the path constrain-t and classify warnings depend on the output of constraint solver. The result is di-vided into three categories:confirmed overflow、false warning and can not be deter-mined.Software testers can use different treatment schemes for different categories. Because static buffer overflow warnings include static target information, and the ac-curacy of warnings validation may depend on execution times of loop, we can apply guided symbolic execution technologies here.(3)We implemented a prototype tool based on the proposed technique. Our ex-periment includes two parts:benchmark with injected defect and real programs with buffer overflow vulnerability. The method proposed in this paper is discussed from sides like verification accuracy, reduction of false warnings and time and space over-head. The experimental results on real open source programs show that our method can effectively reduce false warnings which do not need to be manually validated and reduce time and space consumption in symbolic execution effectively.