Dissertation > Excellent graduate degree dissertation topics show

Research on the Foundamentals of Compilation Correctness and Safety

Author: HuYan
Tutor: GongYuChang
School: University of Science and Technology of China
Course: Computer Applications
Keywords: compiler verification safety property model checking type system
CLC: TP314
Type: PhD thesis
Year: 2007
Downloads: 204
Quote: 1
Read: Download Dissertation

Abstract


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.

Related Dissertations

  1. Research on the Methods for Detecting Mismatch of Web Services Based on Bounded Model Checking,TP311.52
  2. Research on a Secure E-Commerce Payment Protocol Based on Four Parties,TP393.08
  3. Research on UML Modeling and Model Checking of CTCS-3 Train Control System,TP273
  4. Design and Implementation Automatic Analyzer for Security Protocol,TP393.08
  5. Formal Analysis and Verification of a Transaction Coordination Protocol Named WS-TX for Web Services,TP393.09
  6. Research on Security of E-Commerce Protocols Based on UPPAAL,TP393.08
  7. Timed automata model - based verification techniques,TP301.1
  8. Forecasting Model and Applied Research of Based on Time Series ARCH,O211.61
  9. Studies on the Dynamic Simulation Models for Growth of Super Hybrid Rice Seedings,S511
  10. The Monitoring of Farmland Soil Moisture and Water Management System for Cotton on Drip Irrigation under Mulch,S562
  11. Han Wei and Six Dynasties Chinese Guqin music,J632.31
  12. Research on Model Checking Algorithms of Ambients Calculi Systems,TP274
  13. The Analysis of Model Checking and Verification System of Network Security Protocol,TP393.08
  14. Research and Implement on Static Malware Detection System Based on Program Semantics,TP393.08
  15. The Application and Implemenation of PPTL Model Checking Tool,TP311.52
  16. Simulation and Analysis of Schedule Strategy of Reconfigrable HW System,TN791
  17. Study on Systems and Assesssment of Multi-interchange,U412.352
  18. Research on Interaction Adaptation of Time-Aware Web Services,TP393.09
  19. Research on Verification of Web Service Composition Based on XYZ/ADL,TP393.09
  20. HMIPv6 Formal Verification Research Based on Color Petri Nets,TN929.5
  21. The Application Study on Formalism of Multi-Party Non-repudiation Protocols on SVO Logic,TP393.08

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer software > Compiler,interpreter
© 2012 www.DissertationTopic.Net  Mobile