Research And Implementation Of Symbolic Execution Optimization Method For File Vulnerability

In the field of automated vulnerability mining,symbolic execution is a frequently used method.The goal is generally to comprehensively test the software and discover the vulnerability duly and accurately.Symbolic execution consists of two important modules,test case selection and path constraint solving.The former is related to the ability to discover vulnerabilities,test coverage and test code depth.The latter is used to generate test cases,and a large number of constraints are solved affects symbolic execution performance.File vulnerabilities are closely related to file structure.Triggering such vulnerabilities requires that the file format of the test case be correct.The parameter fixing method proposed in this paper maintains the file structure information field as a fixed value,and ensures the correctness of the file format of the test case generated by the symbolic execution.This paper designs a test case sorting method to select test cases for symbolic execution to improve code coverage and test deep code.In addition,the binary static analysis technique is incorporated into the symbolic execution process to reduce the number of path constraints,and the test cases generated by the constraint solution can cover key instructions to improve the probability of vulnerability discovery and mitigate the path explosion problem.In order to improve the symbolic execution throughput,this paper proposes a multi-level parallel method.The single node implements the parallelization of the constraint solving module.Based on the DCR(Decompose Computation Reduce)parallel programming model,the symbolic execution is distributed in multiple nodes.This paper takes the Avalanche system as the prototype and implements all the proposed optimization methods.The test of two CVE vulnerabilities(CVE-2015-8918 and CVE-2016-3622)shows that: 1)The parameter fixed optimization method can enhance the file vulnerability mining ability and discover the vulnerability that the original software system could not find for a long time;2)Constraint solution parallelization improved the throughput of the constraint solution by 22.8 times;3)Time efficiency improved by 55.4% after optimization of test case sequencing,and the test for deep block of instructions with vulnerabilities is faster;4)The pruning optimization for key instructions reduces the number of constraint solves by 20%;5)The system can run on multiple nodes after distributed optimization,which proves that distributed optimization achieves system parallelism.