Typestate Checking of Machine Code

10 years 3 months ago
Typestate Checking of Machine Code
We check statically whether it is safe for untrusted foreign machine code to be loaded into a trusted host system. (Here “safety” means that the program abides by a memory-access policy that is supplied on the host side.) Our technique works on ordinary machine code, and mechanically synthesizes (and verifies) a safety proof. Our earlier work along these lines was based on a C-like type system, which does not suffice for machine code whose origin is C++ source code. In the present paper, we address this limitation with an improved typestate system and introduce several new techniques, including: summarizing the effects of function calls so that our analysis can stop at trusted boundaries, inferring information about the sizes and types of stack-allocated arrays, and a symbolic range analysis for propagating information about array bounds. These techniques make our approach to safety checking more precise, more efficient, and able to handle a larger collection of real-life code ...
Zhichen Xu, Thomas W. Reps, Barton P. Miller
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where ESOP
Authors Zhichen Xu, Thomas W. Reps, Barton P. Miller
Comments (0)