Safety Checking of Machine Code
Zhichen Xu, Barton, P. Miller, and Thomas Reps
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
ntrusted 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 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.
(Click here
to access the paper.)
University of Wisconsin