{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T00:01:25Z","timestamp":1773619285325,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,27]],"date-time":"2024-04-27T00:00:00Z","timestamp":1714176000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["U19A2060"],"award-info":[{"award-number":["U19A2060"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,27]]},"DOI":"10.1145\/3620665.3640398","type":"proceedings-article","created":{"date-parts":[[2024,4,22]],"date-time":"2024-04-22T14:18:06Z","timestamp":1713795486000},"page":"1218-1232","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-4987-3645","authenticated-orcid":false,"given":"Zhenyang","family":"Dai","sequence":"first","affiliation":[{"name":"Tsinghua University and Ant Group, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-1642-6893","authenticated-orcid":false,"given":"Shuang","family":"Liu","sequence":"additional","affiliation":[{"name":"Ant Group, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-7371-4969","authenticated-orcid":false,"given":"Vilhelm","family":"Sjoberg","sequence":"additional","affiliation":[{"name":"CertiK, New York, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9954-008X","authenticated-orcid":false,"given":"Xupeng","family":"Li","sequence":"additional","affiliation":[{"name":"Columbia University, New York, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-8455-3663","authenticated-orcid":false,"given":"Yu","family":"Chen","sequence":"additional","affiliation":[{"name":"Tsinghua University, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7294-2724","authenticated-orcid":false,"given":"Wenhao","family":"Wang","sequence":"additional","affiliation":[{"name":"Institute of Information Engineering, CAS, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-5545-0270","authenticated-orcid":false,"given":"Yuekai","family":"Jia","sequence":"additional","affiliation":[{"name":"Tsinghua University and Ant Group, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-7681-3683","authenticated-orcid":false,"given":"Sean Noble","family":"Anderson","sequence":"additional","affiliation":[{"name":"Portland State University, Portland, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9514-1360","authenticated-orcid":false,"given":"Laila","family":"Elbeheiry","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Software Systems, Saarbr\u00fccken, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-1744-7473","authenticated-orcid":false,"given":"Shubham","family":"Sondhi","sequence":"additional","affiliation":[{"name":"CertiK, New York, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-1160-9851","authenticated-orcid":false,"given":"Yu","family":"Zhang","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-6138-8780","authenticated-orcid":false,"given":"Zhaozhong","family":"Ni","sequence":"additional","affiliation":[{"name":"CertiK, New York, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-9580-5395","authenticated-orcid":false,"given":"Shoumeng","family":"Yan","sequence":"additional","affiliation":[{"name":"Ant Group, Beijing, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6812-6182","authenticated-orcid":false,"given":"Ronghui","family":"Gu","sequence":"additional","affiliation":[{"name":"Columbia University, New York, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7682-1019","authenticated-orcid":false,"given":"Zhengyu","family":"He","sequence":"additional","affiliation":[{"name":"Ant Group, Hangzhou, China"}]}],"member":"320","published-online":{"date-parts":[[2024,4,27]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2021-33478","author":"Cve","year":"2021","unstructured":"Cve - cve-2021-33478. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2021-33478, 2021."},{"key":"e_1_3_2_1_2_1","volume-title":"https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2021-30338","author":"Cve","year":"2021","unstructured":"Cve - cve-2021-33478. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2021-30338, 2021."},{"key":"e_1_3_2_1_3_1","volume-title":"https:\/\/github.com\/nikomatsakis\/a-mir-formality","author":"A PLT","year":"2022","unstructured":"A PLT redex model of MIR and its type system. https:\/\/github.com\/nikomatsakis\/a-mir-formality, 2022."},{"key":"e_1_3_2_1_4_1","volume-title":"https:\/\/www.cloudhypervisor.org\/","author":"Run Cloud Virtual Machines Cloud Hypervisor","year":"2022","unstructured":"Cloud Hypervisor - Run Cloud Virtual Machines Securely and Efficiently. https:\/\/www.cloudhypervisor.org\/, 2022."},{"key":"e_1_3_2_1_5_1","volume-title":"https:\/\/github.com\/google\/crosvm","author":"OS","year":"2022","unstructured":"crosvm - the chrome OS virtual machine monitor. https:\/\/github.com\/google\/crosvm, 2022."},{"key":"e_1_3_2_1_6_1","volume-title":"https:\/\/diosix.org\/","author":"Diosix","year":"2022","unstructured":"Diosix hypervisor. https:\/\/diosix.org\/, 2022."},{"key":"e_1_3_2_1_7_1","volume-title":"https:\/\/github.com\/model-checking\/kani","author":"Kani","year":"2022","unstructured":"Kani rust verifier. https:\/\/github.com\/model-checking\/kani, 2022."},{"key":"e_1_3_2_1_8_1","volume-title":"Rust For The Kernel Could Possibly Be Merged For Linux 5.20. https:\/\/www.phoronix.com\/scan.php?page=news_item&px=Rust-For-Linux-5.20-Possible\/","author":"Torvalds Linus","year":"2022","unstructured":"Linus Torvalds: Rust For The Kernel Could Possibly Be Merged For Linux 5.20. https:\/\/www.phoronix.com\/scan.php?page=news_item&px=Rust-For-Linux-5.20-Possible\/, 2022."},{"key":"e_1_3_2_1_9_1","volume-title":"lib\/transforms\/utils\/mem2reg.cpp source file. https:\/\/llvm.org\/doxygen\/Mem2Reg_8cpp_source.html","author":"Llvm","year":"2022","unstructured":"Llvm: lib\/transforms\/utils\/mem2reg.cpp source file. https:\/\/llvm.org\/doxygen\/Mem2Reg_8cpp_source.html, 2022."},{"key":"e_1_3_2_1_10_1","volume-title":"https:\/\/coq.inria.fr\/refman\/proof-engine\/ltac.html","author":"Ltac","year":"2022","unstructured":"Ltac --- coq 8.15.2 documentation. https:\/\/coq.inria.fr\/refman\/proof-engine\/ltac.html, 2022."},{"key":"e_1_3_2_1_11_1","volume-title":"https:\/\/www.redox-os.org\/","author":"Redox","year":"2022","unstructured":"Redox - your next(gen) os - redox - your next(gen) os. https:\/\/www.redox-os.org\/, 2022."},{"key":"e_1_3_2_1_12_1","volume-title":"https:\/\/www.amd.com\/en\/developer\/sev.html","author":"Secure Encrypted AMD","year":"2023","unstructured":"AMD Secure Encrypted Virtualization (SEV) | AMD. https:\/\/www.amd.com\/en\/developer\/sev.html, 2023."},{"key":"e_1_3_2_1_13_1","volume-title":"https:\/\/aws.amazon.com\/ec2\/nitro\/nitro-enclaves\/","author":"Enclaves Nitro","year":"2023","unstructured":"Nitro Enclaves. https:\/\/aws.amazon.com\/ec2\/nitro\/nitro-enclaves\/, 2023."},{"key":"e_1_3_2_1_14_1","volume-title":"Trustzone: Integrated hardware and software security. 01","author":"Alves Thaynara","year":"2004","unstructured":"Thaynara Alves and D. Felton. Trustzone: Integrated hardware and software security. 01 2004."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_1_16_1","first-page":"1041","volume-title":"26th USENIX Security Symposium (USENIX Security 17)","author":"Bulck Jo Van","year":"2017","unstructured":"Jo Van Bulck, Nico Weichbrodt, R\u00fcdiger Kapitza, Frank Piessens, and Raoul Strackx. Telling your secrets without page faults: Stealthy page table-based attacks on enclaved execution. In 26th USENIX Security Symposium (USENIX Security 17), pages 1041--1056, Vancouver, BC, August 2017. USENIX Association."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSC54232.2022.9888822"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_2_1_21_1","volume-title":"July","author":"Ant Group","year":"2023","unstructured":"Ant Group. Hyperenclave open source release. https:\/\/github.com\/HyperEnclave\/hyperenclave, July 2023."},{"key":"e_1_3_2_1_22_1","first-page":"653","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), pages 653--669, 2016."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192381"},{"key":"e_1_3_2_1_24_1","volume-title":"2022 USENIX Annual Technical Conference (USENIX ATC 22)","author":"Jia Yuekai","year":"2022","unstructured":"Yuekai Jia, Shuang Liu, Wenhao Wang, Yu Chen, Zhengde Zhai, Shoumeng Yan, and Zhengyu He. HyperEnclave: An open and cross-platform trusted execution environment. In 2022 USENIX Annual Technical Conference (USENIX ATC 22), Carlsbad, CA, July 2022. USENIX Association."},{"key":"e_1_3_2_1_25_1","volume-title":"Proc. ACM Program. Lang., 2(POPL), dec","author":"Jung Ralf","year":"2017","unstructured":"Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. Rustbelt: Securing the foundations of the rust programming language. Proc. ACM Program. Lang., 2(POPL), dec 2017."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132786"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_3_2_1_32_1","first-page":"465","volume-title":"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. Design and verification of the arm confidential compute architecture. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22), pages 465--484, Carlsbad, CA, July 2022. USENIX Association."},{"key":"e_1_3_2_1_33_1","first-page":"851","volume-title":"17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23)","author":"Li Xupeng","year":"2023","unstructured":"Xupeng Li, Xuheng Li, Wei Qiang, Ronghui Gu, and Jason Nieh. Spoq: Scaling Machine-Checkable systems verification in coq. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23), pages 851--869, Boston, MA, July 2023. USENIX Association."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2018.8471992"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3317550.3321449"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3342195.3387516"},{"key":"e_1_3_2_1_38_1","volume-title":"A formalization of the rust programming language","author":"Reed Eric C.","year":"2015","unstructured":"Eric C. Reed. Patina : A formalization of the rust programming language. 2015."},{"key":"e_1_3_2_1_39_1","volume-title":"Dependable Software Systems Engineering","author":"Rosu Grigore","year":"2017","unstructured":"Grigore Rosu. K: A semantic framework for programming languages and formal analysis tools. In Dependable Software Systems Engineering, 2017."},{"key":"e_1_3_2_1_40_1","volume-title":"Computer Science Laboratory Menlo Park","author":"Rushby John","year":"1992","unstructured":"John Rushby. Noninterference, transitivity, and channel-control security policies. SRI International, Computer Science Laboratory Menlo Park, 1992."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2995306.2995307"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483560"},{"key":"e_1_3_2_1_43_1","volume-title":"https:\/\/github.com\/rust-lang\/miri","author":"Miri Miri","year":"2021","unstructured":"Miri team. Miri. https:\/\/github.com\/rust-lang\/miri, 2021."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.36"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2018.00014"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134038"},{"key":"e_1_3_2_1_47_1","volume-title":"Oxide: The essence of rust. arXiv preprint arXiv:1903.00982","author":"Weiss Aaron","year":"2019","unstructured":"Aaron Weiss, Olek Gierczak, Daniel Patterson, and Amal Ahmed. Oxide: The essence of rust. arXiv preprint arXiv:1903.00982, 2019."},{"key":"e_1_3_2_1_48_1","volume-title":"Memory-safety challenge considered solved? an in-depth study with all rust cves. ACM Trans. Softw. Eng. Methodol., 31(1), sep","author":"Xu Hui","year":"2021","unstructured":"Hui Xu, Zhuangbin Chen, Mingshen Sun, Yangfan Zhou, and Michael R. Lyu. Memory-safety challenge considered solved? an in-depth study with all rust cves. ACM Trans. Softw. Eng. Methodol., 31(1), sep 2021."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.45"}],"event":{"name":"ASPLOS '24: 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2","location":"La Jolla CA USA","acronym":"ASPLOS '24","sponsor":["SIGARCH ACM Special Interest Group on Computer Architecture","SIGOPS ACM Special Interest Group on Operating Systems","SIGPLAN ACM Special Interest Group on Programming Languages","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3620665.3640398","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3620665.3640398","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:03:42Z","timestamp":1750291422000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3620665.3640398"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,27]]},"references-count":49,"alternative-id":["10.1145\/3620665.3640398","10.1145\/3620665"],"URL":"https:\/\/doi.org\/10.1145\/3620665.3640398","relation":{},"subject":[],"published":{"date-parts":[[2024,4,27]]},"assertion":[{"value":"2024-04-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}