Write a Blog >>

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

Displayed time zone: Saskatchewan, Central America change

15:35 - 17:45
Compartmentalization, memory safety, and isolationPriSC at Rosalie
Chair(s): Marco Patrignani Stanford University & CISPA , Jonathan Protzenko Microsoft Research, Redmond
15:35
24m
Talk
Flexible Tag-based Policies for Compartmentalized C
PriSC
Sean Anderson Portland State University, Andrew Tolmach Portland State University, CHR Chhak Portland State University
Media Attached File Attached
15:59
24m
Talk
Mechanized Reasoning about a Capability Machine
PriSC
Aina Linn Georges Aarhus University, Alix Trieu Aarhus University, Lars Birkedal Aarhus University
Media Attached
16:23
24m
Talk
Securing Interruptible Enclaves
PriSC
Matteo Busi Università di Pisa - Dipartimento di Informatica, Job Noorman imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Jo Van Bulck imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Letterio Galletta IMT School for Advanced Studies, Pierpaolo Degano Università di Pisa - Dipartimento di Informatica, Jan Tobias Mühlberg imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Frank Piessens KU Leuven
Media Attached File Attached
16:47
10m
Break
Mini-break
PriSC

16:57
24m
Talk
WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing
PriSC
Jay Bosamiya Carnegie Mellon University, Benjamin Lim Carnegie Mellon University, Bryan Parno Carnegie Mellon University
Media Attached File Attached
17:21
24m
Talk
Memory Safety Preservation for WebAssembly
PriSC
Marco Vassena CISPA Helmholtz Center for Information Security, Marco Patrignani Stanford University & CISPA
Link to publication Media Attached File Attached