Research And Implementation Of Path Search Strategy In Dynamic Symbolic Execution

As a kind of dynamic program analysis technique,dynamic symbolic execution has been widely used in the field of software testing and verification with the advantages of high code coverage,automatic calculation of input values,accurate analysis results etc..Path search,the key operation in dynamic symbolic execution,is the crucial factor that affects the execution efficiency and code coverage.The traditional Path Depth-First Search is a common path search strategy,however,there are some deficiencies such as the path explosion problem,"hunger path",slow increment speed in code coverage and large storage space occupancy at runtime.In order to solve these problems,this thesis studies the existing path search strategies of dynamic symbolic execution and presents a new path search strategy which is based on the control flow graph(CFG)and combines Branch-Coverage-First Search,Random Search for IF-Statement-First and Path Depth-First Search.The main contributions of this thesis are outlined as follows.1.The basic theory of symbolic execution and dynamic symbolic execution,as well as the mainstream path search methods of existing dynamic symbolic execution are studied.A new path search strategy for dynamic symbolic execution is proposed to solve the problems in the traditional path search area.First of all,CFG corresponding to LLVM Intermediate Representation(LLVM-IR)of source code is constructed and used to guide path search instead of the symbolic execution tree,which eases the path explosion problem caused by the cycle structure and recursive call of functions in complex programs.Next,by combining Branch-Coverage-First Search,Random Search for IF-Statement-First and Path Depth-First Search,and setting the scope of solution for symbolic value,the new path search strategy avoids the “path starvation” state during program execution.Then,under the premise of ensuring the high path coverage of dynamic symbolic execution,the maximum line coverage and branch coverage are obtained by the minimum times of program execution.The increment speed of code coverage is accelerated.Finally,only the input value and related information are stored.In this way,the storage space is greatly reduced compared with the storage of the complete path constraint during dynamic symbolic execution.2.The path search module is designed.Integrated with the LLVM-IR plug-in module,a complete dynamic symbolic execution tool is implemented.This tool is used to provide execution paths for the verification of Modeling,Simulation and Verification Language(MSVL)program,by means of dynamic symbolic execution of LLVM-IR program which is generated by the MSVL compiler.3.The correctness of the workflow of the path search module is illustrated by a simple example.To evaluate the growth of line coverage and branch coverage of the path search strategy proposed in this thesis,it is compared with the traditional path search strategy.The evaluation is conducted on several real-world programs.