In Workshop on Formal Aspects in Security and Trust (FAST 2005), LNCS 3866, Springer-Verlag, pages 171-186, 2005. (Previous version also available as UNSW Computer Science and Engineering Technical Report no. UNSW-CSE-TR-0511, 2005.)
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.
PDF version (16 pages)
Proof scripts are available.
This page is part of Manuel Chakravarty's WWW-stuff.