RockSalt: Better, Faster, Stronger Software Fault Isolation for the x86
Speaker: Prof. Greg Morrisett, Harvard U.
Date: Monday, September 17 2012
Time: 4:00PM to 5:30PM
Location: 32-G575
Host: CSAIL Security Seminar, CSAIL, MIT
Contact: Raluca Ada Popa, 3-6098, ralucap@mit.edu
Relevant URL: 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 variable
length instructions 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.
Joint work with Gang Tan (Lehigh), Jean-Baptiste Tristan (Oracle Labs),
Joe Tassarotti and Edward Gan (Harvard).
See other events that are part of CSAIL Security Seminar 2012/2013
See other events happening in September 2012
