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

Lau Skorstengaard; Dominique Devriese; Lars Birkedal

doi:10.1145/3290332

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

Lau Skorstengaard, Dominique Devriese, Lars Birkedal

Informatica en Toegepaste Informatica

Onderzoeksoutput: Article › peer review

28 Citaten (Scopus)

248 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-2	English
Artikelnummer	19
Pagina's (van-tot)	1-28
Aantal pagina's	28
Tijdschrift	Proceedings of the ACM on Programming Languages
Volume	3
Nummer van het tijdschrift	POPL
DOI's	https://doi.org/10.1145/3290332
Status	Published - jan 2019
Evenement	ACM SIGPLAN Symposium on Principles of Programming Languages - Lisbon, Portugal Duur: 16 jan 2019 → 18 jan 2019 Congresnummer: 46

Toegang tot document

10.1145/3290332Licentie: Unspecified

popl19main-p15-p-9362553-39308-finalFinal published version, 534 KBLicentie: Unspecified

28 Citaties
1 Other report

StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details
Skorstengaard, L., Devriese, D. & Birkedal, L., 7 nov 2018, 86 blz.
Onderzoeksoutput: Other report › Research

Open Access
Bestand

Citeer dit

@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",

}

TY - JOUR

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

AU - Skorstengaard, Lau

AU - Devriese, Dominique

AU - Birkedal, Lars

N1 - Conference code: 46

PY - 2019/1

Y1 - 2019/1

N2 - 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.

AB - 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.

KW - fully abstract compilation

KW - secure compilation

KW - capability machines

KW - linear capabilities

KW - well-bracketed control flow

KW - stack frame encapsulation

KW - fully abstract overlay semantics

U2 - 10.1145/3290332

DO - 10.1145/3290332

M3 - Article

VL - 3

SP - 1

EP - 28

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - POPL

M1 - 19

T2 - ACM SIGPLAN Symposium on Principles of Programming Languages

Y2 - 16 January 2019 through 18 January 2019

ER -

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

Samenvatting

Toegang tot document

Vingerafdruk

Onderzoekersoutput

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

Citeer dit