Efficient Code Certification
Dexter C. Kozen · eCommons (Cornell University) · 1998
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. 1 Introduction An exciting recent development in program verification is the notion of certified code. When downloading executable code from an untrusted foreign source, a client also downloads a certificate that is checked before running the code to ensure that it is safe to run locally. The certificate is produced by the supplier ...