RockSalt: better, faster, stronger SFI for the x86

Software-based fault isolation (SFI), as used in Google’s Native Client (NaCl), relies upon a conceptually simple machine-code analysis to enforce a security policy. But for complicated architectures such as the x86, it is all too easy to get the details of the analysis wrong. We have built a new checker that is smaller, faster, and has a much reduced trusted computing base when compared to Google’s original analysis. The key to our approach is automatically generating the bulk of the analysis from a declarative description which we relate to a formal model of a subset of the x86 instruction set architecture. The x86 model, developed in Coq, is of independent interest and should be usable for a wide range of machine-level verification tasks. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification General Terms security, verification Keywords software fault isolation, domain-specific languages

• Type: Journal
• Year: 2012
• Where: PLDI
• Authors: Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, Edward Gan
• Keywords: Declarative Description, PLDI 2012, Programming Languages, Software Fault Isolation, X86 Instruction Set