StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities

LAU SKORSTENGAARD, DOMINIQUE DEVRIESE, LARS BIRKEDAL

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)
190 Downloads (Pure)

Abstract

We propose and study StkTokens: A new calling convention that provably enforces well-bracketed control flow and local state encapsulation on a capability machine. The calling convention is based on linear capabilities: A type of capabilities that are prevented from being duplicated by the hardware. In addition to designing and formalizing this new calling convention, we also contribute a new way to formalize and prove that it effectively enforces well-bracketed control flow and local state encapsulation using what we call a fully abstract overlay semantics.

Original languageEnglish
Article numbere9
Pages (from-to)1-77
Number of pages77
JournalJournal of Functional Programming
Volume31
Issue numbere9
DOIs
Publication statusPublished - 15 Apr 2021

Bibliographical note

Funding Information:
This research was supported in part by the ModuRes Sapere Aude Advanced Grant from The Danish Council for Independent Research for the Natural Sciences (FNU). Support for an STSM was received from COST Action EUTypes (CA15123). Dominique Devriese held a Postdoctoral fellowship from the Research Foundation Flanders (FWO) during most of this research. This research was supported in part by the Research Foundation Flanders (FWO).

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

Fingerprint

Dive into the research topics of 'StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities'. Together they form a unique fingerprint.

Cite this