PLDI'00 Practice talk

[Zhichen Xu <zhichen@xxxxxxxxxxx>]

-N PLDI'2000 Practice Talk 
-S Zhichen Xu
-F Computer Sciences Department, U. Wisconsin at Madison
-T Safety Checking of Machine Code
-D 6/7/00
-W Wednesday
-M 11:00
-P 7331
-A
.pp
We show how to determine statically whether it is safe for untrusted machine code to be loaded 
into a trusted host system. 
.pp
Our safety-checking technique operates directly on the untrusted machine-code program, 
requiring only that the initial inputs to the untrusted program be annotated with typestate 
information and linear constraints. This approach opens up the possibility of being able 
to certify code produced by any compiler
from any source language, which gives the code producers more freedom in choosing the language in
which they write their programs. It eliminates the dependence of safety on the correctness of the
compiler because the final product of the compiler is checked. It leads to the decoupling of the safety
policy from the language in which the untrusted code is written, and consequently, makes it possible for
safety checking to be performed with respect to an extensible set of safety properties that are specified on
the host side. 
.pp
We have implemented a prototype safety checker for SPARC machine-language programs, and applied
the safety checker to several examples. The safety checker was able to either prove that an example met
the necessary safety conditions, or identify the places where the safety conditions were violated. The
checking times ranged from less than a second to 14 seconds on an UltraSPARC machine. 
.pp
This is joint work with Professor Bart Miller and Professor Tom Reps.
.pp