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 Jan
|10:30 - 10:40|
Cătălin HriţcuInria ParisLink to publication
|10:40 - 10:50|
David NaumannStevens Institute of TechnologyFile Attached
|10:50 - 11:00|
Gabriel SchererNortheastern UniversityFile Attached
|11:00 - 11:10|
Christine RizkallahUniversity of Pennsylvania, USAFile Attached
|11:15 - 12:00|