| Publication Title: |
Efficient, Verifiable Binary Sandboxing for a CISC Architecture |
| Publication Author: |
McCamant, Stephen |
| Additional Authors: |
Greg Morrisett |
| LCS Document Number: |
MIT-LCS-TR-988 |
| Publication Date: |
5-2-2005 |
| LCS Group: |
Program Analysis |
| Additional URL: |
|
| Abstract: |
| Executing untrusted code while preserving security requires
enforcement of memory and control-flow safety policies:
untrusted code must be prevented from modifying memory or
executing code except as explicitly allowed. Software-based
fault isolation (SFI) or \"sandboxing\" enforces those
policies by rewriting the untrusted code at the level of
individual instructions. However, the original sandboxing
technique of Wahbe et al. is applicable only to RISC
architectures, and other previous work is either insecure,
or has been not described in enough detail to give
confidence in its security properties. We present a novel
technique that allows sandboxing to be easily applied to a
CISC architecture like the IA-32. The technique can be
verified to have been applied at load time, so that neither
the rewriting tool nor the compiler needs to be trusted. We
describe a prototype implementation which provides a robust
security guarantee, is scalable to programs of any size, and
has low runtime overheads. Further, we give a
machine-checked proof that any program approved by the
verification algorithm is guaranteed to respect the desired
safety property. |
| To obtain this publication: |
|
|
|
To purchase a printed copy of this publication please contact
MIT
Document Services.
|