StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities

Lau Skorstengaard, Dominique Devriese, Lars Birkedal

Research output: Contribution to journalArticlepeer-review

28 Citations (Scopus)
239 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 number19
Pages (from-to)1-28
Number of pages28
JournalProceedings of the ACM on Programming Languages
Volume3
Issue numberPOPL
DOIs
Publication statusPublished - Jan 2019
EventACM SIGPLAN Symposium on Principles of Programming Languages - Lisbon, Portugal
Duration: 16 Jan 201918 Jan 2019
Conference number: 46

Keywords

  • fully abstract compilation
  • secure compilation
  • capability machines
  • linear capabilities
  • well-bracketed control flow
  • stack frame encapsulation
  • fully abstract overlay semantics

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