| As the developing of computer science, the scale of software is larger and larger. People pay more and more attention on the safety of software. High-confidence software is working on new edge-cutting tools and method to improve the safety of computer software. Program verification works on how to prove the behavior of program satisfies predetermined specification by using mathematical knowledge. Program verification can be done both on source code and assembly code. Verify source code is much easier to understand, but because of the low reliability of normal compiler, we can't guarantee that assembly code which is compiled by normal compiler using certified source code still satisfies the specification. Verify assembly code can ensure the safety of assembly code, but it is not easy to write assertion and proof about assembly code manually. So there is a perfect method is that we can verify source code, and compile these code using certifying compiler, then we can get certified assembly code which includes both code and proof of safety.In this theism, I introduce some previous work on Program verification in the area of software safety and certifying compiler. Then I will introduce the framework of our program CComp: we implement a prototype of certifying compiler whose source language is Clike. This certifying compiler not only translates the source code to assembly code, but also generates proofs which say the assembly code can satisfy the specification.In this certifying compiler, there are Front End, Code Generation, Verification Code Generation, Auto Theorem Prove, Assertion Generation on Assembly Code, Proof Generation on Assembly Code and a verification framework. In this paper, we present a low-level verification framework following Hoare-style certification methods. Based on the framework, we give a definition of assertion language for assembly code and a feasible method to automatically generate assertions and proof for assembly code. |
PDF Full Text Request