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

Sun 15 Jan

SCM-2017
10:30 - 12:00: SCM - Session II at Salle 109, Barre 44-54
SCM-2017148447260000010:30 - 10:40
Talk
Link to publication
SCM-2017148447320000010:40 - 10:50
Talk
David NaumannStevens Institute of Technology
File Attached
SCM-2017148447380000010:50 - 11:00
Talk
Gabriel SchererNortheastern University
File Attached
SCM-2017148447440000011:00 - 11:10
Talk
Christine RizkallahUniversity of Pennsylvania, USA
File Attached
SCM-2017148447530000011:15 - 12:00
Talk
File Attached