SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Fri 9 Dec 2022 10:30 - 11:00 at Seminar Room G007 - Semantics and Security Chair(s): Derek Dreyer

Capability machines are a type of CPUs that support fine-grained privilege separation using capabilities, machine words that include forms of authority. Formal models of capability machines and associated calling conventions have so far focused on establishing two forms of stack safety properties, namely local state encapsulation and well-bracketed control flow. We introduce a novel kind of directed capabilities and show how to use them to make an earlier suggested calling convention more efficient. In contrast to earlier work on capability machine models we do not only consider integrity properties but also confidentiality properties; we provide a unary logical relation to reason about the former and a binary logical relation to reason about the latter, each expressive enough to reason about temporal stack safety. While the logical relations are useful for reasoning about concrete examples, they do not on their own demonstrate that stack safety holds for a large class of programs. Therefore, we also show full abstraction of a compiler from an overlay semantics that internalizes the calling convention as a single call step and explicitly keeps track of the call stack and frame lifetimes to a base capability machine. All results have been mechanized in Coq

Fri 9 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
Semantics and SecurityOOPSLA at Seminar Room G007
Chair(s): Derek Dreyer MPI-SWS
10:30
30m
Research paper
Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed CapabilitiesDistinguished Paper
OOPSLA
Aina Linn Georges Aarhus University, Alix Trieu ANSSI, Lars Birkedal Aarhus University
DOI
11:00
30m
Research paper
Plausible sealing for gradual parametricity
OOPSLA
Elizabeth Labrada University of Chile, Matías Toro University of Chile, Éric Tanter University of Chile, Dominique Devriese KU Leuven
DOI
11:30
30m
Research paper
Purity of an ST monad: full abstraction by semantically typed back-translation
OOPSLA
Koen Jacobs KU Leuven, Dominique Devriese KU Leuven, Amin Timany Aarhus University
DOI