POPL 2017
Sun 15 - Sat 21 January 2017
Sun 15 Jan 2017 11:15 - 12:00 at Salle 109, Barre 44-54 - Session II

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.

Slides (scm17-slides.pdf)372KiB