Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Sun 17 Jan 2021 20:12 - 20:30 at PriSC - Formal analysis & proof techniques Chair(s): Marco Patrignani, Jonathan Protzenko

Capability machines are computers that provide support for fine grained control over memory accesses. Pointers are replaced by capabilities, unforgeable tokens of authority that represent the ability to access a memory location. As such, capability machines are an attractive target for secure compilation, and this interest is further compounded by the recent commitment from Arm to develop an industrial prototype of CHERI-based capability machines. It is thus no surprise that numerous recent works have proposed techniques for enforcing well-bracketed control-flow (WBCF) and local state encapsulation (LSE), temporal stack safety, or temporal heap safety. However, these solutions still fall short of ensuring what we believe to be complete stack safety. In this paper, we review recent propositions from the literature and identify limitations. We further propose a potential solution using a new form of capabilities.

preprint (paper.pdf)362KiB

Sun 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

19:00 - 20:30: Formal analysis & proof techniquesPriSC at PriSC
Chair(s): Marco PatrignaniStanford University, USA / CISPA, Germany, Jonathan ProtzenkoMicrosoft Research, Redmond
19:00 - 19:18
Talk
Nanopass Back-Translation of Multiple Traces for Secure Compilation Proofs
PriSC
Pre-print Media Attached
19:18 - 19:36
Talk
Explicit Leakage: Handling Side-Channel Behavior in Program Rewriting and Analysis
PriSC
Marc GourjonHamburg University of Technology and NXP Semiconductors Germany GmbH
Media Attached
19:36 - 19:54
Talk
Secure Optimization Through Opaque Observations
PriSC
Son Tuan VuSorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Albert CohenGoogle, Karine HeydemannSorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Arnaud de GrandmaisonARM, Christophe GuillonSTMicroelectronics
Pre-print Media Attached File Attached
19:54 - 20:12
Talk
The Fox and the Hound: Comparing Fully Abstract and Robust Compilation
PriSC
Carmine AbateMax Planck Institute for Security and Privacy, Bochum, Germany, Matteo BusiUniversità di Pisa - Dipartimento di Informatica
Pre-print Media Attached File Attached
20:12 - 20:30
Talk
Toward Complete Stack Safety for Capability Machines
PriSC
Aina Linn GeorgesAarhus University, Armaël GuéneauAarhus University, Alix TrieuAarhus University, Lars BirkedalAarhus University
Media Attached File Attached