Another practice talk

[Zhichen Xu <zhichen@xxxxxxxxxxx>]

Dear All,

Thank you very much for coming to my practice talk last week, and providing
lots of valuable feedback.

For those who have missed my practice talk last week. You have another 
chance. I am going to give another practice tomorrow (6/15, Thursday) 
at 11:00am in cs2310. I would greatly appreciate if you can come.

Thanks,

--Zhichen

-- Abstract --

We show how to determine statically whether it is safe for untrusted 
machine code to be loaded into a trusted host system. 

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. 

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. 

This is joint work with Professor Bart Miller and Professor Tom Reps.