{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T13:22:55Z","timestamp":1773840175305,"version":"3.50.1"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T00:00:00Z","timestamp":1680739200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,4,6]]},"abstract":"<jats:p>We present Arm's efforts in verifying the specification and prototype reference implementation of the Realm Management Monitor (RMM), an essential firmware component of Arm Confidential Computing Architecture (Arm CCA), the recently-announced Confidential Computing technologies incorporated in the Armv9-A architecture. Arm CCA introduced the Realm Management Extension (RME), an architectural extension for Armv9-A, and a technology that will eventually be deployed in hundreds of millions of devices. Given the security-critical nature of the RMM, and its taxing threat model, we use a combination of interactive theorem proving, model checking, and concurrency-aware testing to validate and verify security and safety properties of both the specification and a prototype implementation of the RMM. Crucially, our verification efforts were, and are still being, developed and refined contemporaneously with active development of both specification and implementation, and have been adopted by Arm's product teams.<\/jats:p>\n          <jats:p>We describe our major achievements, realized through the application of formal techniques, as well as challenges that remain for future work. We believe that the work reported in this paper is the most thorough application of formal techniques to the design and implementation of any current commercially-viable Confidential Computing implementation, setting a new high-water mark for work in this area.<\/jats:p>","DOI":"10.1145\/3586040","type":"journal-article","created":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:06:02Z","timestamp":1680815162000},"page":"376-405","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["A Verification Methodology for the Arm\u00ae Confidential Computing Architecture: From a Secure Specification to Safe Implementations"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1564-3784","authenticated-orcid":false,"given":"Anthony C. J.","family":"Fox","sequence":"first","affiliation":[{"name":"ARM, UK"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-1773-2846","authenticated-orcid":false,"given":"Gareth","family":"Stockwell","sequence":"additional","affiliation":[{"name":"ARM, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9312-195X","authenticated-orcid":false,"given":"Shale","family":"Xiong","sequence":"additional","affiliation":[{"name":"ARM, UK"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-8277-4312","authenticated-orcid":false,"given":"Hanno","family":"Becker","sequence":"additional","affiliation":[{"name":"Amazon Web Services, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4643-3541","authenticated-orcid":false,"given":"Dominic P.","family":"Mulligan","sequence":"additional","affiliation":[{"name":"Amazon Web Services, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3289-4574","authenticated-orcid":false,"given":"Gustavo","family":"Petri","sequence":"additional","affiliation":[{"name":"Amazon Web Services, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7843-9556","authenticated-orcid":false,"given":"Nathan","family":"Chong","sequence":"additional","affiliation":[{"name":"Amazon Web Services, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,4,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_1","volume-title":"Last viewed","author":"Amazon Inc.","year":"2022","unstructured":"Amazon Inc. . Last viewed June 2022 . AWS CBMC viewer. https:\/\/github.com\/model-checking\/cbmc-viewer Amazon Inc.. Last viewed June 2022. AWS CBMC viewer. https:\/\/github.com\/model-checking\/cbmc-viewer"},{"key":"e_1_2_1_3_1","unstructured":"Arm Ltd.. 2008. ARM Security Technology. Building a Secure System using TrustZone Technology. https:\/\/documentation-service.arm.com\/static\/5f212796500e883ab8e74531 \t\t\t\t  Arm Ltd.. 2008. ARM Security Technology. Building a Secure System using TrustZone Technology. https:\/\/documentation-service.arm.com\/static\/5f212796500e883ab8e74531"},{"key":"e_1_2_1_4_1","unstructured":"Arm Ltd.. 2021. Arm Confidential Compute Architecture. https:\/\/www.arm.com\/architecture\/security-features\/arm-confidential-compute-architecture \t\t\t\t  Arm Ltd.. 2021. Arm Confidential Compute Architecture. https:\/\/www.arm.com\/architecture\/security-features\/arm-confidential-compute-architecture"},{"key":"e_1_2_1_5_1","volume-title":"Realm Management Monitor beta0 specification. https:\/\/developer.arm.com\/documentation\/den0137\/a\/ Accessed 25^ th","author":"Ltd Arm","year":"2022","unstructured":"Arm Ltd .. 2022. Realm Management Monitor beta0 specification. https:\/\/developer.arm.com\/documentation\/den0137\/a\/ Accessed 25^ th October 2022 , final version to be published 2022 Arm Ltd.. 2022. Realm Management Monitor beta0 specification. https:\/\/developer.arm.com\/documentation\/den0137\/a\/ Accessed 25^ th October 2022, final version to be published 2022"},{"key":"e_1_2_1_6_1","volume-title":"Last viewed","author":"Ltd Arm","year":"2022","unstructured":"Arm Ltd .. Last viewed June 2022 . Arm Architecture Reference Manual for A-profile architecture. https:\/\/developer.arm.com\/documentation\/ddi0487\/latest Arm Ltd.. Last viewed June 2022. Arm Architecture Reference Manual for A-profile architecture. https:\/\/developer.arm.com\/documentation\/ddi0487\/latest"},{"key":"e_1_2_1_7_1","volume-title":"Last viewed","author":"Ltd Arm","year":"2022","unstructured":"Arm Ltd .. Last viewed June 2022 . Introducing Iris, the new generation of debug and trace interface in Arm Models . https:\/\/community.arm.com\/arm-community-blogs\/b\/tools-software-ides-blog\/posts\/iris-the-new-debug-and-trace-interface-in-arm-models Arm Ltd.. Last viewed June 2022. Introducing Iris, the new generation of debug and trace interface in Arm Models. https:\/\/community.arm.com\/arm-community-blogs\/b\/tools-software-ides-blog\/posts\/iris-the-new-debug-and-trace-interface-in-arm-models"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.41331"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19458-5_2"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCS.2018.00018"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9446-0"},{"key":"e_1_2_1_13_1","volume-title":"Formally Verifying the FreeRTOS IPC Mechanism. In Embedded World Conference. 202\u2013211","author":"Chong Nathan","year":"2021","unstructured":"Nathan Chong and Bart Jacobs . 2021 . Formally Verifying the FreeRTOS IPC Mechanism. In Embedded World Conference. 202\u2013211 . https:\/\/www.amazon.science\/publications\/formally-verifying-freertos-interprocess-communication-mechanism Nathan Chong and Bart Jacobs. 2021. Formally Verifying the FreeRTOS IPC Mechanism. In Embedded World Conference. 202\u2013211. https:\/\/www.amazon.science\/publications\/formally-verifying-freertos-interprocess-communication-mechanism"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-011-0124-7"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_26"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516702"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517300.2517302"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103799.2103803"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3356903"},{"key":"e_1_2_1_23_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan (Newman) Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016 , Savannah, GA, USA , November 2-4, 2016, Kimberly Keeton and Timothy Roscoe (Eds.). USENIX Association, 653\u2013669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016, Kimberly Keeton and Timothy Roscoe (Eds.). USENIX Association, 653\u2013669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_17"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_23"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_9"},{"key":"e_1_2_1_34_1","volume-title":"30th USENIX Security Symposium, USENIX Security 2021","author":"Li Shih-Wei","year":"2021","unstructured":"Shih-Wei Li , Xupeng Li , Ronghui Gu , Jason Nieh , and John Zhuang Hui . 2021 . Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor . In 30th USENIX Security Symposium, USENIX Security 2021 , August 11-13, 2021, Michael Bailey and Rachel Greenstadt (Eds.). USENIX Association, 3953\u20133970. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/li-shih-wei Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. 2021. Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. In 30th USENIX Security Symposium, USENIX Security 2021, August 11-13, 2021, Michael Bailey and Rachel Greenstadt (Eds.). USENIX Association, 3953\u20133970. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/li-shih-wei"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_2_1_36_1","volume-title":"Design and Verification of the Arm Confidential Compute Architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Li Xupeng","year":"2022","unstructured":"Xupeng Li , Xuheng Li , Christoffer Dall , Ronghui Gu , Jason Nieh , Yousuf Sait , and Gareth Stockwell . 2022 . Design and Verification of the Arm Confidential Compute Architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22) . USENIX Association, Carlsbad, CA. 465\u2013484. isbn:978-1-939133-28-1 https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/li Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, and Gareth Stockwell. 2022. Design and Verification of the Arm Confidential Compute Architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22). USENIX Association, Carlsbad, CA. 465\u2013484. isbn:978-1-939133-28-1 https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/li"},{"key":"e_1_2_1_37_1","volume-title":"The Open Portable Trusted Execution Environment (OP-TEE). https:\/\/www.op-tee.org Accessed 23^ rd","author":"Ltd Linaro","year":"2022","unstructured":"Linaro Ltd .. 2022. The Open Portable Trusted Execution Environment (OP-TEE). https:\/\/www.op-tee.org Accessed 23^ rd June 2022 Linaro Ltd.. 2022. The Open Portable Trusted Execution Environment (OP-TEE). https:\/\/www.op-tee.org Accessed 23^ rd June 2022"},{"key":"e_1_2_1_38_1","unstructured":"Linaro Ltd.. 2022. TrustedFirmware-A. https:\/\/www.trustedfirmware.org\/projects\/tf-a\/ \t\t\t\t  Linaro Ltd.. 2022. TrustedFirmware-A. https:\/\/www.trustedfirmware.org\/projects\/tf-a\/"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-54876-0_9"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/HICSS.2013.121"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46078-8_48"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480741.2480757"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_3"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63406-3_16"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2021.3087421"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSD51259.2020.00099"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_24"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483560"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_18"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586040","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586040","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:10Z","timestamp":1750178770000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586040"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,6]]},"references-count":52,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2023,4,6]]}},"alternative-id":["10.1145\/3586040"],"URL":"https:\/\/doi.org\/10.1145\/3586040","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,6]]},"assertion":[{"value":"2023-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}