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
Y1 - 2012/8
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.
KW - Domain-specific languages
KW - Software fault isolation
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
AN - SCOPUS:84866401628
SN - 1523-2867
VL - 47
SP - 395
EP - 404
JO - ACM SIGPLAN Notices
JF - ACM SIGPLAN Notices
IS - 6
ER -