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

Abstract

Executing untrusted code while preserving security requires that thecode be prevented from modifying memory or executing instructionsexcept as explicitly allowed. Software-based fault isolation (SFI) or"sandboxing" enforces such a policy by rewriting code at theinstruction level. In previous work, we developed a new SFI techniquethat is applicable to CISC architectures such as the Intel IA-32,based on enforcing additional alignment constraints to avoiddifficulties with variable-length instructions. This report describesa machine-checked proof we developed to increase our confidence in thesafety provided by the technique. The proof, constructed for asimplified model of the technique using the ACL2 theorem provingenvironment, certifies that if the code rewriting has been checked tohave been performed correctly, the resulting program cannot perform adangerous operation when run. We describe the high-level structure ofthe proof, then give the intermediate lemmas with interspersedcommentary, and finally evaluate the process of the proof'sconstruction.