Efficient Code Certification

We introduce a simple and efficient approach to the certification of compiled code. We ensure a basic but nontrivial level of code safety, including control flow safety, memory safety, and stack safety. The system is designed to be simple, efficient, and (most importantly) relatively painless to incorporate into existing compilers. Although less expressive than the proof carrying code of Necula and Lee or typed assembly language of Morrisett et al., our certificates are compact and relatively easy to produce and to verify. Unlike JAVA bytecode, our system operates at the level of native code; it is not interpreted and no further compilation is necessary