Research And Implementation Of Fuzzing Based On Symbolic Execution

Fuzz testing,as the most effective means of finding vulnerabilities,has been widely studied and applied in both academic circles and industry.However,there are obstacles such as magic numbers,checksum judgments,and complex conditions in the program,which prevent fuzzing from diving deep into the program and discovering potential vulnerabilities.As an accurate static analysis technique,symbolic execution uses mathematical expressions to describe statements,uses constraints to describe judgment conditions,and then solves the input that satisfies constraints.Therefore,the combination of symbolic execution and fuzzing can improve the ability of fuzzing to break through barriers.In this thesis,on the basis of using byte-level taint analysis to record tainted non-mov instructions,the operand dependency graph and comparison instruction dependency graph are established from tainted instructions,and concolic execution method is applied,which greatly improves the accuracy of fuzzing.First of all,this thesis establishes a perfect file system call model to solve the problem of inaccuracy and loss of taint information in the process of spreading.Then,this thesis analyzes the temporal and spatial characteristics of tainted instructions,and proposes methods that can identify magic numbers,checksum judgments,length fields,type fields and data chunks,and design a precise structured mutation operations based on these identified information,which improves the ability of fuzzers to pass obstacles.Finally,based on the operand dependency graph and the comparison instruction dependency graph,this thesis applies concolic execution method and optimizes the symbolic process of the loop statement,which improves the ability of fuzzing to pass complex conditions and discover paths.This thesis combines the above ideas to implement a byte-level taint analysis tool leetaint and a concolic execution tool Lee Sym,and add structured mutation operations in AFL.Then,a fuzzing system based on symbolic execution is completed by combining AFL and Lee Sym.Finally,Lee Sym conducted a vulnerability discovery ability test on the base64 utility and uniq utility of the LAVA-M test suit,and found not only all the listed vulnerabilities,but also some unlisted vulnerabilities.On the fuzzgoat program,Lee Sym also found all four types of vulnerabilities inserted? in the real environment,Lee Sym can improve the path coverage of the readelf utility in binutils and the gif2 rgb utility in giflib,and is higher than the average path coverage of AFL and Intriguer.The effectiveness of the hybrid fuzzing method proposed in this thesis and the accuracy of solving obstacles are demonstrated.