Research On Software Vulnerability Analysis Oriented Parallel Symbolic Execution

Symbolic execution in the field of software vulnerability analysis has made greatimprovement. Compared with traditional fuzzy testing, it has the advantage of test inputgeneration and execution path analysis, and improves vulnerability detection greatly. Becausethere is a large quantity of execution paths in software, it is low efficiency to analyze path one byone, and test coverage is difficult to improve. It becomes the bottleneck of symbolic execution.With the development of high performance hardware platform and new computing model,parallel symbolic execution technology becomes domestic and foreign research focus gradually.In order to improve parallel efficiency of software security test, the degree of parallelism of thealgorithms and the method of vulnerability detection has become the critical issues. The study onsoftware vulnerability analysis includes symbolic execution, constraint solution and parallelmethod of them in the thesis. The main task can be summarized as follows.1. In respect of static symbolic execution, the parallel method in which load unit consists ofpath families is proposed to improve the degree of parallelism. Through Program DependenceAnalysis, multi paths with control dependency which have the same symbolic value of targetstatement and are reducted into path family. Path family is unit of load scheduling in parallel test.Both the number of actual execution paths is reduced and the degree of parallelism of analysis ispromoted.2. In order to address the problem of interaction with environment, symbolic execution withmixed concrete symbolic input is proposed. The consistency model of program execution isdefined to analyze systematically approximation between symbolic execution and concreteexecution. The method for switching back and forth between symbolic execution and concreteexecution and the heuristic strategy of maintaining consistency are put forward. bydistinguishing solvable constraint from complex constraint and using concrete and symbolicvalues to simplify complex constraint, mixed path constraint solution algorithm is designed andrealized.3. In respect of dynamic symbolic execution, the sensitive point oriented test method forparallel approach is put forward to improve coverage of target statements. The method combinesthe advantages of both static and dynamic. Static analysis is used for realize the method forcomputing the distance from sensitive point to program execution trace based on call chainbacktrack. It provides the basis of oriented test. Distributed test model is designed based ondynamic symbolic execution, which achieves the iterative testing process, including distanceanalysis, path condition solution, cases generation and actual test. The test method combiningsensitive point oriented and symbolic execution strengthens the pertinence. 4. In respect of constant solution, Parallel Consistency Model for Global Constraints basedon Centralized Storage. As well as the model is integrated with backtrack search to parallelsolution method. Dynamic constraints distribution is used for addressing the issue ofload balancing. Collision is detected quickly due to centralized management of variable domain.Since pruning variable domain is monotonic, asynchronous consistency was realized to improvethe degree of parallelism. Parallel search is merged with parallel consistency by dividing andscheduling search space, to improve constraint solving efficiency.5. Static symbolic execution used in software security patches Comparison for the purposeof semantic differences analysis in basic block level. Through traditional structural comparison,syntax differences in function level are analyzed to find the maximum common subgraph. On thebasis, input and output behavior of basic block is analyzed by static symbolic execution. Thenthe I/O behavior is used for determining functional similarity so as to find semantic differences.Ultimately, the experimental results show the accuracy of match result is improved.Models and algorithms included in the thesis have been applied to Large scale DistributedParallel Vulnerability Detection System developed by our team. The experimental results showthat related technologies are feasible and effective and provide support for improve vulnerabilityanalysis efficiency.