A Machine-Checked Safety Proof for a CISC-Compatible SFI Technique

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:

   author = {Stephen McCamant},
   title = {A Machine-Checked Safety Proof for a {CISC}-Compatible {SFI}
   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.