{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:06:36Z","timestamp":1784199996110,"version":"3.55.0"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"DOI":"10.13039\/501100006041","name":"Innovate UK","doi-asserted-by":"publisher","award":["105694"],"award-info":[{"award-number":["105694"]}],"id":[{"id":"10.13039\/501100006041","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"publisher","award":["EP\/Y035976\/1"],"award-info":[{"award-number":["EP\/Y035976\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["789108"],"award-info":[{"award-number":["789108"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/Z000580\/1"],"award-info":[{"award-number":["EP\/Z000580\/1"]}],"id":[{"id":"10.13039\/501100000266","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":[[2025,6,10]]},"abstract":"<jats:p>When designing new architectural security mechanisms, a key question is whether they actually provide the intended security, but this has historically been very hard to assess. One cannot gain much confidence by testing, as such mechanisms should provide protection in the presence of arbitrary unknown code. Previously, one also could not gain confidence by mechanised proof, as the scale of production instruction-set architecture (ISA) designs, many tens or hundreds of thousands of lines of specification, made that prohibitive.<\/jats:p>\n                  <jats:p>We focus in this paper especially on the secure encapsulation of software components, as supported by CHERI architectures in general and by the Arm Morello prototype architecture and hardware design in particular. Secure encapsulation is an essential security mechanism, for fault isolation and to constrain untrusted third-party code. It has previously often been implemented using virtual memory, but that does not scale to large numbers of compartments. Morello provides capability-based mechanisms that do scale, within a single address space.<\/jats:p>\n                  <jats:p>We prove a strong secure encapsulation property for an example of encapsulated code running on Morello, that holds in the presence of arbitrary untrusted code, above a full-scale sequential model of the Morello ISA. To do so, we build on, extend, and unify three orthogonal lines of previous work: the Cerise proof of such an encapsulation property for a highly idealised capability machine, expressed using a logical relation in Iris; the Islaris approach for reasoning about known code in production-scale ISAs; and the T-CHERI security properties of arbitrary Morello code, previously proved only for executions up to domain crossing.<\/jats:p>\n                  <jats:p>This demonstrates how one can prove such strong properties of security mechanisms for full-scale industry\n\t\t\tarchitectures.<\/jats:p>","DOI":"10.1145\/3729329","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1961-1983","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9156-9240","authenticated-orcid":false,"given":"Angus","family":"Hammond","sequence":"first","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 Glasgow, Glasgow, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9607-8942","authenticated-orcid":false,"given":"Thomas","family":"Bauereiss","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\/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,6,13]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3613424.3614266"},{"key":"e_1_3_2_3_1","doi-asserted-by":"crossref","unstructured":"Alasdair Armstrong Brian Campbell Ben Simner Christopher Pulte and Peter Sewell. 2021. Isla: Integrating full-scale ISA semantics and axiomatic concurrency models. In In Proc. 33rd International Conference on Computer-Aided Verification. Extended version available at https:\/\/www.cl.cam.ac.uk\/~pes20\/isla\/isla-cav2021-extended.pdf.","DOI":"10.1007\/978-3-030-81685-8_14"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_7"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676536.3676841"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640416"},{"key":"e_1_3_2_7_1","unstructured":"Dapeng Gao and Robert N. M. Watson. 2023. Library-based Compartmentalisation on CHERI. Extended abstract PLARCH 2023. https:\/\/www.cl.cam.ac.uk\/research\/security\/ctsrd\/pdfs\/202306-plarch-library-basedcompartmentalisation.pdf"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3623510"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","unstructured":"A\u00efna Linn Georges Arma\u00ebl Gu\u00e9neau Thomas Van Strydonck Amin Timany Alix Trieu Sander Huyghebaert Dominique Devriese and Lars Birkedal. 2021. Efficient and provable local capability revocation using uninitialized capabilities. Proc. ACM Program. Lang. 5 POPL (2021) 1\u201330 doi:10.1145\/3434287","DOI":"10.1145\/3434287"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","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. Proc. ACM Program. Lang. 6 OOPSLA1 (2022) 1\u201330 doi:10.1145\/3527318","DOI":"10.1145\/3527318"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2023.3264676"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Angus Hammond Ricardo Almeida Thomas Bauereiss Brian Campbell Ian Stark and Peter Sewell. 2025. Morello Cerise Artifact. doi:10.5281\/zenodo.15047228","DOI":"10.5281\/zenodo.15047228"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3616602"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018) e20. doi:10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","unstructured":"Steven Keuchel Sander Huyghebaert Georgy Lukyanov and Dominique Devriese. 2022. Verified symbolic execution with Kripke specification monads (and no meta-programming). Proc. ACM Program. Lang. 6 ICFP (2022) 194\u2013224. doi:10.1145\/3547628","DOI":"10.1145\/3547628"},{"key":"e_1_3_2_16_1","first-page":"699","volume-title":"In 29th USENIX Security Symposium, USENIX Security 2020","author":"Narayan Shravan","year":"2020","unstructured":"Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, and Deian Stefan. 2020. Retrofitting Fine Grain Isolation in the Firefox Renderer. In 29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020, Srdjan Capkun and Franziska Roesner (Eds.). USENIX Association, 699\u2013716. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/narayan"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-987"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2014.6853201"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729329","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:07:52Z","timestamp":1784196472000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729329"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":19,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729329"],"URL":"https:\/\/doi.org\/10.1145\/3729329","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}