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
3:30pm
Wean 8220