TY - GEN
T1 - RockSalt
T2 - 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'12
AU - Morrisett, Greg
AU - Tan, Gang
AU - Tassarotti, Joseph
AU - Tristan, Jean Baptiste
AU - Gan, Edward
N1 - Copyright:
Copyright 2012 Elsevier B.V., All rights reserved.
PY - 2012
Y1 - 2012
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=84863454556&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84863454556&partnerID=8YFLogxK
U2 - 10.1145/2254064.2254111
DO - 10.1145/2254064.2254111
M3 - Conference contribution
AN - SCOPUS:84863454556
SN - 9781450312059
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 395
EP - 404
BT - PLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation
Y2 - 11 June 2012 through 16 June 2012
ER -