RockSalt: Better, faster, stronger SFI for the x86

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

Research output: Contribution to journalArticlepeer-review

35 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)
Pages (from-to)395-404
Number of pages10
JournalACM SIGPLAN Notices
Volume47
Issue number6
DOIs
StatePublished - Aug 2012

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Fingerprint

Dive into the research topics of 'RockSalt: Better, faster, stronger SFI for the x86'. Together they form a unique fingerprint.

Cite this