February 21, 2018
13:00-14:00
Louvain-la-Neuve
Shannon Room - Maxell building a.105
Reasoning About a Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management
by Dominique Devriesse, KUL
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.