Download: PDF, PostScript, DSpace.
“A Machine-Checked Safety Proof for a CISC-Compatible SFI Technique” by Stephen McCamant. MIT Computer Science and Artificial Intelligence Laboratory technical report 2006-035, (Cambridge, MA), May 2006.
Executing untrusted code while preserving security requires that the code be prevented from modifying memory or executing instructions except as explicitly allowed. Software-based fault isolation (SFI) or “sandboxing” enforces such a policy by rewriting code at the instruction level. In previous work, we developed a new SFI technique that is applicable to CISC architectures such as the Intel IA-32, based on enforcing additional alignment constraints to avoid difficulties with variable-length instructions. This report describes a machine-checked proof we developed to increase our confidence in the safety provided by the technique. The proof, constructed for a simplified model of the technique using the ACL2 theorem proving environment, certifies that if the code rewriting has been checked to have been performed correctly, the resulting program cannot perform a dangerous operation when run. We describe the high-level structure of the proof, then give the intermediate lemmas with interspersed commentary, and finally evaluate the process of the proof's construction.
Download: PDF, PostScript, DSpace.
BibTeX entry:
@techreport{McCamant2006,
author = {Stephen McCamant},
title = {A Machine-Checked Safety Proof for a {CISC}-Compatible {SFI}
Technique},
institution = {MIT Computer Science and Artificial Intelligence Laboratory},
number = {2006-035},
address = {Cambridge, MA},
month = may,
year = {2006}
}
(This webpage was created with bibtex2web.)
Back to Program Analysis Group publications.