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

Lau Skorstengaard, Dominique Devriese, Lars Birkedal

Onderzoeksoutput: Articlepeer review

23 Citaten (Scopus)
193 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.
Originele taal-2English
Artikelnummer19
Pagina's (van-tot)1-28
Aantal pagina's28
TijdschriftProceedings of the ACM on Programming Languages
Volume3
Nummer van het tijdschriftPOPL
DOI's
StatusPublished - jan 2019
EvenementACM SIGPLAN Symposium on Principles of Programming Languages - Lisbon, Portugal
Duur: 16 jan 201918 jan 2019
Congresnummer: 46

Vingerafdruk

Duik in de onderzoeksthema's van 'StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities'. Samen vormen ze een unieke vingerafdruk.

Citeer dit