Write a Blog >>

Capability machines are promising targets for secure compilers since capabilities can be used to enforce abstractions that are usually expected for high-level languages, such as well-bracketed control-flow (WBCF) and local state encapsulation (LSE). We present the first formalization of a capability machine that supports mechanized reasoning about deep semantic properties, including WBCF and LSE. Our formalization is done in the Coq implementation of Iris, a state-of-the-art concurrent higher-order separation logic, and includes a formalization of the logical relation defined by Skorstensgaard et al. [ESOP2018], which can used to prove WBCF and LSE.

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
PriSC
Sean AndersonPortland State University, Andrew TolmachPortland State University, Chris ChhakPortland State University
Media Attached File Attached
15:59 - 16:23
Talk
PriSC
Aina Linn GeorgesAarhus University, Alix TrieuAarhus University, Lars BirkedalAarhus University
Media Attached
16:23 - 16:47
Talk
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
PriSC
16:57 - 17:21
Talk
PriSC
Jay BosamiyaCarnegie Mellon University, Benjamin LimCarnegie Mellon University, Bryan ParnoCarnegie Mellon University
Media Attached File Attached
17:21 - 17:45
Talk
PriSC
Marco VassenaCISPA Helmholtz Center for Information Security, Marco PatrignaniStanford University & CISPA
Link to publication Media Attached File Attached