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

Lau Skorstengaard, Dominique Devriese, Lars Birkedal

Onderzoeksoutput: Other reportResearch

53 Downloads (Pure)

Samenvatting

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.
Originele taal-2English
Aantal pagina's86
StatusPublished - 7 nov 2018

Keywords

  • cs.PL

Vingerafdruk

Duik in de onderzoeksthema's van 'StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details'. Samen vormen ze een unieke vingerafdruk.

Citeer dit