A capability machine is a kind of CPU with hardware support for fine-grained privilege separation. Practical designs and prototypes for such machines are seeing recent development as part of the CHERI project (University of Cambridge, SRI, ARM) (cheri-cpu.org, morello-project.org), making capability machines a promising target for designing and building new software with security in mind. In this talk, I will present some of the work done at Aarhus University and KU Leuven on developing formal principles for reasoning about security properties of code running on capability machines. I will show how one can prove functional correctness of programs that interact with untrusted (and possibly malicious) code while leveraging capabilities to protect their private state. The key aspects of this methodology are a program logic for reasoning about known code, and a logical relation providing a /universal contract/ of unknown code.

The whole work has been mechanized in Coq using the Iris framework.