@article{f9bbcb825d0847ddbc41cc0f7c1b956a,
title = "StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities",
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.",
keywords = "fully abstract compilation, secure compilation, capability machines, linear capabilities, well-bracketed control flow, stack frame encapsulation, fully abstract overlay semantics",
author = "Lau Skorstengaard and Dominique Devriese and Lars Birkedal",
year = "2019",
month = jan,
doi = "10.1145/3290332",
language = "English",
volume = "3",
pages = "1--28",
journal = "Proceedings of the ACM on Programming Languages",
issn = "2475-1421",
publisher = "Association for Computing Machinery",
number = "POPL",
note = "ACM SIGPLAN Symposium on Principles of Programming Languages, POPL ; Conference date: 16-01-2019 Through 18-01-2019",
}