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.)
Abstract
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.