Sciweavers

Share
PLDI
2012
ACM

RockSalt: better, faster, stronger SFI for the x86

7 years 2 months ago
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
Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-
Added 27 Sep 2012
Updated 27 Sep 2012
Type Journal
Year 2012
Where PLDI
Authors Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan, Edward Gan
Comments (0)
books