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.
Slides (scm17-slides.pdf) | 372KiB |
Sun 15 Jan
10:30 - 10:40 Talk | Cătălin HriţcuInria Paris Link to publication | |||||||||||||||||||||||||||||||||||||||||
10:40 - 10:50 Talk | David NaumannStevens Institute of Technology File Attached | |||||||||||||||||||||||||||||||||||||||||
10:50 - 11:00 Talk | Gabriel SchererNortheastern University File Attached | |||||||||||||||||||||||||||||||||||||||||
11:00 - 11:10 Talk | Christine RizkallahUniversity of Pennsylvania, USA File Attached | |||||||||||||||||||||||||||||||||||||||||
11:15 - 12:00 Talk | File Attached |