Dept. of Computer Science, Aarhus University
8200 Aarhus N
My research is on language-based security with an emphasis on the language part. I apply modern techniques for reasoning about programs and programming languages in a security setting.
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.
In recent time, the idea of using capabilities to provide access control in low-level machines has resurfaced. At the same time, significant advances has been made in the area of logical relations to the point where we are capable of reasoning about programs written in modern programming languages. We have designed a logical relation that allows us to reason about assembly programs for a simple capability machine.
In this talk, I will present what we consider a capability machine and a formalisation of a CHERI and M-Machine inspired capability machine. I will provide a couple of examples of programs along with their correctness lemmas. Finally, I will talk about the logical relation we have come up with that enable us to prove these lemmas.
In this talk, I will present the joint work I have been doing in Belgium with Dominique Devriese. The talk will consist of a presentation of capability machines and the formalisation we work with as well as a presentation of the logical relation we have developed to reason about programs on this capability machine.