Enforcing Well-Bracketed Control Flow on a Capability Machine using Local Capabilities
Capability machines are a type of processors that feature a form of low-level object capabilities, which can be used to enforce encapsulation of components. They are a compelling target for the secure compilation of high-level languages, although many challenges remain to be solved for this to happen. In this work, we investigate how to formally reason about code in a capability machine and, specifically, how to enforce well-bracketed control flow provably and efficiently, without relying on trusted stack management. It turns out that this can be realistically enforced using a form of local capabilities (as supported by CHERI) but there are quite a few non-obvious details that must be properly dealt with.
For proving results about the capability machine, we define a logical relation that can be used to reason about code on a capability machine. Our logical relation is closely related to one that was previously used for reasoning about well-bracketed control flow in a lambda calculus. For reasoning about local capabilities, we reuse the notion of public-private transitions, although the details are interestingly different. We use the logical relation for proving results about standard examples from the literature that rely on well-bracketed control flow. The proofs rely on a fundamental theorem that constitutes a very general and powerful statement of the guarantees provided by the capability machine for arbitrary, untrusted machine code.
Sun 15 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00
|What is Secure Compilation? Part II (Short talk)|
Cătălin Hriţcu Inria ParisLink to publication
|Can relational logic facilitate secure compilation? (Short talk)|
David Naumann Stevens Institute of TechnologyFile Attached
|Full Abstraction for Language Design (Short talk)|
Gabriel Scherer Northeastern UniversityFile Attached
|Cogent: Where we Stand and What Comes Next (Short talk)|
Christine Rizkallah University of Pennsylvania, USAFile Attached
|Enforcing Well-Bracketed Control Flow on a Capability Machine using Local Capabilities|