{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T10:08:06Z","timestamp":1781258886083,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Digital Security by De- sign (DSbD)","award":["105694"],"award-info":[{"award-number":["105694"]}]},{"name":"European Research Council","award":["grant agreement No 789108, ERC AdG ELVER"],"award-info":[{"award-number":["grant agreement No 789108, ERC AdG ELVER"]}]},{"name":"UK Research and Innovation","award":["ERC-AdG-2022, EP\\\/Y035976\\\/1 SAFER"],"award-info":[{"award-number":["ERC-AdG-2022, EP\\\/Y035976\\\/1 SAFER"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705878","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"112-126","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A CHERI C Memory Model for Verified Temporal Safety"],"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\/0000-0001-6941-5034","authenticated-orcid":false,"given":"Brian","family":"Campbell","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, 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, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-9698-1503","authenticated-orcid":false,"given":"Nathaniel","family":"Filardo","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"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, 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":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"Ricardo Almeida et al. 2024. coq-cheri-capabilities library. GitHub repository. https:\/\/github.com\/rems-project\/coq-cheri-capabilities Accessed 2024-09-13."},{"key":"e_1_3_2_2_2_1","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_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3613424.3614266"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674652"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_24"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_5"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_6"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3543289"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304042"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-961"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640416"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00098"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527318"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2023.3264676"},{"key":"e_1_3_2_2_16_1","volume-title":"Victor BF Gomes, and Martin Uecker","author":"Gustedt Jens","year":"2022","unstructured":"Jens Gustedt, Peter Sewell, Kayvan Memarian, Victor BF Gomes, and Martin Uecker. 2022. A Provenance-aware Memory Object Model for C. Working draft ISO Technical Specification TS6010."},{"key":"e_1_3_2_2_17_1","unstructured":"Ben Hawkes. 2019. 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_2_18_1","volume-title":"Steven Keuchel, and Dominique Devriese.","author":"Huyghebaert Sander","year":"2020","unstructured":"Sander Huyghebaert, Thomas Van Strydonck, Steven Keuchel, and Dominique Devriese. 2020. Uninitialized Capabilities. arxiv:2006.01608 [cs.PL] https:\/\/arxiv.org\/abs\/2006.01608"},{"key":"e_1_3_2_2_19_1","first-page":"2018","article-title":"Programming Languages \u2013 C","volume":"9899","author":"International Organization for Standardization.","year":"2018","unstructured":"International Organization for Standardization. 2018. Programming Languages \u2013 C. International Standard 9899:2018. ISO\/IEC, Geneva, Switzerland.","journal-title":"International Standard"},{"key":"e_1_3_2_2_20_1","unstructured":"Nicolas Joly Saif ElSherei and Saar Amar. 2020. Security Analysis of CHERI ISA. Technical Report. Microsoft Security Response Center. https:\/\/github.com\/microsoft\/MSRC-Security-Research\/blob\/master\/papers\/2020\/Security"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738005"},{"key":"e_1_3_2_2_22_1","volume-title":"The C Standard Formalized in Coq. Ph. D. Dissertation","author":"Krebbers Robbert Jan","unstructured":"Robbert Jan Krebbers. 2015. The C Standard Formalized in Coq. Ph. D. Dissertation. Radboud University, Nijmegen, Netherlands."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_22"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276495"},{"key":"e_1_3_2_2_25_1","unstructured":"Xavier Leroy Andrew W. Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert Memory Model Version 2. Research report RR-7987. INRIA. http:\/\/hal.inria.fr\/hal-00703441"},{"key":"e_1_3_2_2_26_1","unstructured":"Gregory Malecha et al. 2012. ExtLib Coq library. GitHub repository. https:\/\/github.com\/coq-ext-lib\/coq-ext-lib Accessed: 2024-09-11."},{"key":"e_1_3_2_2_27_1","unstructured":"Kayvan Memarian. 2023. The Cerberus C semantics. Technical Report UCAM-CL-TR-981. University of Cambridge Computer Laboratory. 10.48456\/tr-981"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806651.1806657"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983997"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_28"},{"key":"e_1_3_2_2_32_1","unstructured":"Alex Rebert and Christoph Kern. 2024. Secure by Design: Google\u2019s Perspective on Memory Safety. Technical Report. Google Security Engineering. https:\/\/research.google\/pubs\/secure-by-design-googles-perspective-on-memory-safety\/"},{"key":"e_1_3_2_2_33_1","unstructured":"CWE Team. 2023. CWE Top 25 Most Dangerous Software Weaknesses. https:\/\/cwe.mitre.org\/top25\/index.html Access: 2024-09-14."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00024"},{"key":"e_1_3_2_2_35_1","unstructured":"Robert N. M. Watson Ben Laurie and Alex Richardson. 2021. Assessing the Viability of an Open-Source CHERI Desktop Software Ecosystem. Technical Report. Capabilities Limited. https:\/\/www.cl.cam.ac.uk\/research\/security\/ctsrd\/pdfs\/20210917-capltd-cheri-desktop-report-version1-FINAL.pdf"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-941"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-987"},{"key":"e_1_3_2_2_38_1","unstructured":"WG14. 2004. Defect Report 260. http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/dr_260.htm."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2014.6853201"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358288"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3617232.3624859"}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Denver CO USA","acronym":"CPP '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"]},"container-title":["Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705878","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705878","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:08Z","timestamp":1750295888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705878"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":42,"alternative-id":["10.1145\/3703595.3705878","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705878","relation":{},"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}