{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:32:21Z","timestamp":1767929541742,"version":"3.49.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2019,12,10]],"date-time":"2019-12-10T00:00:00Z","timestamp":1575936000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"STSM"},{"name":"ModuRes Sapere Aude Advanced Grant from The Danish Council for Independent Research for the Natural Sciences"},{"name":"COST Action EUTypes","award":["CA15123"],"award-info":[{"award-number":["CA15123"]}]},{"DOI":"10.13039\/501100003130","name":"Research Foundation Flanders","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003130","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2020,3,31]]},"abstract":"<jats:p>Capability machines provide security guarantees at machine level which makes them an interesting target for secure compilation schemes that provably enforce properties such as control-flow correctness and encapsulation of local state. We provide a formalization of a representative capability machine with local capabilities and study a novel calling convention. We provide a logical relation that semantically captures the guarantees provided by the hardware (a form of capability safety) and use it to prove control-flow correctness and encapsulation of local state. The logical relation is not specific to our calling convention and can be used to reason about arbitrary programs.<\/jats:p>","DOI":"10.1145\/3363519","type":"journal-article","created":{"date-parts":[[2019,12,11]],"date-time":"2019-12-11T13:27:18Z","timestamp":1576070838000},"page":"1-53","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Reasoning about a Machine with Local Capabilities"],"prefix":"10.1145","volume":"42","author":[{"given":"Lau","family":"Skorstengaard","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3862-6856","authenticated-orcid":false,"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Brussel, Pleinlaan, Elsene, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,12,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49255-0_70"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102165"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Amal Ahmed Derek Dreyer and Andreas Rossberg. 2009. State-dependent representation independence. In Principles of Programming Languages. ACM 340--353.","DOI":"10.1145\/1594834.1480925"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90027-5"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_2_1_8_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2014. A Taste of Categorical Logic - Tutorial Notes. http:\/\/cs.au.dk\/&sim;birke\/modures\/tutorial\/categorical-logic-tutorial-notes.pdf."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"Lars Birkedal Bernhard Reus Jan Schwinghammer Kristian St\u00f8vring Jacob Thamsborg and Hongseok Yang. 2011. Step-indexed kripke models over recursive worlds. In Principles of Programming Languages. ACM 119--132. DOI:https:\/\/doi.org\/10.1145\/1926385.1926401","DOI":"10.1145\/1926385.1926401"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"e_1_2_1_11_1","volume-title":"Some Theorems about Mutually Recursive Domain Equations in the Category of Preordered COFEs. (Feb","author":"Bizjak Ale\u0161","year":"2017","unstructured":"Ale\u0161 Bizjak. 2017. Some Theorems about Mutually Recursive Domain Equations in the Category of Preordered COFEs. (Feb. 2017). Manuscript. Available at http:\/\/alesb.com\/documents\/notes\/mutually-recursive-domain-eq.pdf."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/195473.195579"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037725"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_2_1_15_1","volume-title":"European Symposium on Security and Privacy. IEEE.","author":"Devriese Dominique","year":"2016","unstructured":"Dominique Devriese, Lars Birkedal, and Frank Piessens. 2016. Reasoning about object capabilities using logical relations and effect parametricity. In European Symposium on Security and Privacy. IEEE."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_2_1_17_1","volume-title":"A Formal Model for Capability Machines: An Illustrative Case Study towards Secure Compilation to CHERI.Master\u2019s thesis","author":"El-Korashy Akram","unstructured":"Akram El-Korashy. 2016. A Formal Model for Capability Machines: An Illustrative Case Study towards Secure Compilation to CHERI.Master\u2019s thesis. Saarland University. https:\/\/people.mpi-sws.org\/ elkorashy\/files\/Thesis.pdf."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/HOTOS.1997.595185"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"Chung-Kil Hur and Derek Dreyer. 2011. A Kripke logical relation between ML and assembly. In Principles of Programming Languages. ACM 133--146. DOI:https:\/\/doi.org\/10.1145\/1926385.1926402","DOI":"10.1145\/1926385.1926402"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2017.112"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.11"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_23_1","volume-title":"Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Principles of Programming Languages. ACM, 637--650.","author":"Jung Ralf","year":"2015","unstructured":"Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Principles of Programming Languages. ACM, 637--650."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017b. Interactive proofs in higher-order concurrent separation logic. In Principles of Programming Languages. ACM.","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)90047-7"},{"key":"e_1_2_1_27_1","volume-title":"Capability-based Computer Systems","author":"Levy Henry M.","unstructured":"Henry M. Levy. 1984. Capability-based Computer Systems. Vol. 12. Digital Press Bedford."},{"key":"e_1_2_1_28_1","unstructured":"Tim Lindholm Frank Yellin Gilad Bracha and Alex Buckley. 2014. The Java Virtual Machine Specification. Pearson Education."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.16"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_2_1_31_1","unstructured":"Zhaozhong Ni and Zhong Shao. 2006. Certified assembly programming with embedded code pointers. In Principles of Programming Languages. ACM."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","unstructured":"Leo Osvald Gr\u00e9gory Essertel Xilun Wu Lilliam I. Gonz\u00e1lez Alay\u00f3n and Tiark Rompf. 2016. Gentrification gone too far? Affordable 2Nd-class values for fun and (co-)effect. In Object-Oriented Programming Systems Languages and Applications. ACM 234--251. DOI:https:\/\/doi.org\/10.1145\/2983990.2984009","DOI":"10.1145\/2983990.2984009"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.9"},{"key":"e_1_2_1_35_1","volume-title":"Stark","author":"Pitts Andrew M.","year":"1998","unstructured":"Andrew M. Pitts and Ian D. B. Stark. 1998. Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics, Andrew D. Gordon and Andrew M. Pitts (Eds.). Cambridge University Press, 227--274."},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Thomas Sewell Simon Winwood Peter Gammie Toby Murray June Andronick and Gerwin Klein. 2011. seL4 enforces integrity. In Interactive Theorem Proving Marko van Eekelen Herman Geuvers Julien Schmaltz and Freek Wiedijk (Eds.). Springer Berlin 325--340.","DOI":"10.1007\/978-3-642-22863-6_24"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/319151.319163"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_17"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290332"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","unstructured":"David Swasey Deepak Garg and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. In OOPSLA. ACM. DOI:https:\/\/doi.org\/10.1145\/3133913","DOI":"10.1145\/3133913"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.13"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034831"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/168619.168635"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2014.6853201"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3363519","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3363519","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:25Z","timestamp":1750203865000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3363519"}},"subtitle":["Provably Safe Stack and Return Pointer Management"],"short-title":[],"issued":{"date-parts":[[2019,12,10]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,3,31]]}},"alternative-id":["10.1145\/3363519"],"URL":"https:\/\/doi.org\/10.1145\/3363519","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,10]]},"assertion":[{"value":"2018-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-12-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}