{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:57:09Z","timestamp":1774025829103,"version":"3.50.1"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","award":["ASPIRE"],"award-info":[{"award-number":["ASPIRE"]}],"id":[{"id":"10.13039\/100006785","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":[[2023,6,6]]},"abstract":"<jats:p>Thin hypervisors make it possible to isolate key security components like keychains, fingerprint readers, and digital wallets from the easily-compromised operating system.  \nTo work together, virtual machines running on top of the hypervisor can make hypercalls to the hypervisor to share pages between each other in a controlled way.  \nHowever, the design of such hypercall ABIs remains a delicate balancing task between conflicting needs for expressivity, performance, and security.  \nIn particular, it raises the question of what makes the specification of a hypervisor, and of its hypercall ABIs, good enough for the virtual machines.  \nIn this paper, we validate the expressivity and security of the design of the hypercall ABIs of Arm's FF-A.  \nWe formalise a substantial fragment of FF-A as a machine with a simplified ISA in which hypercalls are steps of the machine.  \nWe then develop VMSL, a novel separation logic, which we prove sound with respect to the machine execution model, and use it to reason modularly about virtual machines which communicate through the hypercall ABIs, demonstrating the hypercall ABIs' expressivity.  \nMoreover, we use the logic to prove robust safety of communicating virtual machines, that is, the guarantee that even if some of the virtual machines are compromised and execute unknown code, they cannot break the safety properties of other virtual machines running known code.  \nThis demonstrates the intended security guarantees of the hypercall ABIs.  \nAll the results in the paper have been formalised in Coq using the Iris framework.<\/jats:p>","DOI":"10.1145\/3591279","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"1438-1462","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9652-4869","authenticated-orcid":false,"given":"Zongyuan","family":"Liu","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7322-5644","authenticated-orcid":false,"given":"Sergei","family":"Stepanenko","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4442-6543","authenticated-orcid":false,"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9035-4034","authenticated-orcid":false,"given":"Aslan","family":"Askarov","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2016.0331"},{"key":"e_1_2_1_3_1","unstructured":"Arm. 2021. Morello project. https:\/\/www.morello-project.org\/ \t\t\t\t  Arm. 2021. Morello project. https:\/\/www.morello-project.org\/"},{"key":"e_1_2_1_4_1","unstructured":"Arm Ltd.. 2022. Arm Firmware Framework for Arm A-profile version 1.1 - DEN0077A. https:\/\/documentation-service.arm.com\/static\/624d5f52dc9d4f0e74a54e5f \t\t\t\t  Arm Ltd.. 2022. Arm Firmware Framework for Arm A-profile version 1.1 - DEN0077A. https:\/\/documentation-service.arm.com\/static\/624d5f52dc9d4f0e74a54e5f"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_14"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_7"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuCNC.2016.7561034"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-019-00216-4"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250743"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/195473.195579"},{"key":"e_1_2_1_13_1","unstructured":"Vijay Chidambaram. 2018. We found a bug in a verified file system!. Twitter. https:\/\/twitter.com\/vj_chidambaram\/status\/1047505696533741568 \t\t\t\t  Vijay Chidambaram. 2018. We found a bug in a verified file system!. Twitter. https:\/\/twitter.com\/vj_chidambaram\/status\/1047505696533741568"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_2_1_15_1","unstructured":"Will Deacon. 2020. Virtualisation for the Masses: Exposing KVM on Android. http:\/\/linux-kernel.uio.no\/pub\/linux\/kernel\/people\/will\/slides\/kvmforum-2020-edited.pdf \t\t\t\t  Will Deacon. 2020. Virtualisation for the Masses: Exposing KVM on Android. http:\/\/linux-kernel.uio.no\/pub\/linux\/kernel\/people\/will\/slides\/kvmforum-2020-edited.pdf"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.22"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086365.1086399"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"e_1_2_1_20_1","volume-title":"Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code","author":"Georges A\u00efna Linn","year":"2022","unstructured":"A\u00efna Linn Georges , Arma\u00ebl Gu\u00e9neau , Thomas van Strydonck , Amin Timany , Alix Trieu , Dominique Devriese , and Lars Birkedal . 2022 . Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code . Aarhus University . https:\/\/cs.au.dk\/~birke\/papers\/cerise.pdf A\u00efna Linn Georges, Arma\u00ebl Gu\u00e9neau, Thomas van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, and Lars Birkedal. 2022. Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. Aarhus University. https:\/\/cs.au.dk\/~birke\/papers\/cerise.pdf"},{"key":"e_1_2_1_21_1","volume-title":"Cap","author":"Georges A\u00efna Linn","year":"2021","unstructured":"A\u00efna Linn Georges , Arma\u00ebl Gu\u00e9neau , Thomas Van-Strydonck , Amin Timany , Dominique Trieu , Alix Devriese , and Lars Birkedal . 2021. Cap \u2019 ou pas cap\u2019 ?: Preuve de programmes pour une machine \u00e0 capacit\u00e9s en pr\u00e9sence de code inconnu. In Journ\u00e9es Francophones des Langages Applicatifs 2021 . https:\/\/cris.vub.be\/ws\/portalfiles\/portal\/55081793\/paper.pdf A\u00efna Linn Georges, Arma\u00ebl Gu\u00e9neau, Thomas Van-Strydonck, Amin Timany, Dominique Trieu, Alix Devriese, and Lars Birkedal. 2021. Cap\u2019 ou pas cap\u2019 ?: Preuve de programmes pour une machine \u00e0 capacit\u00e9s en pr\u00e9sence de code inconnu. In Journ\u00e9es Francophones des Langages Applicatifs 2021. https:\/\/cris.vub.be\/ws\/portalfiles\/portal\/55081793\/paper.pdf"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527318"},{"key":"e_1_2_1_23_1","unstructured":"Google LLC. 2021. pKVM. https:\/\/android-kvm.googlesource.com\/linux\/+\/refs\/heads\/pkvm\/ \t\t\t\t  Google LLC. 2021. pKVM. https:\/\/android-kvm.googlesource.com\/linux\/+\/refs\/heads\/pkvm\/"},{"key":"e_1_2_1_24_1","unstructured":"Hafnium development team. 2022. Hafnium \u2014 A security-focussed type-1 hypervisor. https:\/\/opensource.google\/projects\/hafnium \t\t\t\t  Hafnium development team. 2022. Hafnium \u2014 A security-focussed type-1 hypervisor. https:\/\/opensource.google\/projects\/hafnium"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19056-8_4"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505897"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"e_1_2_1_35_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_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7813157"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201907)","author":"Magnus","year":"2084","unstructured":"Magnus O. Myreen and Michael J. C. Gordon. 2007. Hoare Logic for Realistically Modelled Machine Code . In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201907) . Springer-Verlag, Berlin, Heidelberg. 568\u2013582. isbn:978354071 2084 https:\/\/doi.org\/10.5555\/1763507.1763565 10.5555\/1763507.1763565 Magnus O. Myreen and Michael J. C. Gordon. 2007. Hoare Logic for Realistically Modelled Machine Code. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201907). Springer-Verlag, Berlin, Heidelberg. 568\u2013582. isbn:9783540712084 https:\/\/doi.org\/10.5555\/1763507.1763565"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111066"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_15"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00055"},{"key":"e_1_2_1_43_1","unstructured":"Quentin Perret. 2020. Protected KVM: Memory protection of KVM guests in Android. https:\/\/linuxplumbersconf.org\/event\/7\/contributions\/780\/ \t\t\t\t  Quentin Perret. 2020. Protected KVM: Memory protection of KVM guests in Android. https:\/\/linuxplumbersconf.org\/event\/7\/contributions\/780\/"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_24"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_6"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290332"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483560"},{"key":"e_1_2_1_51_1","volume-title":"Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis","author":"Watson Robert N. M.","year":"2019","unstructured":"Robert N. M. Watson , Peter G. Neumann , Jonathan Woodruff , Michael Roe , Hesham Almatary , Jonathan Anderson , John Baldwin , David Chisnall , Brooks Davis , Nathaniel Wesley Filardo , Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis , Robert Norton , Alex Richardson , Peter Sewell, Stacey Son, and Hongyan Xia. 2019 . Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7). University of Cambridge, Computer Laboratory. https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-927.html Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Hesham Almatary, Jonathan Anderson, John Baldwin, David Chisnall, Brooks Davis, Nathaniel Wesley Filardo, Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Kyndylan Nienhuis, Robert Norton, Alex Richardson, Peter Sewell, Stacey Son, and Hongyan Xia. 2019. Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 7). University of Cambridge, Computer Laboratory. https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-927.html"},{"key":"e_1_2_1_52_1","unstructured":"M. V. Wilkes and R. M. Needham. 1979. The Cambridge CAP Computer and Its Operating System. Elsevier. https:\/\/www.microsoft.com\/en-us\/research\/publication\/the-cambridge-cap-computer-and-its-operating-system\/ \t\t\t\t  M. V. Wilkes and R. M. Needham. 1979. The Cambridge CAP Computer and Its Operating System. Elsevier. https:\/\/www.microsoft.com\/en-us\/research\/publication\/the-cambridge-cap-computer-and-its-operating-system\/"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-36987-3_5"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016875"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591279","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591279","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:20Z","timestamp":1750178840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591279"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":54,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591279"],"URL":"https:\/\/doi.org\/10.1145\/3591279","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}