The Research Of Partitioned Symbolic Execution Model And Its Environment Interaction Problem

High code coverage and automatic software testing is the key technology to develop high-quality software; symbolic execution model is a static analysis theory to implement the test case generation covering a specific execution paths. Symbolic execution is an important formal and automatic program analysis method, has potential ability to combine program abstract and reasoning, model checking and other theories, to application in automated testing, defects detection, program verification, validation and proofing.The basic principle of symbolic execution is transforming the computing process to the symbolic expression of the execution path's conditions that based on satisfiability theory by symbolized input data. So the test data generation problem is converted to constraint solving problems in satisfiability theory.Symbolic execution technology is developing rapidly in recent years, from early that only can be applied to the program that has simple data types, simple mathematical operations and simple single-procedure to now that can be applied to complex data types, complex operations, and multi-procedures programs.But the research development process that makes symbolic execution techniques practical still has flowing three difficulties. First, the approaches for analysis an external procedure call of arbitrary function have significant limitation (external call is the way that program interact with execution environment, so this limitation is also named environment-interaction problem). In practice, because of the external procedures are either invisible or to large-scale, it call not do symbolic execution analyzing effectively. The method use concrete variable value is not comprehensive and the environment modeling method is not practical. Second is the path explosion problem, the phenomenon in symbolic execution that path number of procedures will be growth exponentially with the program scale, which makes the analysis of large programs cannot be completed in tolerable time or resources consumption, and the function summary approach is not accuracy. Third, the analysis model of the program with complex data structures, pointer-based computing and dynamic memory allocation is not perfect. Currently, these issues are become the biggest obstacle to symbolic execution theory development, it has become a focus in academic research.The target of my research is to solve these problems. The work in this paper includes the following:First and most important, this paper proposed Partitioned Symbolic Execution (PSE) model to deal with the path explosion problem. PSE is a new symbolic execution model, the basic idea is to split a large scale program of multiple program units during analysis, therefore the path number of each unit can be controlled in a limitation, would not cause the continuous explosion problem. PSE can select different part of program to analysis in different period. There is condition to make the total time consuming is just the sum of every part's, which is getting a solution to the environment-interaction problem, and make the concrete execution's time is much less than symbolic execution's. In PSE the inter-unit call is also a external call, so the environment-interaction problem is critical.In this paper we present several methods to deal with this problem, including the distinguishing of procedure's parameter propriety,IO object modeling and program behavior analysis using execution state.Second, based on data flow analysis theory, propose a definition and a method to decide the properties of the external procedure call's parameters. Describing external procedures'data input and output behavior, by abstract the parameters of property which can effectively detect data input, and make symbolization. This process method will make the inter-procedure analysis issue become an intra-procedure issue, and data flow analysis is a well studied program analysis methods, the increased time consumption is much less than the symbolic execution.Third, proposed a symbolic execution system framework, including an execution engine and the intermediate language that applicable to PSE. To implement of the execution engine, framework set up a built-in heap blocks as primitive data type, and monitor memory allocate and release operations. Framework also use a symbolization system objects method, that monitor IO operations in the process of concrete execution of external procedure, establish relationship between the program behavior of external process and symbolic execution process. This is the method to deal with the problem that symbolic execution cannot be performance by the missing of external functions'representation, which can effectively solving the external environment-interaction problem. Make the selection arbitrary procedures of object program as analysis target unit is possible, its basis to implement PSE.Forth, study on how to use the PSE model to detect memory-related defects such as buffer overflow in program. Based on PSE, the paper studied an abstract representation of arbitrary form data structures and its semantics, and studied using separation logic reasoning rules and constraint solving methods to detect potential security vulnerability to improve the security of complex program.Finally, the experiments proof the effectiveness of the PSE model to handle the path exposition problem and environment-interaction problem.