Dissertation > Excellent graduate degree dissertation topics show

Certifying Compilation in an Infrastructure for Developing Trustable Software

Author: GeLin
Tutor: ChenYiYun
School: University of Science and Technology of China
Course: Computer Software and Theory
Keywords: software safety program verification Hoare logic Trusted Computing Base type safety verification framework certifying compiler
CLC: TP311.52
Type: PhD thesis
Year: 2007
Downloads: 619
Quote: 2
Read: Download Dissertation

Abstract


Nowadays, high-assurance software is more and more valued, and among its properties, safety and security are most important. Safety is the ability to guarantee that software execution does no harm to the system. And security is the ability to preserve the confidentiality, integrity, availability and authentication of data. There is a close relationship between safety and security. For example, hackers usually use low-grade safety errors, such as buffer overflows, out-of-bound array accesses and dangling pointer dereferences, to destroy a system or achieve unauthorized control of a system. Apparently, it is helpful to ensure software security by strengthening its safety.To achieve software safety, all program errors should be discovered before the execution of the program or be gently captured during the execution. The research goal of software safety is to build a wholesome scientific and technological infrastructure for the management of software safety. And the verification method for software to meet its safety policies (i.e. program verification) is one of the hot topics in this research field. In the past decade, great progress has been made in the area of program verification. Many projects adopt type-based or logic-based approaches to reason about program properties. And in recent years, some projects have tried to combine them. However, previous program verification projects have focused on either high-level programming languages or low-level assembly languages, but not on both simultaneously. Research on high-level languages has many advantages such as user-friendliness, early safety bug detection etc., but the TCB (Trusted Computing Base) is relatively large; on the other hand, the TCB of low-level program verification is much smaller but the low-level safety proofs are more complex and harder to construct than the high-level ones. Even though some certifying compilers are able to produce safety proofs for assembly programs based on the knowledge of the compiled source programs, only some simple program properties—typically those of type system—could be proved automatically. Much more complex properties, such as partial correctness about values, are hard to prove automatically in these compilers.Under the above considerations, in this dissertation, I present the design and implementation of a high-assurance software development infrastructure. In this infrastructure, source-level and assembly-level program verification could be done simultaneously, and a certifying compiler produces assembly-level safety proofs automatically from the source-level specifications and safety proofs. The main advantage of this infrastructure is that the proved safety properties include not only type properties, but also advanced properties, such as partial correctness about values. This dissertation presents the important technique I adopted in certifying compilation. That is, along with code generation, the compiler produces the safety proofs of the assembly programs satisfying assembly specifications from source-level programs, specifications and safety proofs. Both the specifications and the safety proofs are carried by the code, and could be checked by an assembly-level proof checker to ensure that the code satisfies its specifications. The work in this dissertation is inspired by TAL (Typed Assembly Language), CAP (Certified Assembly Programming) and PCC (Proof-Carrying Code) etc., and adopts an approach of combining both types and logics.In this dissertation, I, firstly, introduce some previous work on program verification and certifying compilation; then I present a high-assurance software development infrastructure; next I mainly present the certifying compilation techniques based on this infrastructure and the design and implementation of a certifying compiler prototype. These techniques include: verification condition generation (VC Gen), assembly-level code specification translation and generation, assembly-level safety proof generation, etc. I also discuss the influence of certifying compilation techniques on traditional compilation.The main contributions and characteristics of this dissertation are:It presents an infrastructure for high-assurance software development. This infrastructure gives an interface for programmers to provide source specifications and the proofs of programs satisfying these specifications along with source programs. A certifying compiler in this infrastructure could produce the assembly specifications and safety proofs from the source-level ones. Assembly-level proof checking removes the compiler from the TCB, and so enhances the reliability of the system. The automatic assembly-level proof generation alleviates the difficulty of writing proofs.It improves the design of source-level VC Generation algorithm. The new algorithm turns the problem of proving programs satisfying specifications into an equivalent problem of judging the validity of the verification conditions (VCs). This algorithm also combines the collection of side conditions in source typing rules and considers the simplification of VCs. The proving of source VCs makes the early bug detection possible and easy.It shows the design and implementation of a certifying compiler prototype, and this certifying compiler produces assembly-level specifications and safety proofs automatically from the source-level counterparts. The generated proofs contain the soundness proofs of VC generation, so that the VC generator is removed from the TCB. And this avoids the existence of a big TCB—VC generator. Compared with previous certifying compilers, this compiler could deal with much more complex program properties, such as partial correctness about values.

Related Dissertations

  1. File Protection System Research Based on Hardware Assisted Virtualization,TP309
  2. Application and Research of Finite Element Method Among Lue Yang Electric Factory Slope Stability Analysis,TU43
  3. The Research of Software Formal Verification Technology Based on Hoare Logic,TP311.52
  4. The Study on Network Planning and Optimization Technology of IP Core Networks,TN915.02
  5. Proof Generation for Certifying Compiler,TP314
  6. A Method to Generate Assertion and Proof about Assembly Language Certifying Compiler,TP314
  7. Verify with dynamic thread creation and exit multithreaded programs,TP311.53
  8. Analysis and Testing of Web Services Choreography Description Language,TP393.09
  9. A program verification tool design and implementation,TP311.53
  10. The Research of Anti-Trojan Technology Based JAVA Bytecode,TP393.08
  11. Axiomatic Semantics of Class and Polymorphism for Java,TP312
  12. The Study and Development of the Simulation Programmer for NC Lathers,TG519.1
  13. The Modelling and Application of a New Model of Software Reliability and Safety,TP311.52
  14. Analysis and Designs of Tax Bank Treasury Electronic Payment Platform System,TP311.52
  15. Embedded System Supported Safety Critical Software Design for Railway Signal,U284.362
  16. Design and Implementation of Static Verifier in VeriJava,TP312.1
  17. Axiomatic semantics of the Java language 's exception handling mechanism,TP312
  18. Analysis and Check of Type Conversion and Control Flow Safety Vulnerability,TP309
  19. Software Safety Assurance Framework and Safety Technology Application,TP311.52
  20. Research on the Trusted Computing Base and Security Mechanism of UCard,TP393.08
  21. Research on Methods of Security Assurance Based on Computer-Assisted Proof,TP309

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer software > Program design,software engineering > Software Engineering > Software Development
© 2012 www.DissertationTopic.Net  Mobile