Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities
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 DecDisplayed time zone: Auckland, Wellington change
10:30 - 12:00 | |||
10:30 30mResearch paper | Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities OOPSLA DOI | ||
11:00 30mResearch 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 30mResearch paper | Purity of an ST monad: full abstraction by semantically typed back-translation OOPSLA DOI |