Symbolic Execution Based On The Analysis Of Software Taint

Software security is closely related to our daily life. It is a topic that we pay close attention to. Software vulnerabilities are the most important tasks for software security personnel. Currently, there are two ways to study the most popular method of software vulnerabilities. The stain analysis method is to set up the information from the risk path to be contaminated data, while the analysis of the instruction statement, and found that the relevant data are also set to be contaminated data, a nd then according to the specific vulnerability to explore the loopholes in the rules. This analysis method is a method based on the data stream to explore the vulnerability. Another method of using symbolic representation variables, instead of the actual variable value simulation software, is called symbolic execution.There are three problems, which are the detection blind spot, which can not be analyzed, and the path coverage is low. Performance in the use of detection tools to explore three aspects, first, the change of the test case can not be informed that there is no change in the process of the implementation path; second, after the discovery of vulnerabilities can not further narrow the scope of the vulnerability can only locate the variable itself and can not be found to trigger the vulnerability specific byte or bit, and finally, a test case analysis is not generated after the completion of the path of the test case.According to the above problems, this paper puts forward third kinds of pollution control, which is based on the two kinds of state: "pollution" and "non pollution". It expands the detection state, and summarizes the existing vulnerabilities, designs six kinds of loopholes, and can avoid the three problems above, and can find the potent ial of the software. With the method of symbolic execution and blot analysis, all the memory byte can be assigned to a symbol variable, recording their mapping relationship to help track analysis, save the path conditions of the previous symbol execution, in order to guide the generation of test cases.In this thesis, we design and implement the STD and SESTD according to the above six rules and three kinds of pollution state to verify the feasibility and efficiency of the theory. SESTD has a symbolic stain management model, which can be analyzed, can clearly identify the source of the source of the culprit is what byte. It is also capable of generating new and effective test cases using the saved path information. In the end, two kinds of optimization methods are proposed to improve the operating efficiency and reduce the cost of the API filter.Experiments show that STD and SESTD can effectively explore the program vulnerabilities, in the experiment, we use the system to detect the five software on the market, scanning out the 59 vulnerabilities, loading after optimization of the STD, software execution time increased 3.2 times, while LIFT is 3.7 times, TaintC heck is 20 times, has the most ideal system overhead. SESTD system overhead is only 16.89 times faster than TaintCheck.