Selective Symbolization Based Symbolic Execution

The large-scale use of computer and application software affects all aspects of human life.But there are inevitably various bugs in the software,and the existence of these bugs has caused many serious losses to human beings.Software testing use a variety of testing techniques to test the program,and then find the bugs in the software.Symbolic execution is a very popular software testing technique and plays a very important role in finding software vulnerabilities.However,because of the working mechanism of symbolic execution,it also has many problems.A major problem that symbolic execution facing is the cost of constraint solving.Symbolic execution will collect path constraints when it is running.And then it will call the solver to solve the constraints.Due to the limited ability of the solver,the solver cannot solve some constraints effectively.This has seriously affected the efficiency of symbolic execution.Therefore,this thesis wants to use different solving methods for constraints at the level of constraint solving to improve the efficiency of symbolic execution.Symbolic execution will call the solver to solve the entire collection of constraints all together.But sometimes the solver cannot solve some of the subconstraints efficiently.Therefore,this thesis can combine fuzzing and constraint solving at the level of constraint solving.For the collected constraints,some constraints are solved by fuzzing.And the other part of constraints can be solved by calling the solver.According to the characteristics of the two parts of the constraints,a suitable method is adopted to improve the efficiency of the solving.The main work of this thesis is as follows:(1)this thesis combines fuzzing and constraint solving at the level of constraint solving,and formally defines the optimal combination as the optimal policy calculation problem in the Markov Decision Process with cost.(2)The optimal policy problem of symbolic input variables is formally defined as a variable partitioning problem.And the variable partitioning is done according to the solution cost and the solution count.(3)The constraints are divided according to the relationship graph between the variables.And then the constraints are predicted by the offline trained model to decide whether to symbolize the input part.(4)The practical algorithm of this thesis is implemented on the two tools of KLEE and JFS,and a lot of experiments are carried out on the GSL benchmark program.This thesis compares with other existing methods in terms of effectiveness and efficiency to evaluate whether the method is effective.The experimental results show that the method in this thesis significantly improves the statement coverage and branch coverage compared with other existing methods.And the method in this thesis also has an order of magnitude acceleration when the same code coverage is achieved.