Certifying Compilation and Run-Time Code Generation

A certifying compiler takes a source language program and produces object code, as well as a certi cate" that can be used to verify that the object code satis es desirable properties, such as type safety and memory safety. Certifying compilation helps to increase both compiler robustness and program safety. Compiler robustness is improved since some compiler errors can be caught by checking the object code against the certi cate immediately after compilation. Program safety is improved because the object code and certi cate alone are su cient to establish safety: even if the object code and certi cate are produced on an unknown machine by an unknown compiler and sent over an untrusted network, safe execution is guaranteed as long as the code and certi cate pass the veri er. Existing work in certifying compilation has addressed statically generated code. In this paper, we extend this to code generated at run time. Our goal is to combine certifying compilation with run-time code ge...

• Type: Conference
• Year: 1999
• Where: PEPM
• Authors: Luke Hornof, Trevor Jim
• Keywords: Compiler Robustness, Object Code, PEPM 1999, Run-time Code Generation, Software Engineering