A standard method for securing untrusted code is code rewriting, whereby operations that might compromise a safety policy are secured by additional dynamic checks. In this paper, we propose a novel approach to sandboxing that is based on a combination of code rewriting and hardware-based memory protection. In contrast to previous work, we perform rewriting on raw binary code and provide a machine-checkable proof of safety that includes the interaction of the untrusted binary with the operating system. This proof constitutes a crucial step towards the use of rewritten binaries with proof-carrying code.
A version of this paper is to appear at FAST 2005