Dissertation > Excellent graduate degree dissertation topics show

A Method to Generate Assertion and Proof about Assembly Language Certifying Compiler

Author: ZhangZhenZuo
Tutor: ChenYiYun
School: University of Science and Technology of China
Course: Computer Software and Theory
Keywords: Program Verification Bearing identification code Certifying compiler Assembly-level verification
CLC: TP314
Type: Master's thesis
Year: 2010
Downloads: 39
Quote: 0
Read: Download Dissertation


With the rapid development of computer science, software increasingly large-scale. Now consider the efficiency of software execution, but also increasingly concerned about their safety (Safety). High Confidence Software is committed to using cutting-edge technologies and tools to improve the security of computer software. Program verification is a method for constructing High Confidence Software, its principle is mathematically rigorous proof of program behavior consistent with its intended specification, thus ensuring the safety of the procedure. The program verifies the source code, assembly code. Source-level verification easier understanding and participation of programmers, but due to the low reliability of the ordinary compiler, the compiler can not guarantee that the assembly code generated by the verification of source code (Certified Source Code) is still scheduled to meet the safety norms. Although the assembly level verification to ensure the security of the generated assembly code, but if it is to manually write assembly code, writing assertions, interactive completion certificate, the cost is too high, the development of low efficiency. Therefore an ideal method is validated at the source code level, and then by integrating certifying compiler (Certifying Compiler) tool automatically generates a proven assembly code. This paper first introduces based on the nature of the program proven software security research at home and abroad as well as certifying compiler, then to introduced our project CComp the framework model: we have achieved a C-like language certifying compiler prototype in with standard notes compile source code into assembly code, but also to generate assembly code to meet the appropriate specifications Coq inspection certificate, thus ensuring the security of assembly code. The certifying compiler include: the front end of the compiler, assembler code generator, source-level verification condition generation, automated theorem proving, assembly-level assertion generator, assembly-level proof generator and assembler-level validation framework. The main work is concentrated in three parts of the back of a Hoare-style assembly-level validation framework, designed on the basis of the existing validation framework, the assertion language defined in this framework, and a new compilation level assertions and proven method of generating the assembly level assertion generation and assembly-level proof generator.

Related Dissertations

  1. Application and Research of Finite Element Method Among Lue Yang Electric Factory Slope Stability Analysis,TU43
  2. The Study on Network Planning and Optimization Technology of IP Core Networks,TN915.02
  3. Proof Generation for Certifying Compiler,TP314
  4. Verify with dynamic thread creation and exit multithreaded programs,TP311.53
  5. Analysis and Testing of Web Services Choreography Description Language,TP393.09
  6. A program verification tool design and implementation,TP311.53
  7. Axiomatic Semantics of Class and Polymorphism for Java,TP312
  8. The Study and Development of the Simulation Programmer for NC Lathers,TG519.1
  9. Design and Implementation of Static Verifier in VeriJava,TP312.1
  10. Axiomatic semantics of the Java language 's exception handling mechanism,TP312
  11. Research on Methods of Security Assurance Based on Computer-Assisted Proof,TP309
  12. Study on Program Verification,TP311.11
  13. Verification of Low-level Concurrent Code with Several Synchronization Mechanisms,TP332
  14. Automated Loop Invariant Generation for Program Verification,TP311.11
  15. Verifying Parallel Programs Using Software Transactional Memory,TP311.5
  16. Program Verification Based on Computer Algebra,TP311.1
  17. The Research of Partitioned Symbolic Execution Model and Its Environment Interaction Problem,TP311.11
  18. Study on Program Verification Based on Symbolic Computation,TP311.1
  19. Design of Parallel Optimization Algorithm and Software and Port of Numerical Software,TP311.52
  20. Slicing Execution for Verification of C Programs,TP312.1

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