Research And Implementation Of Program Instrumentation In Dynamic Symbolic Execution

Symbolic execution is a way between program validation and program debugging,and it is a static analysis method.But it is not possible to detect software reliability comprehensively through symbolic execution.Dynamic symbolic execution is developed by symbol execution.In dynamic symbolic execution,the input value is express by symbol value.And it also provides a specific value for the program.When the application is execution,symbolic execution is performed as well.We can get a specific input through the solution of condition.So we can get many paths as much as possible.Instrumentation technology is one of the important techniques in the dynamic symbolic execution.Instrumentation technology is to analyze the specific program,construct its plug-in module.In the dynamic symbolic execution,we analyze the source program,construct the jacking module to achieve the input value of the symbolic,symbol calculation and constraint collection.Instrumentation in the program analysis and program detection has a wide range of applications.Researchers have developed a number of dynamic symbol execution tools.But lots of them are basically based on the Linux platform.We do the research about dynamic symbolic execution technology on the Windows platform.Instrumentation technology is also carried out under the Windows platform.The main work of this thesis is to study and implement the instrumentation in dynamic symbol execution.In this thesis,the purpose of the program is to complete the implementation of dynamic symbols,so we have to calculate the symbol to collect constraints.This thesis is based on LLVM(Low Level Virtual Machine)IR(Intermediate Representation)code.The main contributions include the following points:1.We do research about the technology of dynamic symbolic execution technology.Dynamic symbol execution as the goal,we designed dynamic symbolic execution framework and the instrumentation under the Windows platform.2.We do research on LLVM IR language,including its lexical analysis.In the analysis of the process,we collect the information of instrumentation.This article mainly focuses on the implementation dynamic symbolic execution for LLVM IR which is generated by the MSVL(Modeling Simulation Verification Language)compiler.3.We design the instrumentation in the dynamic symbolic execution.We achieved the goal of dynamic symbolic execution.(1)We design the pile function.It can implement the symbolic of program input value,the symbolic variables of the operation,as well as the collection of constraints.(2)We output the control flow graph of the program for later path searching.4.We use a selection of representative test cases and an example "Bubble Sorting" to verify the correctness and availability of program stakes in dynamic symbolic execution.