{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T02:17:54Z","timestamp":1772158674961,"version":"3.50.1"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3290332","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities"],"prefix":"10.1145","volume":"3","author":[{"given":"Lau","family":"Skorstengaard","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Brussel, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Secure Internet programming","author":"Abadi Mart\u00edn"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102165"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11576280_9"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243745"},{"key":"e_1_2_2_5_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2014. A Taste of Categorical Logic \u2014 Tutorial Notes. (2014). http:\/\/cs.au.dk\/~birke\/modures\/ tutorial\/categorical-logic-tutorial-notes.pdf  Lars Birkedal and Ale\u0161 Bizjak. 2014. A Taste of Categorical Logic \u2014 Tutorial Notes. (2014). http:\/\/cs.au.dk\/~birke\/modures\/ tutorial\/categorical-logic-tutorial-notes.pdf"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926401"},{"key":"e_1_2_2_7_1","volume-title":"Gross","author":"Carlini Nicholas","year":"2015"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_2_2_9_1","volume-title":"fully-abstract compilation by approximate back-translation. Logical Methods in Computer Science 13 (10","author":"Devriese Dominique","year":"2017"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813646"},{"key":"e_1_2_2_11_1","volume-title":"Arthur Azevedo de Amorim, and Benjamin C. Pierce","author":"Juglaret Yannis","year":"2016"},{"key":"e_1_2_2_12_1","volume-title":"Capability-Based Computer Systems","author":"Levy Henry M."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951941"},{"key":"e_1_2_2_14_1","volume-title":"Computer Security Foundations","author":"Patrignani Marco"},{"key":"e_1_2_2_15_1","volume-title":"Computer Security Foundations","author":"Patrignani Marco"},{"key":"e_1_2_2_16_1","volume-title":"Programming Languages and Systems","author":"Skorstengaard Lau"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5210\/fm.v2i9.548"},{"key":"e_1_2_2_19_1","unstructured":"Nick Szabo. 2004. Scarce Objects. https:\/\/nakamotoinstitute.org\/scarce-objects\/  Nick Szabo. 2004. Scarce Objects. https:\/\/nakamotoinstitute.org\/scarce-objects\/"},{"key":"e_1_2_2_20_1","volume-title":"CHERI: A Research Platform Deconflating Hardware Virtualization and Protection. In Workshop on Runtime Environments, Systems, Layering and Virtualized Environments (RESoLVE).","author":"Watson Robert NM","year":"2012"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2016.84"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2665671.2665740"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290332","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290332","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290332"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":22,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290332"],"URL":"https:\/\/doi.org\/10.1145\/3290332","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}