StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities. (15th April 2021)

• Record Type: Journal Article
• Authors: SKORSTENGAARD, LAU; DEVRIESE, DOMINIQUE; BIRKEDAL, LARS
• Is Part Of: Journal of functional programming. Volume 31(2021)
• Publication Date: 2021-04-15
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S095679682100006X
• Languages: English
• ISSNs: 0956-7968

Abstract

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.