Research And Implementation Of Statically-Guided Symbolic Execution For Vulnerability Detection

As a dynamic program analysis technique, symbolic execution has the advantages of high code coverage and no false positive. However, when applied to the field of vulnerability detection, the path exploration in symbolic execution, which aims at high code coverage, will reduce the efficiency of vulnerability detection and increase false negatives in the circumstance of limited time and computing resource. To address this issue, we go deeply into symbolic execution in this thesis, and guide path exploration with static analysis in order to improve the efficiency and accuracy of vulnerability detection.The main work is as follows:(1) In the aspect of vulnerability detection, we introduce the definition of vulnerability and the categories of vulnerability detection techniques, and conduct a comparative study between source code vulnerability detection and binary vulnerability detection. The advantages and disadvantages of static vulnerability detection and dynamic vulnerability detection are also discussed in this thesis.(2) As for symbolic execution, according to different execution strategies on branch instructions, symbolic execution is classified into two types, i.e. fork-based symbolic execution and execution-based symbolic execution. We summarized their representative work, and compared their advantages and disadvantages in real-world scenarios. Besides, we conducted a study on the two challenges in symbolic execution, i.e. path explosion and symbolic address/symbolic jump, including their causes, influence and common solutions. Finally, the applications of symbolic execution in the field of test case generation, malware analysis and vulnerability detection are listed in this thesis as well.(3) We researched and concluded the three problems faced by symbolic execution when applied to the field of vulnerability detection, i.e. the useless exploration for invulnerable paths, the reliance on seed inputs and the deficiency of existing execution state select strategies. To mitigate these problems, we proposed a statically-guided symbolic execution technique for vulnerability detection. At first, static analysis is used to exclude the exploration for invulnerable paths. Then, fork-based symbolic execution is applied to avert the reliance of seed input. At last, an execution state selection strategy based on the ratio of vulnerable paths is proposed to speed up the discovery of sensitive operations.(4) Based on statically-guided symbolic execution for vulnerability detection, we implemented a prototype named SAF-SE and evaluated it. Experimental results show that in the cases where symbolic executions are completed, SAF-SE can reduce the total number of analyzed instructions and time consumption without sacrificing the ability of vulnerability detection. Moreover, SAF-SE can explore more sensitive operations than traditional symbolic execution under the same time for large-scale programs, which increases the accuracy of vulnerability detection with limited time.