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

LAU SKORSTENGAARD, DOMINIQUE DEVRIESE, LARS BIRKEDAL

Research output: Contribution to journalArticle

3 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
Pages (from-to)1-77
Number of pages77
JournalJournal of Functional Programming
Volume31
Issue numbere9
DOIs
Publication statusPublished - 15 Apr 2021

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