Dexter Kozen

Efficient Code Certification

In this talk I will describe a new approach to the certification of mobile code that addresses issues of efficiency and ease of implementation. Current type theoretic and logic-based approaches, although more general than ours, suffer from significant inefficiencies in time and space. We sacrifice generality for efficiency. In contrast to PCC [Necula and Lee], in which certificates can be difficult to generate and can be several times the size of the object code, our certificates are significantly smaller than the object code itself (.05-.25 times the object code size) and are relatively easy to produce in the code generation phase of compilation. In contrast to TAL [Morrisett et al.], no type inference is necessary. Verification is linear time (mostly table lookup) except for sorting of jump destinations, and involves no theorem proving or type inference. Unlike JAVA bytecode, our system operates at the level of native code; thus it is not interpreted and no further compilation is necessary. We ensure a basic but nontrivial level of code safety, including control flow safety, memory safety, and stack safety. A prototype has been implemented for SCHEME to x86.
December 2, 1998
Wean 8220