{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:07Z","timestamp":1780994707707,"version":"3.54.1"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,2,11]],"date-time":"2024-02-11T00:00:00Z","timestamp":1707609600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Villum Investigator","award":["25804"],"award-info":[{"award-number":["25804"]}]},{"name":"Center for Basic Research in Program Verification"},{"DOI":"10.13039\/100008398","name":"VILLUM Foundation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Research Foundation - Flanders"},{"name":"DFF","award":["6108-00363"],"award-info":[{"award-number":["6108-00363"]}]},{"name":"The Danish Council for Independent Research for the Natural Sciences"},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-21-1-0054"],"award-info":[{"award-number":["FA9550-21-1-0054"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Research Fund KU\u00a0Leuven"},{"name":"Flemish Research Programme Cybersecurity"},{"name":"Research Foundation - Flanders"},{"DOI":"10.13039\/501100003130","name":"Flemish Research Foundation","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":["J. ACM"],"published-print":{"date-parts":[[2024,2,29]]},"abstract":"<jats:p>\n            A capability machine is a type of CPU allowing fine-grained privilege separation using\n            <jats:italic>capabilities<\/jats:italic>\n            , machine words that represent certain kinds of authority. We present a mathematical model and accompanying proof methods that can be used for formal verification of functional correctness of programs running on a capability machine, even when they invoke and are invoked by unknown (and possibly malicious) code. We use a program logic called Cerise for reasoning about known code, and an associated logical relation, for reasoning about unknown code. The logical relation formally captures the capability safety guarantees provided by the capability machine. The Cerise program logic, logical relation, and all the examples considered in the paper have been mechanized using the Iris program logic framework in the Coq proof assistant.\n          <\/jats:p>\n          <jats:p>\n            The methodology we present underlies recent work of the authors on formal reasoning about capability machines\u00a0[Georges et\u00a0al.\n            <jats:xref ref-type=\"bibr\">2021<\/jats:xref>\n            ; Skorstengaard et\u00a0al.\n            <jats:xref ref-type=\"bibr\">2019a<\/jats:xref>\n            ; Van Strydonck et\u00a0al.\n            <jats:xref ref-type=\"bibr\">2022<\/jats:xref>\n            ], but was left somewhat implicit in those publications. In this paper we present a pedagogical introduction to the methodology, in a simpler setting (no exotic capabilities), and starting from minimal examples. We work our way up to new results about a heap-based calling convention and implementations of sophisticated object-capability patterns of the kind previously studied for high-level languages with object-capabilities, demonstrating that the methodology scales to such reasoning.\n          <\/jats:p>","DOI":"10.1145\/3623510","type":"journal-article","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:32:37Z","timestamp":1694701957000},"page":"1-59","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code"],"prefix":"10.1145","volume":"71","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5951-4642","authenticated-orcid":false,"given":"A\u00efna Linn","family":"Georges","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3072-4045","authenticated-orcid":false,"given":"Arma\u00ebl","family":"Gu\u00e9neau","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire M\u00e9thodes Formelles, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5262-1381","authenticated-orcid":false,"given":"Thomas","family":"Van Strydonck","sequence":"additional","affiliation":[{"name":"imec-Distrinet, KU Leuven, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","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-0002-3862-6856","authenticated-orcid":false,"given":"Dominique","family":"Devriese","sequence":"additional","affiliation":[{"name":"imec-Distrinet, KU Leuven, Belgium"}],"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":[[2024,2,11]]},"reference":[{"key":"e_1_3_4_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1998.705669"},{"key":"e_1_3_4_3_1","volume-title":"CHERIoT: Rethinking Security for Low-cost Embedded Systems","author":"Amar Saar","year":"2023","unstructured":"Saar Amar, Tony Chen, David Chisnall, Felix Domke, Nathaniel Filardo, Kunyan Liu, Robert Norton-Wright, Yucong Tao, Robert N. M. Watson, and Hongyan Xia. 2023. CHERIoT: Rethinking Security for Low-cost Embedded Systems. Technical Report MSR-TR-2023-6. Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/cheriot-rethinking-security-for-low-cost-embedded-systems\/"},{"key":"e_1_3_4_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/129099"},{"key":"e_1_3_4_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_4_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_7"},{"key":"e_1_3_4_7_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2022. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. https:\/\/iris-project.org\/tutorial-pdfs\/iris-lecture-notes.pdf. (2022). [Online; accessed 26-May-2023]."},{"key":"e_1_3_4_8_1","article-title":"A multipurpose formal RISC-V specification","author":"Bourgeat Thomas","year":"2021","unstructured":"Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Andrew Wright, and Adam Chlipala. 2021. A multipurpose formal RISC-V specification. arXiv:2104.00762 [cs] (April2021). arxiv:cs\/2104.00762. http:\/\/arxiv.org\/abs\/2104.00762","journal-title":"arXiv:2104.00762 [cs]"},{"key":"e_1_3_4_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/195473.195579"},{"key":"e_1_3_4_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037725"},{"key":"e_1_3_4_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_3_4_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.22"},{"key":"e_1_3_4_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_3_4_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00036"},{"key":"e_1_3_4_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00098"},{"key":"e_1_3_4_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"e_1_3_4_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527318"},{"key":"e_1_3_4_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3616602"},{"key":"e_1_3_4_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_4_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_4_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547628"},{"key":"e_1_3_4_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_4_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/538134"},{"key":"e_1_3_4_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591279"},{"key":"e_1_3_4_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2017.2647955"},{"key":"e_1_3_4_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586043"},{"key":"e_1_3_4_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_4_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00055"},{"key":"e_1_3_4_29_1","volume-title":"Complete Spatial Safety for C and C++ Using CHERI Capabilities","author":"Richardson Alexander","year":"2020","unstructured":"Alexander Richardson. 2020. Complete Spatial Safety for C and C++ Using CHERI Capabilities. Ph.D. Dissertation. University of Cambridge, Computer Laboratory. https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-949.html"},{"key":"e_1_3_4_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371100"},{"key":"e_1_3_4_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_3_4_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_4_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_17"},{"key":"e_1_3_4_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3363519"},{"key":"e_1_3_4_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290332"},{"key":"e_1_3_4_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964015"},{"key":"e_1_3_4_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_3_4_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919645"},{"key":"e_1_3_4_39_1","volume-title":"8th IEEE European Symposium on Security and Privacy, EuroS&P 2023, Delft, The Netherlands, July 3\u20137, 2023","author":"Strydonck Thomas Van","year":"2023","unstructured":"Thomas Van Strydonck, Job Noorman, Jennifer Jackson, Leonardo Alves Dias, Robin Vanderstraeten, David Oswald, Frank Piessens, and Dominique Devriese. 2023. CHERI-TrEE: Flexible enclaves on capability machines. In 8th IEEE European Symposium on Security and Privacy, EuroS&P 2023, Delft, The Netherlands, July 3\u20137, 2023. IEEE. https:\/\/people.cs.kuleuven.be\/thomas.vanstrydonck\/cheri-tree-preprint.pdf. Accepted for publication."},{"key":"e_1_3_4_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341688"},{"key":"e_1_3_4_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_3_4_42_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-951"},{"key":"e_1_3_4_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2016.84"},{"key":"e_1_3_4_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2019.2914037"},{"key":"e_1_3_4_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358288"},{"key":"e_1_3_4_46_1","volume-title":"32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 09\u201311, 2023","author":"Yu Jason Zhijingcheng","year":"2023","unstructured":"Jason Zhijingcheng Yu, Conrad Watt, Aditya Badole, Trevor E. Carlson, and Prateek Saxena. 2023. Capstone: A capability-based foundation for trustless secure memory access. In 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 09\u201311, 2023, Joe Calandrino and Carmela Troncoso (Eds.). USENIX Association. https:\/\/www.usenix.org\/conference\/usenixsecurity23\/presentation\/yujason"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623510","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3623510","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3623510","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:36Z","timestamp":1750287036000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623510"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2,11]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,2,29]]}},"alternative-id":["10.1145\/3623510"],"URL":"https:\/\/doi.org\/10.1145\/3623510","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,2,11]]},"assertion":[{"value":"2021-10-03","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-08-25","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-02-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}