RockSalt: Better, faster, stronger SFI for the x86

Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean Baptiste Tristan, Edward Gan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

72 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationPLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation
Pages395-404
Number of pages10
DOIs
StatePublished - 2012
Event33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'12 - Beijing, China
Duration: Jun 11 2012Jun 16 2012

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Other

Other33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'12
Country/TerritoryChina
CityBeijing
Period6/11/126/16/12

All Science Journal Classification (ASJC) codes

  • Software

Cite this