{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:56Z","timestamp":1780994696072,"version":"3.54.1"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,4,29]]},"abstract":"<jats:p>\n            Capability machines are a type of CPUs that support fine-grained privilege separation using\n            <jats:italic>capabilities<\/jats:italic>\n            , machine words that include forms of authority. Formal models of capability machines and associated calling conventions have so far focused on establishing two forms of stack safety properties, namely local state encapsulation and well-bracketed control flow. We introduce a novel kind of\n            <jats:italic>directed<\/jats:italic>\n            capabilities and show how to use them to make an earlier suggested calling convention more efficient. In contrast to earlier work on capability machine models we do not only consider integrity properties but also confidentiality properties; we provide a unary logical relation to reason about the former and a binary logical relation to reason about the latter, each expressive enough to reason about temporal stack safety. While the logical relations are useful for reasoning about concrete examples, they do not on their own demonstrate that stack safety holds for a large class of programs. Therefore, we also show full abstraction of a compiler from an overlay semantics that internalizes the calling convention as a single call step and explicitly keeps track of the call stack and frame lifetimes to a base capability machine. All results have been mechanized in Coq.\n          <\/jats:p>","DOI":"10.1145\/3527318","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5951-4642","authenticated-orcid":false,"given":"A\u00efna Linn","family":"Georges","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8239-8125","authenticated-orcid":false,"given":"Alix","family":"Trieu","sequence":"additional","affiliation":[{"name":"ANSSI, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48749-2_2"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243745"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_2_2_5_1","volume-title":"Security Properties for Stack Safety. CoRR, abs\/2105.00417","author":"Anderson Sean Noble","year":"2021","unstructured":"Sean Noble Anderson , Leonidas Lampropoulos , Roberto Blanco , Benjamin C. Pierce , and Andrew Tolmach . 2021. Security Properties for Stack Safety. CoRR, abs\/2105.00417 ( 2021 ), arxiv:2105.00417. arxiv:2105.00417 Sean Noble Anderson, Leonidas Lampropoulos, Roberto Blanco, Benjamin C. Pierce, and Andrew Tolmach. 2021. Security Properties for Stack Safety. CoRR, abs\/2105.00417 (2021), arxiv:2105.00417. arxiv:2105.00417"},{"key":"e_1_2_2_6_1","unstructured":"Arm. 2021. Morello project. https:\/\/www.morello-project.org\/  Arm. 2021. Morello project. https:\/\/www.morello-project.org\/"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535839"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.55"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_4"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_7"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926401"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/195473.195579"},{"key":"e_1_2_2_13_1","unstructured":"Chromium. 2020. Memory safety. https:\/\/www.chromium.org\/Home\/chromium-security\/memory-safety  Chromium. 2020. Memory safety. https:\/\/www.chromium.org\/Home\/chromium-security\/memory-safety"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.22"},{"key":"e_1_2_2_16_1","volume-title":"Logical Step-Indexed Logical Relations. LMCS, 7, 2:16","author":"Dreyer Derek","year":"2011","unstructured":"Derek Dreyer , Amal Ahmed , and Lars Birkedal . 2011. Logical Step-Indexed Logical Relations. LMCS, 7, 2:16 ( 2011 ), June, 1\u201337. Derek Dreyer, Amal Ahmed, and Lars Birkedal. 2011. Logical Step-Indexed Logical Relations. LMCS, 7, 2:16 (2011), June, 1\u201337."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863566"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706323"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00036"},{"key":"e_1_2_2_20_1","volume-title":"Alexander Richardson, John Baldwin, David Chisnall, Jessica Clarke, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo Mazzinghi","author":"Filardo Nathaniel Wesley","unstructured":"Nathaniel Wesley Filardo , Brett F. Gutstein , Jonathan Woodruff , Sam Ainsworth , Lucian Paul-Trifu , Brooks Davis , Hongyan Xia , Edward Tomasz Napierala , Alexander Richardson, John Baldwin, David Chisnall, Jessica Clarke, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo Mazzinghi , Robert M. Norton , Michael Roe , Peter Sewell, Stacey Son, Timothy M. Jones, Simon W. Moore, Peter G. Neumann, and Robert N. M. Watson. 2020. Cornucopia: Temporal Safety for CHERI Heaps. In IEEE Symposium on Security and Privacy. IEEE. Nathaniel Wesley Filardo, Brett F. Gutstein, Jonathan Woodruff, Sam Ainsworth, Lucian Paul-Trifu, Brooks Davis, Hongyan Xia, Edward Tomasz Napierala, Alexander Richardson, John Baldwin, David Chisnall, Jessica Clarke, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Alfredo Mazzinghi, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, Timothy M. Jones, Simon W. Moore, Peter G. Neumann, and Robert N. M. Watson. 2020. Cornucopia: Temporal Safety for CHERI Heaps. In IEEE Symposium on Security and Privacy. IEEE."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5821862"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"A\u00efna Linn Georges Alix Trieu and Lars Birkedal. 2022. Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities. https:\/\/cs.au.dk\/~ageorges\/publications_pdfs\/monotone-technical.pdf  A\u00efna Linn Georges Alix Trieu and Lars Birkedal. 2022. Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities. https:\/\/cs.au.dk\/~ageorges\/publications_pdfs\/monotone-technical.pdf","DOI":"10.1145\/3527318"},{"key":"e_1_2_2_25_1","unstructured":"Nicolas Joly Saif ElSherei and Saar Amar. 2020. Security Analysis of CHERI ISA. https:\/\/msrc-blog.microsoft.com\/2020\/10\/14\/security-analysis-of-cheri-isa\/  Nicolas Joly Saif ElSherei and Saar Amar. 2020. Security Analysis of CHERI ISA. https:\/\/msrc-blog.microsoft.com\/2020\/10\/14\/security-analysis-of-cheri-isa\/"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_29_1","volume-title":"Isolation Without Taxation: Near Zero Cost Transitions for SFI. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM.","author":"Kolosick Matthew","year":"2022","unstructured":"Matthew Kolosick , Shravan Narayan , Conrad Watt , Michael LeMay , Deepak Garg , Ranjit Jhala , and Deian Stefan . 2022 . Isolation Without Taxation: Near Zero Cost Transitions for SFI. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM. Matthew Kolosick, Shravan Narayan, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, and Deian Stefan. 2022. Isolation Without Taxation: Near Zero Cost Transitions for SFI. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009877"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_2_35_1","volume-title":"Capability-Based Computer Systems","author":"Levy Henry M.","unstructured":"Henry M. Levy . 1984. Capability-Based Computer Systems . Digital Press . isbn:978-1-4831-0106-4 https:\/\/homes.cs.washington.edu\/~levy\/capabook\/ Henry M. Levy. 1984. Capability-Based Computer Systems. Digital Press. isbn:978-1-4831-0106-4 https:\/\/homes.cs.washington.edu\/~levy\/capabook\/"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00055"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00066"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_17"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3363519"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290332"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1284320.1284325"},{"key":"e_1_2_2_44_1","doi-asserted-by":"crossref","unstructured":"David Swasey Deepak Garg and Derek Dreyer. 2017. Robust and Compositional Verification of Object Capability Patterns. In OOPSLA. ACM. https:\/\/people.mpi-sws.org\/~swasey\/papers\/ocpl\/ocpl-20170418.pdf  David Swasey Deepak Garg and Derek Dreyer. 2017. Robust and Compositional Verification of Object Capability Patterns. In OOPSLA. ACM. https:\/\/people.mpi-sws.org\/~swasey\/papers\/ocpl\/ocpl-20170418.pdf","DOI":"10.1145\/3133913"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.13"},{"key":"e_1_2_2_46_1","unstructured":"Gavin Thomas. 2019. A proactive approach to more secure code. https:\/\/msrc-blog.microsoft.com\/2019\/07\/16\/a-proactive-approach-to-more-secure-code\/  Gavin Thomas. 2019. A proactive approach to more secure code. https:\/\/msrc-blog.microsoft.com\/2019\/07\/16\/a-proactive-approach-to-more-secure-code\/"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00024"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000022"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/168619.168635"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-951"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2019.2914037"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358288"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527318","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527318","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:53Z","timestamp":1750191533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527318"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":52,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527318"],"URL":"https:\/\/doi.org\/10.1145\/3527318","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}