Safety checking of machine code

13 years 9 months ago

Download ftp.cs.wisc.edu

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 ﬁnal 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 speciﬁed on the host side. We have implemented a prototype safe...

Zhichen Xu, Barton P. Miller, Thomas W. Reps

Real-time Traffic