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 provide security guarantees at machine level which makes them an interesting target for secure compilation schemes that provably enforce properties such as control-flow correctness and encapsulation of local state. We provide a formalization of a representative capability machine with local capabilities and study a novel calling convention. We provide a logical relation that semantically captures the guarantees provided by the hardware (a form of capability safety) and use it to prove control-flow correctness and encapsulation of local state. The logical relation is not specific to our calling convention and can be used to reason about arbitrary programs.
A brief introduction to WebAssembly from a programming language researcher's perspective.
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.