Linear capabilities for fully abstract compilation of separation-logic-verified code

Separation logic is a powerful program logic for the static modular verification of imperative pro-grams. However,dynamicchecking of separation logic contracts on the boundaries between verifiedand untrusted modules is hard because it requires one to enforce (among other things) that outcallsfrom a verified to an untrusted module do not access memory resources currently owned by theverified module. This paper proposes an approach to dynamic contract checking by relying on sup-port for capabilities, a well-studied form of unforgeable memory pointers that enables fine-grained,efficient memory access control. More specifically, we rely on a form of capabilities calledlinearcapabilities for which the hardware enforces that they cannot be copied. We formalize our approachas a fully abstract compiler from a statically verified source language to an unverified target languagewith support for linear capabilities. The key insight behind our compiler is that memory resourcesdescribed by spatial separation logic predicates can be represented at run time by linear capabili-ties. The compiler isseparation-logic-proof-directed: it uses the separation logic proof of the sourceprogram to determine how memory accesses in the source program should be compiled to linearcapability accesses in the target program. The full abstraction property of the compiler essentiallyguarantees that compiled verified modules can interact with untrusted target language modules as ifthey were compiled from verified code as well.