A Formal Certifying Framework for Assembly Programs

Proofcarrying code brings two grand challenges to the research field of programming languages. One is to study the technology of certifying compilation. The other is to seek more expressive program logics or type systems to specify or reason about the properties of highlevel or lowlevel programs. And safety is an important issue among the properties of highassurance software. The verification method for software to meet its safety policies is one of the hot researches. In terms of the framework to design and verification of safety programs, and the pointer logic proof system, this paper introduces the research on the formal description of target machine, the formal certifying framework for assembly programs and property proof of assembly pointer programs. The main characteristics of the design and implementation are as follows: first, the design of the certifying framework is based on program verification method of Hoare style; second, program property related with pointers is proved using a pointer logic which is similar to the counterpart in the level of source language; and finally, a simple type system is designed to fulfill type checking on pointers. Moreover, this work has been formalized in the proof assistant Coq and all code is available on the website of the authors’ laboratory.