Importing and executing untrusted foreign code has become an everyday occurrence: Web servers download plug-ins and applets; databases load type-specific extensions; and operating systems load customized policies and performance measurement code. Certification of the safety of the untrusted code is crucial in these domains.

I have developed new methods to determine statically whether it is safe for untrusted machine code to be loaded into a trusted host system. My 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. 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.

I have implemented a prototype safety checker for SPARC machine-language programs, and applied the safety checker to examples (ranging from code that contains just a few branches, to code that contains nested loops, and to code that contains function and method calls). The safety checker was able to mechanically synthesize the loop invariants and check these examples in times ranging from less than a second to dozens of seconds.

(Click here to access the paper: PostScript, PDF.)