StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details

Lau Skorstengaard, Dominique Devriese, Lars Birkedal

Research output: Book/ReportOther reportResearch

14 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. This document is a technical report accompanying a paper by the same title and authors, published at POPL 2019. It contains proofs and details that were omitted from the paper for space and presentation reasons.
Original languageEnglish
Number of pages86
Publication statusPublished - 7 Nov 2018

Fingerprint Dive into the research topics of 'StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details'. Together they form a unique fingerprint.

Cite this