RockSalt

Better, faster, stronger SFI for the x86

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

Research output: Contribution to journalArticle

23 Citations (Scopus)

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 1 2012

Fingerprint

Trusted computing

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Cite this

Morrisett, G., Tan, G., Tassarotti, J., Tristan, J. B., & Gan, E. (2012). RockSalt: Better, faster, stronger SFI for the x86. ACM SIGPLAN Notices, 47(6), 395-404. https://doi.org/10.1145/2345156.2254111
Morrisett, Greg ; Tan, Gang ; Tassarotti, Joseph ; Tristan, Jean Baptiste ; Gan, Edward. / RockSalt : Better, faster, stronger SFI for the x86. In: ACM SIGPLAN Notices. 2012 ; Vol. 47, No. 6. pp. 395-404.
@article{e6be838df2274409868afb9ed98c1052,
title = "RockSalt: Better, faster, stronger SFI for the x86",
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.",
author = "Greg Morrisett and Gang Tan and Joseph Tassarotti and Tristan, {Jean Baptiste} and Edward Gan",
year = "2012",
month = "8",
day = "1",
doi = "10.1145/2345156.2254111",
language = "English (US)",
volume = "47",
pages = "395--404",
journal = "ACM SIGPLAN Notices",
issn = "1523-2867",
publisher = "Association for Computing Machinery (ACM)",
number = "6",

}

Morrisett, G, Tan, G, Tassarotti, J, Tristan, JB & Gan, E 2012, 'RockSalt: Better, faster, stronger SFI for the x86', ACM SIGPLAN Notices, vol. 47, no. 6, pp. 395-404. https://doi.org/10.1145/2345156.2254111

RockSalt : Better, faster, stronger SFI for the x86. / Morrisett, Greg; Tan, Gang; Tassarotti, Joseph; Tristan, Jean Baptiste; Gan, Edward.

In: ACM SIGPLAN Notices, Vol. 47, No. 6, 01.08.2012, p. 395-404.

Research output: Contribution to journalArticle

TY - JOUR

T1 - RockSalt

T2 - Better, faster, stronger SFI for the x86

AU - Morrisett, Greg

AU - Tan, Gang

AU - Tassarotti, Joseph

AU - Tristan, Jean Baptiste

AU - Gan, Edward

PY - 2012/8/1

Y1 - 2012/8/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84866401628&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84866401628&partnerID=8YFLogxK

U2 - 10.1145/2345156.2254111

DO - 10.1145/2345156.2254111

M3 - Article

VL - 47

SP - 395

EP - 404

JO - ACM SIGPLAN Notices

JF - ACM SIGPLAN Notices

SN - 1523-2867

IS - 6

ER -