Securing Interruptible Enclaves
Computer systems often provide hardware support for isolation mechanisms like privilege levels, virtual memory, or enclaved execution. Over the past few years, several successful software-based side-channel attacks have been developed that break, or at least significantly weaken, the isolation that these mechanisms offer. Extending a processor with new (micro)architectural features brings a risk of enabling new such side-channel attacks.
Here, we summarize our work in extending a processor with new features \emph{without} weakening the security of the isolation mechanisms that it offers.
For that, we first argue that a sensible formal criterion for proving the security of a processor extension is \emph{full abstraction}. Then, we sketch the proof that our carefully designed extension of a microprocessor supports interruptibility of enclaved executions in a secure manner.
(talk.pdf) | 252KiB |
Sat 25 Jan Times are displayed in time zone: Saskatchewan, Central America change
15:35 - 17:45: Compartmentalization, memory safety, and isolationPriSC at Rosalie Chair(s): Marco PatrignaniStanford University & CISPA , Jonathan ProtzenkoMicrosoft Research, Redmond | |||
15:35 - 15:59 Talk | Flexible Tag-based Policies for Compartmentalized C PriSC Sean AndersonPortland State University, Andrew TolmachPortland State University, CHR ChhakPortland State University Media Attached File Attached | ||
15:59 - 16:23 Talk | Mechanized Reasoning about a Capability Machine PriSC Media Attached | ||
16:23 - 16:47 Talk | Securing Interruptible Enclaves PriSC Matteo BusiUniversità di Pisa - Dipartimento di Informatica, Job Noormanimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Jo Van Bulckimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Letterio GallettaIMT School for Advanced Studies, Pierpaolo DeganoUniversità di Pisa - Dipartimento di Informatica, Jan Tobias Mühlbergimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Frank PiessensKU Leuven Media Attached File Attached | ||
16:47 - 16:57 Break | Mini-break PriSC | ||
16:57 - 17:21 Talk | WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing PriSC Jay BosamiyaCarnegie Mellon University, Benjamin LimCarnegie Mellon University, Bryan ParnoCarnegie Mellon University Media Attached File Attached | ||
17:21 - 17:45 Talk | Memory Safety Preservation for WebAssembly PriSC Marco VassenaCISPA Helmholtz Center for Information Security, Marco PatrignaniStanford University & CISPA Link to publication Media Attached File Attached |