LLVM-based Bounded Model Checking Static Programs

Under the background of rapid development in science and technology,the application of the computer is more and more popular so that the program has widespread application.The program is widely used,including mobile applications,smart appliances control systems,access control systems,traffic control systems,high-speed rail train control systems and satellite communications systems and so on.With the gradual increase of people's safety awareness,the requirements for the safety and reliability of the program are stricter.How to protect the security and reliability of the program has been one of the core issues in the development and application of software technology.This dissertation will introduce the program analysis in the field of static program verification.Firstly,using LLVM(Low Level Virtual Machine)converts the source code into an intermediate representation and promotes the intermediate representation into a static single assignment form.Secondly,the loop will be unrolled in a finite time by using bounded model checking method.Additionally,the intermediate representation will be transformed into the equivalent formula based on SMT-lib2 specification by semantic analysis.Finally,the correctness of the parsed set of formulas is verified by the SMT(Satisfiability Modulo Theories)solver.In this paper,we implement the bounded model detection method of the basic block state transition system based on the LLVM-based intermediate representation,avoid the direct verification of the source code.This method realize the loop unfolding through the bounded model detection,encodes data flow through semantic analysis,encodes control flow by constructing transition relations,and uses SMT solver to verify the SMT-lib2 formula.We implement the optimization of the previous method and reduce the number of variables in the control flow.We also implement a bounded model checking method based on control dependence to encoding the control flow information.Through the experimental analysis,the three methods correctly realize program verification and trace the potential error location through the verification results of the SMT solver.The improved method based on state transition not only reduces the number of variables and the formula size,but also improves the verification efficiency.The verification method based on control dependence further reduces the variable overhead,greatly reduces the formula size,and the verification efficiency is faster.