{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:17:57Z","timestamp":1784233077016,"version":"3.55.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    CHERI-C extends the C programming language by adding\n                    <jats:italic>hardware capabilities<\/jats:italic>\n                    , ensuring a certain degree of memory safety while remaining efficient. Capabilities can also be employed for higher-level security measures, such as software compartmentalization, that have to be used correctly to achieve the desired security guarantees. As the extension changes the semantics of C, new theories and tooling are required to reason about CHERI-C code and verify correctness. In this work, we present a formal memory model that provides a memory semantics for CHERI-C programs. We present a generalised theory with rich properties suitable for verification and potentially other types of analyses. Our theory is backed by an Isabelle\/HOL formalisation that also generates an OCaml executable instance of the memory model. The verified and extracted code is then used to instantiate the parametric\n                    <jats:italic>Gillian<\/jats:italic>\n                    program analysis framework, with which we can perform concrete execution of CHERI-C programs. The tool can run a CHERI-C test suite, demonstrating the correctness of our tool, and catch a good class of safety violations that the CHERI hardware might miss.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_28","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T16:19:12Z","timestamp":1682093952000},"page":"549-568","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A Formal CHERI-C Semantics for Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7165-6857","authenticated-orcid":false,"given":"Seung Hoon","family":"Park","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5964-8819","authenticated-orcid":false,"given":"Rekha","family":"Pai","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2462-2782","authenticated-orcid":false,"given":"Tom","family":"Melham","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,22]]},"reference":[{"key":"28_CR1","unstructured":"CHERI C Tests. https:\/\/github.com\/CTSRD-CHERI\/cheri-c-tests"},{"key":"28_CR2","unstructured":"cheri-compressed-cap. https:\/\/github.com\/CTSRD-CHERI\/cheri-compressed-cap"},{"key":"28_CR3","unstructured":"CHERI RISC-V Sail model. https:\/\/github.com\/CTSRD-CHERI\/sail-cheri-riscv"},{"key":"28_CR4","unstructured":"CHERI: The Arm Morello Board, https:\/\/www.cl.cam.ac.uk\/research\/security\/ctsrd\/cheri\/cheri-morello.html"},{"key":"28_CR5","unstructured":"CHERI: The Digital Security by Design (DSbD) Initiative, https:\/\/www.cl.cam.ac.uk\/research\/security\/ctsrd\/cheri\/dsbd.html"},{"key":"28_CR6","unstructured":"Digital Security by Design Challenge \u2013 UKRI, https:\/\/www.ukri.org\/our-work\/our-main-funds\/industrial-strategy-challenge-fund\/artificial-intelligence-and-data-economy\/digital-security-by-design-challenge\/"},{"key":"28_CR7","unstructured":"fix the behaviour of free, https:\/\/github.com\/GillianPlatform\/Gillian\/commit\/6fa87b046f8d8f328c20b89cbdff1a00944da3fe, GillianPlatform\/Gillian@6fa87b0"},{"key":"28_CR8","unstructured":"Morello Sail specification. https:\/\/github.com\/CTSRD-CHERI\/sail-morello"},{"key":"28_CR9","unstructured":"Sail model of CHERI-MIPS ISA. https:\/\/github.com\/CTSRD-CHERI\/sail-cheri-mips"},{"key":"28_CR10","unstructured":"SCorCH: Secure Code for Capability Hardware, https:\/\/scorch-project.github.io"},{"key":"28_CR11","unstructured":"Armv8.5-A Memory Tagging Extension. Tech. rep. (Jun 2021), https:\/\/documentation-service.arm.com\/static\/624ea580caabfd7b3c13e23f?token="},{"key":"28_CR12","unstructured":"ARM Ltd.: Arm Architecture Reference Manual Supplement Morello for A-Profile Architecture (2022), https:\/\/documentation-service.arm.com\/static\/61e577e1b691546d37bd38a0?token="},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Armstrong, A., Bauereiss, T., Campbell, B., Reid, A., Gray, K.E., Norton, R.M., Mundkur, P., Wassell, M., French, J., Pulte, C., Flur, S., Stark, I., Krishnaswami, N., Sewell, P.: ISA Semantics for ARMv8-a, RISC-v, and CHERI-MIPS. Proc. ACM Program. Lang. 3(POPL) (Jan 2019)","DOI":"10.1145\/3290384"},{"key":"28_CR14","unstructured":"Beeren, J., Fernandez, M., Gao, X., Klein, G., Kolanski, R., Lim, J., Lewis, C., Matichuk, D., Sewell, T.: Finite Machine Word Library. Archive of Formal Proofs (Jun 2016), https:\/\/isa-afp.org\/entries\/Word_Lib.html, Formal proof development"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Brau\u00dfe, F., Shmarov, F., Menezes, R., Gadelha, M.R., Korovin, K., Reger, G., Cordeiro, L.C.: ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC. In: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. p. 773\u2013776. ISSTA 2022, Association for Computing Machinery, New York, NY, USA (2022)","DOI":"10.1145\/3533767.3543289"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local Action and Abstract Separation Logic. In: 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007). pp. 366\u2013378 (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"28_CR17","unstructured":"Chisnall, D.: Towards a Safe, High-Performance Heap Allocator (Sep 2022), https:\/\/soft-dev.org\/events\/cheritech22\/slides\/Chisnall.pdf, presented at CHERI Technical Workshop 2022"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Chisnall, D., Rothwell, C., Watson, R.N., Woodruff, J., Vadera, M., Moore, S.W., Roe, M., Davis, B., Neumann, P.G.: Beyond the PDP-11: Architectural Support for a Memory-Safe C Abstract Machine. SIGPLAN Not. 50(4), 117\u2013130 (Mar 2015)","DOI":"10.1145\/2775054.2694367"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A Precise Yet Efficient Memory Model For C. Electronic Notes in Theoretical Computer Science 254, 85\u2013103 (2009). https:\/\/doi.org\/10.1016\/j.entcs.2009.09.061, proceedings of the 4th International Workshop on Systems Software Verification (SSV 2009)","DOI":"10.1016\/j.entcs.2009.09.061"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"Fragoso\u00a0Santos, J., Maksimovi\u0107, P., Ayoun, S.E., Gardner, P.: Gillian, Part i: A Multi-Language Platform for Symbolic Execution. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 927\u2013942. PLDI 2020, Association for Computing Machinery, New York, NY, USA (2020)","DOI":"10.1145\/3385412.3386014"},{"key":"28_CR21","unstructured":"Haftmann, F.: Code generation from Isabelle\/HOL theories (Dec 2021), https:\/\/isabelle.in.tum.de\/doc\/codegen.pdf"},{"key":"28_CR22","doi-asserted-by":"publisher","unstructured":"Haftmann, F., Krauss, A., Kun\u010dar, O., Nipkow, T.: Data Refinement in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving. pp. 100\u2013115. Springer Berlin Heidelberg, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_10","DOI":"10.1007\/978-3-642-39634-2_10"},{"key":"28_CR23","doi-asserted-by":"publisher","unstructured":"Klein, G., Kolanski, R., Boyton, A.: Mechanised Separation Algebra. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving. pp. 332\u2013337. Springer Berlin Heidelberg, Berlin, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_22","DOI":"10.1007\/978-3-642-32347-8_22"},{"key":"28_CR24","doi-asserted-by":"publisher","unstructured":"Krebbers, R.: A Formal C Memory Model for Separation Logic. Journal of Automated Reasoning 57(4), 319\u2013387 (Dec 2016). https:\/\/doi.org\/10.1007\/s10817-016-9369-1","DOI":"10.1007\/s10817-016-9369-1"},{"key":"28_CR25","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Leroy, X., Wiedijk, F.: Formal C Semantics: CompCert and the C Standard. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving. pp. 543\u2013548. Springer International Publishing, Cham (2014)","DOI":"10.1007\/978-3-319-08970-6_36"},{"key":"28_CR26","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert Memory Model, Version 2. Research Report RR-7987, INRIA (Jun 2012)"},{"key":"28_CR27","doi-asserted-by":"publisher","unstructured":"Lochbihler, A.: Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving. pp. 116\u2013132. Springer Berlin Heidelberg, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_11","DOI":"10.1007\/978-3-642-39634-2_11"},{"key":"28_CR28","doi-asserted-by":"publisher","unstructured":"Maksimovic, P., Ayoun, S.E., Santos, J.F., Gardner, P.: Gillian, part II: real-world verification for javascript and C. In: Silva, A., Leino, K.R.M. (eds.) Proceedings of the 33rd Computer Aided Verification International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Part II. Lecture Notes in Computer Science, vol. 12760, pp. 827\u2013850. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_38","DOI":"10.1007\/978-3-030-81688-9_38"},{"key":"28_CR29","doi-asserted-by":"publisher","unstructured":"Maksimovic, P., Santos, J.F., Ayoun, S.E., Gardner, P.: Gillian: A Multi-Language Platform for Unified Symbolic Analysis (2021). https:\/\/doi.org\/10.48550\/ARXIV.2105.14769, https:\/\/arxiv.org\/abs\/2105.14769","DOI":"10.48550\/ARXIV.2105.14769"},{"key":"28_CR30","doi-asserted-by":"crossref","unstructured":"Memarian, K., Gomes, V.B.F., Davis, B., Kell, S., Richardson, A., Watson, R.N.M., Sewell, P.: Exploring C Semantics and Pointer Provenance. Proc. ACM Program. Lang. 3(POPL) (Jan 2019).","DOI":"10.1145\/3290380"},{"key":"28_CR31","unstructured":"Miller, M.: Trends, challenges, and strategic shifts in the software vulnerability mitigation landscape (Feb 2019), https:\/\/msrnd-cdn-stor.azureedge.net\/bluehat\/bluehatil\/2019\/assets\/doc\/Trends%2C%20Challenges%2C%20and%20Strategic%20Shifts%20in%20the%20Software%20Vulnerability%20Mitigation%20Landscape.pdf, presented at BlueHat IL"},{"key":"28_CR32","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. [ecture Notes in Computer Science, Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"28_CR33","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Incorrectness logic. Proc. ACM Program. Lang. 4(POPL) (Dec 2019). https:\/\/doi.org\/10.1145\/3371078, https:\/\/doi.org\/10.1145\/3371078","DOI":"10.1145\/3371078"},{"key":"28_CR34","unstructured":"Park, S.H.: A Formal CHERI-C Memory Model. Archive of Formal Proofs (Nov 2022), https:\/\/isa-afp.org\/entries\/CHERI-C_Memory_Model.html, Formal proof development"},{"key":"28_CR35","doi-asserted-by":"publisher","unstructured":"Park, S.H., Pai, R., Melham, T.: Artifact for Paper A formal CHERI-C Semantics for Verification (Jan 2023). https:\/\/doi.org\/10.5281\/zenodo.7504675, https:\/\/doi.org\/10.5281\/zenodo.7504675","DOI":"10.5281\/zenodo.7504675"},{"key":"28_CR36","unstructured":"Richardson, A.: Porting C\/C++ software to Morello (Sep 2022), https:\/\/soft-dev.org\/events\/cheritech22\/slides\/Richardson.pdf, presented at CHERI Technical Workshop 2022"},{"key":"28_CR37","unstructured":"Santos, J.F., Maksimovic, P., Ayoun, S.E., Gardner, P.: Gillian: Compositional Symbolic Execution for All. CoRR abs\/2001.05059 (2020), https:\/\/arxiv.org\/abs\/2001.05059"},{"key":"28_CR38","doi-asserted-by":"publisher","unstructured":"Tuch, H.: Formal Verification of C Systems Code. Journal of Automated Reasoning 42(2), 125\u2013187 (Apr 2009). https:\/\/doi.org\/10.1007\/s10817-009-9120-2","DOI":"10.1007\/s10817-009-9120-2"},{"key":"28_CR39","unstructured":"Watson, R., Laurie, B., Richardson, A.: Assessing the Viability of an Open-Source CHERI Desktop Software Ecosystem. Tech. rep., Capabilities Limited (Sep 2021), https:\/\/www.capabilitieslimited.co.uk\/pdfs\/20210917-capltd-cheri-desktop-report-version1-FINAL.pdf"},{"key":"28_CR40","unstructured":"Watson, R.N.M., Neumann, P.G., Woodruff, J., Roe, M., Almatary, H., Anderson, J., Baldwin, J., Barnes, G., Chisnall, D., Clarke, J., et\u00a0al.: Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 8). Tech. rep., University of Cambridge, Cambridge, England (Oct 2020), https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-951.pdf"},{"key":"28_CR41","unstructured":"Watson, R.N.M., Richardson, A., Davis, B., Baldwin, J., Chisnall, D., Clarke, J., Filardo, N., Moore, S.M., Napierala, E., Sewell, P., Neumann, P.G.: CHERI C\/C++ Programming Guide. Tech. rep., University of Cambridge, Cambridge, England (Jun 2020), https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-947.pdf"},{"key":"28_CR42","doi-asserted-by":"publisher","unstructured":"Wesley\u00a0Filardo, N., Gutstein, B.F., Woodruff, J., Ainsworth, S., Paul-Trifu, L., Davis, B., Xia, H., Tomasz\u00a0Napierala, E., Richardson, A., Baldwin, J., Chisnall, D., Clarke, J., Gudka, K., Joannou, A., Theodore\u00a0Markettos, A., Mazzinghi, A., Norton, R.M., Roe, M., Sewell, P., Son, S., Jones, T.M., Moore, S.W., Neumann, P.G., Watson, R.N.M.: Cornucopia: Temporal Safety for CHERI Heaps. In: 2020 IEEE Symposium on Security and Privacy (SP). pp. 608\u2013625 (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00098","DOI":"10.1109\/SP40000.2020.00098"},{"key":"28_CR43","doi-asserted-by":"publisher","unstructured":"Woodruff, J., Joannou, A., Xia, H., Fox, A., Norton, R.M., Chisnall, D., Davis, B., Gudka, K., Filardo, N.W., Markettos, A.T., Roe, M., Neumann, P.G., Watson, R.N.M., Moore, S.W.: CHERI Concentrate: Practical Compressed Capabilities. IEEE Transactions on Computers 68(10), 1455\u20131469 (2019). https:\/\/doi.org\/10.1109\/TC.2019.2914037","DOI":"10.1109\/TC.2019.2914037"},{"key":"28_CR44","doi-asserted-by":"crossref","unstructured":"Woodruff, J., Watson, R.N.M., Chisnall, D., Moore, S.W., Anderson, J., Davis, B., Laurie, B., Neumann, P.G., Norton, R., Roe, M.: The CHERI Capability Model: Revisiting RISC in an Age of Risk. In: 2014 ACM\/IEEE 41st International Symposium on Computer Architecture (ISCA). pp. 457\u2013468. IEEE (Jun 2014)","DOI":"10.1109\/ISCA.2014.6853201"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T17:06:49Z","timestamp":1781024809000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}