Abstract

Separation logic is the basis for many tools that support sound, modular verification of programs, such as VeriFast. We are concerned with scenarios where separation-logic-verified code interacts with untrusted, non-verified code (for example, when installing plugins from the internet). Our goal is to compile the verified code in such a way that we can preserve the guarantees obtained from verification, even under this untrusted interaction. This preservation of guarantees can be expressed in terms of the notion of fully abstract compilation: a formal property that is sometimes used to define secure compilation. We contribute a new approach to secure compilation of verified to unverified C code that we conjecture to be fully abstract. The approach relies on target language support for capabilities: a well-studied form of unforgeable memory pointers that enables fine-grained, efficient privilege separation. We rely on a form of capabilities called linear capabilities. Linear capabilities are specially treated by the hardware to ensure that they can never be copied. Our compiler relies on information from both the source program and its verification proof, i.e. it will be formally defined as a separation-logic-proof-directed compiler.