{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:09Z","timestamp":1780994709093,"version":"3.54.1"},"reference-count":47,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2021,4,15]],"date-time":"2021-04-15T00:00:00Z","timestamp":1618444800000},"content-version":"unspecified","delay-in-days":104,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <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.1017\/s095679682100006x","type":"journal-article","created":{"date-parts":[[2021,4,15]],"date-time":"2021-04-15T05:01:12Z","timestamp":1618462872000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":5,"title":["StkTokens\n                    <i>: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities<\/i>"],"prefix":"10.1017","volume":"31","author":[{"given":"LAU","family":"SKORSTENGAARD","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3862-6856","authenticated-orcid":false,"given":"DOMINIQUE","family":"DEVRIESE","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"LARS","family":"BIRKEDAL","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2021,4,15]]},"reference":[{"key":"S095679682100006X_ref24","volume-title":"Capability-Based Computer Systems","author":"Levy","year":"1984"},{"key":"S095679682100006X_ref39","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00024"},{"key":"S095679682100006X_ref43","unstructured":"Watson, R. N. M. , Neumann, P. G. , Woodruff, J. , Roe, M. , Anderson, J. , Chisnall, D. , Davis, B. , Joannou, A. , Laurie, B. , Moore, S. W. , Murdoch, S. J. , Norton, R. & Son, S. (2015b) Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture. Technical report UCAM-CL-TR-876. University of Cambridge, Computer Laboratory."},{"key":"S095679682100006X_ref8","unstructured":"Ahmed, A. J. (2004) Semantics of Types for Mutable State. PhD thesis, Princeton University."},{"key":"S095679682100006X_ref27","volume-title":"Computer Security Foundations","author":"Patrignani","year":"2016"},{"key":"S095679682100006X_ref34","first-page":"5:1","article-title":"Reasoning about a machine with local capabilities: Provably safe stack and return pointer management","volume":"42","author":"Skorstengaard","year":"2019","journal-title":"ACM Trans. Program. Lang. Syst"},{"key":"S095679682100006X_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90027-5"},{"key":"S095679682100006X_ref5","volume-title":"Computer and Communications Security","author":"Abate","year":"2018"},{"key":"S095679682100006X_ref17","first-page":"1","article-title":"Modular, fully-abstract compilation by approximate back-translation","volume":"13","author":"Devriese","year":"2017","journal-title":"Logical Methods Comput. Sci."},{"key":"S095679682100006X_ref40","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134026"},{"key":"S095679682100006X_ref28","volume-title":"Computer Security Foundations","author":"Patrignani","year":"2017"},{"key":"S095679682100006X_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"S095679682100006X_ref19","doi-asserted-by":"crossref","unstructured":"Georges, A. L. , Gu\u00e9neau, A. , Van Strydonck, T. , Timany, A. , Trieu, A. , Huyghebaert, S. , Devriese, D. & Birkedal, L. (2021) Efficient and provable local capability revocation using uninitialized capabilities. Proc. ACM Program. Lang. 5(POPL), 6:1\u20136:30.","DOI":"10.1145\/3434287"},{"key":"S095679682100006X_ref13","unstructured":"Birkedal, L. & Bizjak, A. (2014) A Taste of Categorical Logic \u2014 Tutorial Notes."},{"key":"S095679682100006X_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/11576280_9"},{"key":"S095679682100006X_ref30","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1137\/0205037","article-title":"Data types as lattices","volume":"5","author":"Scott","year":"1976","journal-title":"SIAM J. Comput."},{"key":"S095679682100006X_ref36","doi-asserted-by":"publisher","DOI":"10.5210\/fm.v2i9.548"},{"key":"S095679682100006X_ref41","doi-asserted-by":"crossref","unstructured":"Van Strydonck, T. , Piessens, F. & Devriese, D. (2019) Linear capabilities for fully abstract compilation of separation-logic-verified code. Proc. ACM Program. Lang. ICFP. accepted.","DOI":"10.1145\/3342538"},{"key":"S095679682100006X_ref45","first-page":"20","volume-title":"IEEE Symposium on Security and Privacy","author":"Watson","year":"2015"},{"key":"S095679682100006X_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034830"},{"key":"S095679682100006X_ref3","first-page":"340","volume-title":"In Conference on Computer and Communications Security","author":"Abadi","year":"2005"},{"key":"S095679682100006X_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/3290332"},{"key":"S095679682100006X_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034831"},{"key":"S095679682100006X_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951941"},{"key":"S095679682100006X_ref46","unstructured":"Watson, R. N. , Neumann, P. G. , Woodruff, J. , Anderson, J. , Anderson, R. , Dave, N. , Laurie, B. , Moore, S. W. , Murdoch, S. J. , Paeps, P. , Roe, M. & Saidi, H. (2012) CHERI: A research platform deconflating hardware virtualization and protection. In Workshop on Runtime Environments, Systems, Layering and Virtualized Environments (RESoLVE)."},{"key":"S095679682100006X_ref20","doi-asserted-by":"crossref","unstructured":"Joannou, A. , Woodruff, J. , Kovacsics, R. , Moore, S. W. , Bradbury, A. , Xia, H. , Watson, R. N. M. , Chisnall, D. , Roe, M. , Davis, B. , Napierala, E. , Baldwin, J. , Gudka, K. , Neumann, P. G. , Mazzinghi, A. , Richardson, A. , Son, S. & Markettos, A. T. (2017) Efficient tagged memory. In IEEE International Conference on Computer Design (ICCD). IEEE.","DOI":"10.1109\/ICCD.2017.112"},{"key":"S095679682100006X_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48749-2_2"},{"key":"S095679682100006X_ref47","doi-asserted-by":"crossref","unstructured":"Woodruff, J. , Watson, R. N. , Chisnall, D. , Moore, S. W. , Anderson, J. , Davis, B. , Laurie, B. , Neumann, P. G. , Norton, R. & Roe, M. (2014) The CHERI capability model: Revisiting RISC in an age of risk. In International Symposium on Computer Architecuture. IEEE, pp. 457\u2013468.","DOI":"10.1109\/ISCA.2014.6853201"},{"key":"S095679682100006X_ref15","unstructured":"Carlini, N. , Barresi, A. , Payer, M. , Wagner, D. & Gross, T. R. (2015) Control-flow bending: On the effectiveness of control-flow integrity. In USENIX Security. USENIX Association."},{"key":"S095679682100006X_ref21","volume-title":"CSF","author":"Juglaret","year":"2016"},{"key":"S095679682100006X_ref29","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00066"},{"key":"S095679682100006X_ref18","volume-title":"Computer and Communications Security","author":"Evans","year":"2015"},{"key":"S095679682100006X_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.022"},{"key":"S095679682100006X_ref44","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2016.84"},{"key":"S095679682100006X_ref33","doi-asserted-by":"crossref","unstructured":"Skorstengaard, L. , Devriese, D. & Birkedal, L. (2018b) StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities. Technical Report with Proofs and Details.","DOI":"10.1145\/3290332"},{"key":"S095679682100006X_ref11","doi-asserted-by":"crossref","unstructured":"Azevedo de Amorim, A. , D\u00e9n\u00e8s, M. , Giannarakis, N. , Hritcu, C. , Pierce, B. C. , Spector-Zabusky, A. & Tolmach, A. (2015) Micro-policies: Formally verified, tag-based security monitors. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17\u201321, 2015, pp. 813\u2013830.","DOI":"10.1109\/SP.2015.55"},{"key":"S095679682100006X_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"S095679682100006X_ref6","doi-asserted-by":"crossref","unstructured":"Abate, C. , Blanco, R. , Garg, D. , Hritcu, C. , Patrignani, M. & Thibault, J. (2019) Journey beyond full abstraction: Exploring robust property preservation for secure compilation. In Computer Security Foundations Symposium. IEEE Computer Society Press.","DOI":"10.1109\/CSF.2019.00025"},{"key":"S095679682100006X_ref10","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-15784"},{"key":"S095679682100006X_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_17"},{"key":"S095679682100006X_ref12","unstructured":"Barthe, G. , Blazy, S. , Gr\u00e9goire, B. , Hutin, R. , Laporte, V. , Pichardie, D. & Trieu, A. (2019) Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4(POPL), 7:1\u20137:30."},{"key":"S095679682100006X_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926401"},{"key":"S095679682100006X_ref42","unstructured":"Watson, R. N. M. , Neumann, P. G. , Woodruff, J. , Roe, M. , Almatary, H. , Anderson, J. , Baldwin, J. , Barnes, G. , Chisnall, D. , Clarke, J. , Davis, B. , Eisen, L. , Filardo, N. W. , Grisenthwaite, R. , Joannou, A. , Laurie, B. , Markettos, A. T. , Moore, S. W. , Murdoch, S. J. , Nienhuis, K. , Norton, R. , Richardson, A. , Rugg, P. , Sewell, P. , Son, S. & Xia, H. (2020) Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8). Technical report UCAM-CL-TR-951. University of Cambridge, Computer Laboratory."},{"key":"S095679682100006X_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49255-0_70"},{"key":"S095679682100006X_ref22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0956796818000151","article-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic","volume":"28","author":"Jung","year":"2018","journal-title":"J. Funct. Program."},{"key":"S095679682100006X_ref37","unstructured":"Szabo, N. (2004) Scarce Objects."},{"key":"S095679682100006X_ref31","unstructured":"Skorstengaard, L. (2019) Formal Reasoning about Capability Machines. PhD thesis, Aarhus University."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S095679682100006X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:54Z","timestamp":1779835014000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S095679682100006X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"references-count":47,"alternative-id":["S095679682100006X"],"URL":"https:\/\/doi.org\/10.1017\/s095679682100006x","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}],"article-number":"e9"}}