{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:06:24Z","timestamp":1767927984991,"version":"3.49.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 architectures.<\/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":1,"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"}]},{"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"}]},{"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"}]},{"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"}]},{"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"}]},{"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"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3613424.3614266"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_14"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_7"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676536.3676841"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3620665.3640416"},{"key":"e_1_2_2_6_1","volume-title":"PLARCH 2023","author":"Gao Dapeng","year":"2023","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-based-compartmentalisation.pdf"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3623510"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527318"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2023.3264676"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","unstructured":"Angus Hammond Ricardo Almeida Thomas Bauereiss Brian Campbell Ian Stark and Peter Sewell. 2025. Morello Cerise Artifact. https:\/\/doi.org\/10.5281\/zenodo.15047228 10.5281\/zenodo.15047228","DOI":"10.5281\/zenodo.15047228"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3616602"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547628"},{"key":"e_1_2_2_15_1","volume-title":"Retrofitting Fine Grain Isolation in the Firefox Renderer. 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_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-987"},{"key":"e_1_2_2_19_1","volume-title":"David Chisnall, Simon W Moore, Jonathan Anderson, Brooks Davis, Ben Laurie, Peter G Neumann","author":"Woodruff Jonathan","year":"2014","unstructured":"Jonathan Woodruff, Robert NM Watson, David Chisnall, Simon W Moore, Jonathan Anderson, Brooks Davis, Ben Laurie, Peter G Neumann, Robert Norton, and Michael Roe. 2014. The CHERI capability model: Revisiting RISC in an age of risk. In Proceeding of the 41st annual international symposium on Computer architecuture. 457\u2013468."}],"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":[[2025,7,16]],"date-time":"2025-07-16T06:07:36Z","timestamp":1752646056000},"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"}}]}}