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


Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)
139 Downloads (Pure)


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.
Original languageEnglish
Pages (from-to)1-55
Number of pages55
JournalJournal of Functional Programming
Issue numbere6
Publication statusPublished - 30 Mar 2021

Bibliographical note

Funding Information:
This research is partially funded by the Research Fund KU Leuven, by the Research Foundation - Flanders (FWO) under grant number G0G0519N and by the Air Force Office of Scientific Research under award number FA9550-21-1-0054. Thomas Van Strydonck holds a PhD Fellowship of the Research Foundation - Flanders (FWO).

Publisher Copyright:
© The Author(s), 2021. Published by Cambridge University Press.


Dive into the research topics of 'Linear capabilities for fully abstract compilation of separation-logic-verified code'. Together they form a unique fingerprint.

Cite this