{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T15:43:15Z","timestamp":1783438995794,"version":"3.54.6"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,17]],"date-time":"2024-04-17T00:00:00Z","timestamp":1713312000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Digital Security by Design (DSbD)","award":["105694)."],"award-info":[{"award-number":["105694)."]}]},{"name":"Horizon 2020 research and innovation programme","award":["789108"],"award-info":[{"award-number":["789108"]}]},{"name":"DARPA","award":["HR0011-22-C-0110"],"award-info":[{"award-number":["HR0011-22-C-0110"]}]},{"name":"AFRL","award":["HR0011-23- C-0031"],"award-info":[{"award-number":["HR0011-23- C-0031"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,27]]},"DOI":"10.1145\/3617232.3624859","type":"proceedings-article","created":{"date-parts":[[2024,4,17]],"date-time":"2024-04-17T20:10:56Z","timestamp":1713384656000},"page":"181-196","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9145-3288","authenticated-orcid":false,"given":"Vadim","family":"Zaliva","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3723-636X","authenticated-orcid":false,"given":"Kayvan","family":"Memarian","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1667-1683","authenticated-orcid":false,"given":"Ricardo","family":"Almeida","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, Scotland Uk"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8157-5567","authenticated-orcid":false,"given":"Jessica","family":"Clarke","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-6256-0419","authenticated-orcid":false,"given":"Brooks","family":"Davis","sequence":"additional","affiliation":[{"name":"SRI International, Menlo Park, California, United States of America"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6372-217X","authenticated-orcid":false,"given":"Alexander","family":"Richardson","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6060-0153","authenticated-orcid":false,"given":"David","family":"Chisnall","sequence":"additional","affiliation":[{"name":"Microsoft, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6941-5034","authenticated-orcid":false,"given":"Brian","family":"Campbell","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, Scotland Uk"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6800-812X","authenticated-orcid":false,"given":"Ian","family":"Stark","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, Scotland Uk"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8139-8783","authenticated-orcid":false,"given":"Robert N. M.","family":"Watson","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9352-1013","authenticated-orcid":false,"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,17]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"CHERI x86-64 Sail model. https:\/\/github.com\/CTSRD-CHERI\/sail-cheri-x86. Accessed 2023-04-17."},{"key":"e_1_3_2_1_2_1","first-page":"96","volume-title":"USENIX Security Symposium","volume":"10","author":"Akritidis Periklis","year":"2009","unstructured":"Periklis Akritidis, Manuel Costa, Miguel Castro, and Steven Hand. Baggy bounds checking: An efficient and backwards-compatible defense against out-of-bounds errors. In USENIX Security Symposium, volume 10, page 96, 2009."},{"key":"e_1_3_2_1_4_1","volume-title":"Arm Morello Program. https:\/\/developer.arm.com\/architectures\/cpu-architecture\/a-profile\/morello","year":"2022","unstructured":"Arm. Arm Morello Program. https:\/\/developer.arm.com\/architectures\/cpu-architecture\/a-profile\/morello, 2022. Accessed 2021-06-29."},{"key":"e_1_3_2_1_5_1","first-page":"2022","volume-title":"June","author":"Ltd Arm","year":"2021","unstructured":"Arm Ltd. Arm\u00ae architecture reference manual supplement Morello for A-profile architecture. https:\/\/developer.arm.com\/documentation\/ddi0606\/latest, June 2021. DDI0606A.j. 1288pp. Accessed 2022-06-15."},{"key":"e_1_3_2_1_6_1","volume-title":"November","author":"Ltd Arm","year":"2022","unstructured":"Arm Ltd. Arm Morello program, landing page for Morello open source software. https:\/\/www.morello-project.org\/, November 2022."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8\\_7"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3543289"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1298455.1298470"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762221"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304042"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/356571.356573"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1346281.1346295"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1133999"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSREW.2012.24"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00098"},{"key":"e_1_3_2_1_18_1","volume-title":"Victor BF Gomes, and Martin Uecker. A Provenance-aware Memory Object Model for C","author":"Gustedt Jens","year":"2022","unstructured":"Jens Gustedt, Peter Sewell, Kayvan Memarian, Victor BF Gomes, and Martin Uecker. A Provenance-aware Memory Object Model for C, 2022. Working draft ISO Technical Specification TS6010."},{"key":"e_1_3_2_1_19_1","volume-title":"0day in the wild","author":"Hawkes Ben","year":"2019","unstructured":"Ben Hawkes. 0day in the wild. 2019. Project Zero team blog, Google. https:\/\/googleprojectzero.blogspot.com\/p\/0day.html. Accessed 2023-04-19."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591257"},{"key":"e_1_3_2_1_21_1","volume-title":"ISO\/IEC 9899:2018 edition","author":"ISO","year":"2018","unstructured":"ISO WG14. Programming languages - C, ISO\/IEC 9899:2018 edition, July 2018."},{"key":"e_1_3_2_1_22_1","first-page":"13","volume-title":"AADEBUG","volume":"97","author":"Jones Richard WM","year":"1997","unstructured":"Richard WM Jones and Paul HJ Kelly. Backwards-compatible bounds checking for arrays and pointers in C programs. In AADEBUG, volume 97, pages 13--26, 1997."},{"key":"e_1_3_2_1_23_1","volume-title":"Lattner and Vikram Adve. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04)","author":"Chris","year":"2004","unstructured":"Chris Lattner and Vikram Adve. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04), Palo Alto, California, Mar 2004."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9\\_38"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_3_2_1_29_1","volume-title":"February","author":"Miller Matt","year":"2019","unstructured":"Matt Miller. Trends, challenge, and shifts in software vulnerability mitigation. https:\/\/github.com\/Microsoft\/MSRC-Security-Research\/tree\/master\/presentations\/2019_02_BlueHatIL, February 2019. Microsoft Security Response Center."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542504"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503286"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250746"},{"key":"e_1_3_2_1_33_1","first-page":"1","volume-title":"TPHOLs","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle\/HOL: A proof assistant for higher-order logic. In TPHOLs, pages 1--18. Springer, 2002."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_28"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345137"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17138-4\\_4"},{"key":"e_1_3_2_1_38_1","first-page":"159","volume-title":"NDSS","volume":"2004","author":"Ruwase Olatunji","year":"2004","unstructured":"Olatunji Ruwase and Monica S Lam. A practical dynamic buffer over-flow detector. In NDSS, volume 2004, pages 159--169, 2004."},{"key":"e_1_3_2_1_39_1","volume-title":"USENIX","author":"Serebryany Konstantin","year":"2012","unstructured":"Konstantin Serebryany and Timur Iskhodzhanov. AddressSanitizer: A fast address sanity checker. In Presented as part of the 2012 USENIX Annual Technical Conference (ATC 12), pages 309--318. USENIX, 2012."},{"key":"e_1_3_2_1_40_1","volume-title":"2005 USENIX Annual Technical Conference (USENIX ATC 05)","author":"Seward Julian","year":"2005","unstructured":"Julian Seward and Nicholas Nethercote. Using Valgrind to detect undefined value errors with Bit-Precision. In 2005 USENIX Annual Technical Conference (USENIX ATC 05), Anaheim, CA, April 2005. USENIX Association. URL: https:\/\/www.usenix.org\/conference\/2005-usenix-annual-technical-conference\/using-valgrind-detect-undefined-value-errors-bit."},{"key":"e_1_3_2_1_41_1","volume-title":"https:\/\/www.dsbd.tech\/ and https:\/\/www.ukri.org\/our-work\/our-main-funds\/industrial-strategy-challenge-fund\/artificial-intelligence-and-data-economy\/digital-security-by-design-challenge\/","author":"UKRI.","year":"2022","unstructured":"UKRI. Digital security by design. https:\/\/www.dsbd.tech\/ and https:\/\/www.ukri.org\/our-work\/our-main-funds\/industrial-strategy-challenge-fund\/artificial-intelligence-and-data-economy\/digital-security-by-design-challenge\/, 2022. Accessed 2021-06-29."},{"key":"e_1_3_2_1_42_1","unstructured":"Robert N. M. Watson Ben Laurie and Alexander Richardson. Assessing the Viability of an Open- Source CHERI Desktop Software Ecosystem. http:\/\/www.capabilitieslimited.co.uk\/pdfs\/20210917-capltd-cheri-desktop-report-version1-FINAL.pdf September 2021."},{"key":"e_1_3_2_1_43_1","volume-title":"Richard Grisenthwaite, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis","author":"Watson Robert N. M.","unstructured":"Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, Graeme Barnes, David Chisnall, Jessica Clarke, Brooks Davis, Lee Eisen, Nathaniel Wesley Filardo, Richard Grisenthwaite, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert Norton, Alexander Richardson, Peter Rugg, Peter Sewell, Stacey Son, and Hongyan Xia. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 9 - DRAFT). Accessed 2023-04-12. URL: https:\/\/github.com\/CTSRD-CHERI\/cheri-specification."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-951"},{"key":"e_1_3_2_1_46_1","volume-title":"Defect report","year":"2004","unstructured":"WG14. Defect report 260, September 2004. http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/dr_260.htm."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2019.2914037"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2014.6853201"}],"event":{"name":"ASPLOS '24: 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1","location":"La Jolla CA USA","acronym":"ASPLOS '24","sponsor":["SIGARCH ACM Special Interest Group on Computer Architecture","SIGOPS ACM Special Interest Group on Operating Systems","SIGPLAN ACM Special Interest Group on Programming Languages","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3617232.3624859","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3617232.3624859","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3617232.3624859","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:14Z","timestamp":1750178774000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3617232.3624859"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,17]]},"references-count":43,"alternative-id":["10.1145\/3617232.3624859","10.1145\/3617232"],"URL":"https:\/\/doi.org\/10.1145\/3617232.3624859","relation":{},"subject":[],"published":{"date-parts":[[2024,4,17]]},"assertion":[{"value":"2024-04-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}