Research On The Foundamentals Of Compilation Correctness And Safety

Software security has become a critical issue that need to be considered throughout the software development cycle. During the software development process, from design to coding, any phase with security deficiencies can lead to insecure software. It is important to integrate security testing into the whole development process. Compilation is one of the most important phases in the software development process, which transforms source code to executable. The correctness and safety of the compilation process will have a great impact on the safety of the resulting executable code. With the rapid development of hardware and software verification technologies, many mature verification tools have emerged. Now it is possible to use these tools to verify complex software systems, such as compilers. In fact, compiler verification is one of the hottest research areas.The thesis focuses on compiler verification, and conducts research on some of the essential problems in the verification of compilers. In this thesis, A compiler verification framework based on program analysis is proposed. Methods for the specification and checking of program properties are also exploited, and a new method for program property checking based on the combination of type checking and model checking is proposed. A binary analysis framework for machine code checking and verification is also proposed, which helps to make a complete set of program checking tools for the compiler verification framework. In detail, the thesis focuses on the following topics:(1) The essential problems of compiler verification are exploited. A compiler verification framework based on program analysis is then proposed. The verification process is integrated into the framework as independent modules, with customizable analysis modules to adapt to application-specific property checking.(2) Methods for the representation of program properties are exploited. New methods for the representation of memory safety and information flow security are proposed. Memory safety properties are represent in a unified way with the type refinement mechanism. The typed representation of information flow security property on the SSA intermediate form is also exploited in this part. The study of program property representation method forms the basis of the compiler verification problem.(3) Methods for verifying the correctness of compiler implementation are exploited. Based on the understanding of various compiler implementation technologies, several methods for the verification of the correctness of implementation of the major components of a compiler implementation are proposed. The parser correctness is ensured by the parse-unparse verification method. The correctness of code generation and optimization implementation is verified by checking the correctness of the rewriting condition. For the verification of compiler optimization, an extended attribute grammar is introduced and is integrated with model checking tools to check the rewriting conditions.(4) Program analysis methods are carefully studied. After comparing the advantages and disadvantages of type checking and model checking method, a new technique is proposed that combines the two methods. The new method called TCMC is then applied to the checking of memory safety properties to explain its effectiveness. TCMC method provide a way for the uniform analysis method for the various program representations during the compilation process.(5) The machine code verification problem is discussed, and a new method for machine code property checking is proposed. The new method is based on decompileation techniques, and it can easily recover machine independent intermediate representations from machine code. The intermediate representation can be converted into SSA representation, and the TCMC method can then be used to check the property of the SSA form that is recovered from machine code(in the form of assembly code, or binary code).The new features of the thesis include:(1) A compiler verification framework based on program analysis is proposed. The framework supports flexible program property checking, and can be easily customized for the checking of new safety and security properties.(2) New methods for the representation of memory safety and information flow security are proposed. The new method makes extentions to standard type system, and can be used to represent many kinds of program properties.(3) New method for property checking using the combination of type analysis and model checking techniques is proposed. The new method (TCMC) makes use of the advantages of type checking and model checking, and improves the precision of the analysis.(4) A property checking method for machine code is proposed. With the method, control flow and data flow information can be recovered from machine code without the help of compiling or debugging information. Machine code is first transformed into machine independent intermediate representation. This machine code analysis method, together with the methods for source program checking, provide the compiler verification framework with a complete toolset for program property checking.