LLVM IR Programs Verification Baesd On CEGAR

With the application of software in a wide range of diverse fields,the scale of software is increasing greatly as well as the complexity.Meanwhile,software security issues also turn to be prominent.Therefore,how to improve the correctness,reliability and security of software systems is a great challenge in the computer science.As a kind of important automatic verification technique,model checking has become an important approach to enhance the reliability and security of software.However,high complexity of algorithms and difficulties of implementation are the main bottlenecks for model checking of verification algorithms.In most cases,a model checker only supports one verification algorithm for one programming language.LLVM is a compiler framework,and any programming language supported by LLVM front-end can be transformed into the intermediate representation LLVM IR.Additionally,optimization strategies and analysis methodologies of LLVM are applied efficiently in LLVM IR,which provide convenience for program analysis and verification.In this thesis,we study the abstract verification theory and method for LLVM IR programs,which can support the abstract verification of various programming languages.The main contributions of this thesis are outlined as follows.1.The framework of LLVM,the syntax and semantics of LLVM IR are studied.Lexical analysis and syntactic parsing of the LLVM IR programs are conducted.Consequently the algorithm for the CFA generation of LLVM IR programs is put forward.2.Inspired by CEGAR,we propose the CFA based method for verifying LLVM IR programs.Then,the basic framework of LLVM IR programs verification tool is designed according to the method above.The design and implementation schemes of the each module are presented in detail.In addition,the corresponding verification tool is implemented in C++,and ultimately the verification of programs written in different programming languages is conducted.3.The test cases of LLVM IR programs are generated based on the C and MSVL programs.And the test cases are used to test the CEGAR based LLVM IR program verification tool.The results demonstrate the correctness and availability of the verification tool developed.