Research And Implementation Of Dynamic Taint Analysis Method Combined With Concolic Symbolic Execution

With the growth of software engineering projects,software security issues have become current research points.The China National Vulnerability Database(CNVD)collected 19,930 vulnerabilities in 2020,setting a new high in the number of vulnerabilities in the past ten years.The main reason for vulnerabilities is that software developers made mistakes in the design and development process.In the field of software defect detection,taint analysis,symbolic execution are the methods with high attention.This article uses the advantages of concolic symbolic execution technology,combined with dynamic taint analysis,to ensure the accuracy of the analysis,and to improve the efficiency of software defect detection.Concolic symbolic execution and dynamic taint analysis have their own limitations.In this paper,we combine them to assist in dynamic taint analysis,and propose the following solutions.In order to solve the problem of false negative in dynamic taint analysis and the limitation of not being able to generate test input,considering that SPF,a symbolic execution tool based on model checking,can systematically explore program path,automatically generate test input by calling constraint solver,and concrete execute in case of complex constraints to simplify path constraints,a concolic symbolic execution method is introduced.In order to solve the problem of path explosion in symbolic execution,this method uses program dependency to guide symbolic execution,prunes redundant paths based on the concept of path equivalence,and effectively reduces the number of paths explored by symbolic execution.This method is mainly based on JPF framework,extends the implementation of Taint Instruction Factory class to modify the execution semantics of the program,uses Attribute object to store the symbol taint tag,and uses Listener to monitor the execution for taint propagation analysis,so as to reduce the scale of code instrumentation.Finally,a prototype system is implemented based on the method in this paper.Through the analysis and comparison of the test results of Droid Bench data set,it shows that the method is feasible and effective.