{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:29Z","timestamp":1776305249482,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":57,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,12,5]],"date-time":"2022-12-05T00:00:00Z","timestamp":1670198400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["61772266, 61431008"],"award-info":[{"award-number":["61772266, 61431008"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,12,5]]},"DOI":"10.1145\/3564625.3567984","type":"proceedings-article","created":{"date-parts":[[2022,12,3]],"date-time":"2022-12-03T01:01:29Z","timestamp":1670029289000},"page":"88-101","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal Modeling and Security Analysis for Intra-level Privilege Separation"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8104-6470","authenticated-orcid":false,"given":"Yinggang","family":"Guo","sequence":"first","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5154-162X","authenticated-orcid":false,"given":"Zicheng","family":"Wang","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0436-2709","authenticated-orcid":false,"given":"Bingnan","family":"Zhong","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0610-1553","authenticated-orcid":false,"given":"Qingkai","family":"Zeng","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,12,5]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Retrieved","year":"2022","unstructured":"Arm. 2022 . Arm Architecture Reference Manual . Retrieved June 28, 2022 from https:\/\/developer.arm.com\/documentation Arm. 2022. Arm Architecture Reference Manual. Retrieved June 28, 2022 from https:\/\/developer.arm.com\/documentation"},{"key":"e_1_3_2_1_2_1","volume-title":"SKEE: A lightweight Secure Kernel-level Execution Environment for ARM.. In NDSS, Vol.\u00a016. 21\u201324.","author":"Azab M","year":"2016","unstructured":"Ahmed\u00a0 M Azab , Kirk Swidowski , Rohan Bhutkar , Jia Ma , Wenbo Shen , Ruowen Wang , and Peng Ning . 2016 . SKEE: A lightweight Secure Kernel-level Execution Environment for ARM.. In NDSS, Vol.\u00a016. 21\u201324. Ahmed\u00a0M Azab, Kirk Swidowski, Rohan Bhutkar, Jia Ma, Wenbo Shen, Ruowen Wang, and Peng Ning. 2016. SKEE: A lightweight Secure Kernel-level Execution Environment for ARM.. In NDSS, Vol.\u00a016. 21\u201324."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00061"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10586-017-0833-4"},{"key":"e_1_3_2_1_5_1","volume-title":"SGXLock: Towards Efficiently Establishing Mutual Distrust Between Host Application and Enclave for SGX. In USENIX Security Symposium. 4129\u20134146","author":"Chen Yuan","year":"2022","unstructured":"Yuan Chen , Jiaqi Li , Guorui Xu , Yajin Zhou , Zhi Wang , Cong Wang , and Kui Ren . 2022 . SGXLock: Towards Efficiently Establishing Mutual Distrust Between Host Application and Enclave for SGX. In USENIX Security Symposium. 4129\u20134146 . Yuan Chen, Jiaqi Li, Guorui Xu, Yajin Zhou, Zhi Wang, Cong Wang, and Kui Ren. 2022. SGXLock: Towards Efficiently Establishing Mutual Distrust Between Host Application and Enclave for SGX. In USENIX Security Symposium. 4129\u20134146."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274704"},{"key":"e_1_3_2_1_7_1","unstructured":"Yeongpil Cho Donghyun Kwon Hayoon Yi and Yunheung Paek. 2017. Dynamic Virtual Address Range Adjustment for Intra-Level Privilege Separation on ARM.. In NDSS.  Yeongpil Cho Donghyun Kwon Hayoon Yi and Yunheung Paek. 2017. Dynamic Virtual Address Range Adjustment for Intra-Level Privilege Separation on ARM.. In NDSS."},{"key":"e_1_3_2_1_8_1","volume-title":"Retrieved","author":"CLEARSY.","year":"2022","unstructured":"CLEARSY. 2022 . Atelier B . Retrieved June 28, 2022 from https:\/\/www.atelierb.eu\/en\/ CLEARSY. 2022. Atelier B. Retrieved June 28, 2022 from https:\/\/www.atelierb.eu\/en\/"},{"key":"e_1_3_2_1_9_1","volume-title":"29th USENIX Security Symposium (USENIX Security 20)","author":"Cloosters Tobias","year":"2020","unstructured":"Tobias Cloosters , Michael Rodler , and Lucas Davi . 2020 . {TeeRex}: Discovery and Exploitation of Memory Corruption Vulnerabilities in {SGX} Enclaves . In 29th USENIX Security Symposium (USENIX Security 20) . 841\u2013858. Tobias Cloosters, Michael Rodler, and Lucas Davi. 2020. {TeeRex}: Discovery and Exploitation of Memory Corruption Vulnerabilities in {SGX} Enclaves. In 29th USENIX Security Symposium (USENIX Security 20). 841\u2013858."},{"key":"e_1_3_2_1_10_1","unstructured":"Victor Costan and Srinivas Devadas. 2016. Intel SGX explained. Cryptology ePrint Archive(2016).  Victor Costan and Srinivas Devadas. 2016. Intel SGX explained. Cryptology ePrint Archive(2016)."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694386"},{"key":"e_1_3_2_1_12_1","volume-title":"Retrieved","author":"Details CVE","year":"2022","unstructured":"CVE Details . 2022 . Linux kernel vulnerabilities . Retrieved June 28, 2022 from https:\/\/www.cvedetails.com\/product\/47\/Linux-Linux-Kernel.html?vendor_id=33 CVE Details. 2022. Linux kernel vulnerabilities. Retrieved June 28, 2022 from https:\/\/www.cvedetails.com\/product\/47\/Linux-Linux-Kernel.html?vendor_id=33"},{"key":"e_1_3_2_1_13_1","volume-title":"Retrieved","author":"Dill David","year":"2019","unstructured":"David Dill . 2019 . Murphi Model Checker . Retrieved June 28, 2022 from http:\/\/formalverification.cs.utah.edu\/Murphi\/ David Dill. 2019. Murphi Model Checker. Retrieved June 28, 2022 from http:\/\/formalverification.cs.utah.edu\/Murphi\/"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132782"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.29"},{"key":"e_1_3_2_1_17_1","volume-title":"31st USENIX Security Symposium (USENIX Security 22)","author":"Gu Jinyu","year":"2022","unstructured":"Jinyu Gu , Bojun Zhu , Mingyu Li , Wentai Li , Yubin Xia , and Haibo Chen . 2022 . A Hardware-Software Co-design for Efficient Intra-Enclave Isolation . In 31st USENIX Security Symposium (USENIX Security 22) . Jinyu Gu, Bojun Zhu, Mingyu Li, Wentai Li, Yubin Xia, and Haibo Chen. 2022. A Hardware-Software Co-design for Efficient Intra-Enclave Isolation. In 31st USENIX Security Symposium (USENIX Security 22)."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676975"},{"key":"e_1_3_2_1_19_1","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\u00a0Newman 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 16) . 653\u2013669. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan\u00a0Newman 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 16). 653\u2013669."},{"key":"e_1_3_2_1_20_1","volume-title":"Myth and truth about hypervisor-based kernel protector: The reason why you need shadow-box. Blackhat-ASIA","author":"Han Seunghun","year":"2017","unstructured":"Seunghun Han , Junghwan Kang , Wook Shin , H Kim , and Eungki Park . 2017. Myth and truth about hypervisor-based kernel protector: The reason why you need shadow-box. Blackhat-ASIA ; 2017 (2017). Seunghun Han, Junghwan Kang, Wook Shin, H Kim, and Eungki Park. 2017. Myth and truth about hypervisor-based kernel protector: The reason why you need shadow-box. Blackhat-ASIA; 2017 (2017)."},{"key":"e_1_3_2_1_21_1","volume-title":"Retrieved","author":"Heinrich-Heine-University","year":"2021","unstructured":"Heinrich-Heine-University . 2021 . The ProB Animator and Model Checker . Retrieved June 28, 2022 from https:\/\/prob.hhu.de\/ Heinrich-Heine-University. 2021. The ProB Animator and Model Checker. Retrieved June 28, 2022 from https:\/\/prob.hhu.de\/"},{"key":"e_1_3_2_1_22_1","volume-title":"Retrieved","year":"2022","unstructured":"Intel. 2022 . Intel 64 and IA-32 Architectures Software Developer Manuals . Retrieved June 28, 2022 from https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/intel-sdm.html Intel. 2022. Intel 64 and IA-32 Architectures Software Developer Manuals. Retrieved June 28, 2022 from https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/articles\/technical\/intel-sdm.html"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.45"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3386901.3389023"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3195970.3196061"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3309698"},{"key":"e_1_3_2_1_28_1","volume-title":"26th USENIX Security Symposium (USENIX Security 17)","author":"Lee Jaehyuk","year":"2017","unstructured":"Jaehyuk Lee , Jinsoo Jang , Yeongjin Jang , Nohyun Kwak , Yeseul Choi , Changho Choi , Taesoo Kim , Marcus Peinado , and Brent\u00a0 ByungHoon Kang . 2017 . Hacking in darkness: Return-oriented programming against secure enclaves . In 26th USENIX Security Symposium (USENIX Security 17) . 523\u2013539. Jaehyuk Lee, Jinsoo Jang, Yeongjin Jang, Nohyun Kwak, Yeseul Choi, Changho Choi, Taesoo Kim, Marcus Peinado, and Brent\u00a0ByungHoon Kang. 2017. Hacking in darkness: Return-oriented programming against secure enclaves. In 26th USENIX Security Symposium (USENIX Security 17). 523\u2013539."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483554"},{"key":"e_1_3_2_1_30_1","volume-title":"28th USENIX Security Symposium (USENIX Security 19)","author":"Li Shih-Wei","year":"2019","unstructured":"Shih-Wei Li , John\u00a0 S Koh , and Jason Nieh . 2019 . Protecting cloud virtual machines from hypervisor and host operating system exploits . In 28th USENIX Security Symposium (USENIX Security 19) . 1357\u20131374. Shih-Wei Li, John\u00a0S Koh, and Jason Nieh. 2019. Protecting cloud virtual machines from hypervisor and host operating system exploits. In 28th USENIX Security Symposium (USENIX Security 19). 1357\u20131374."},{"key":"e_1_3_2_1_31_1","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Li Shih-Wei","year":"2021","unstructured":"Shih-Wei Li , Xupeng Li , Ronghui Gu , Jason Nieh , and John\u00a0Zhuang Hui . 2021 . Formally verified memory protection for a commodity multiprocessor hypervisor . In 30th USENIX Security Symposium (USENIX Security 21) . 3953\u20133970. Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John\u00a0Zhuang Hui. 2021. Formally verified memory protection for a commodity multiprocessor hypervisor. In 30th USENIX Security Symposium (USENIX Security 21). 3953\u20133970."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3313808.3313810"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.00071"},{"key":"e_1_3_2_1_35_1","volume-title":"BOOMERANG: Exploiting the Semantic Gap in Trusted Execution Environments.. In NDSS.","author":"Machiry Aravind","year":"2017","unstructured":"Aravind Machiry , Eric Gustafson , Chad Spensky , Christopher Salls , Nick Stephens , Ruoyu Wang , Antonio Bianchi , Yung\u00a0Ryn Choe , Christopher Kruegel , and Giovanni Vigna . 2017 . BOOMERANG: Exploiting the Semantic Gap in Trusted Execution Environments.. In NDSS. Aravind Machiry, Eric Gustafson, Chad Spensky, Christopher Salls, Nick Stephens, Ruoyu Wang, Antonio Bianchi, Yung\u00a0Ryn Choe, Christopher Kruegel, and Giovanni Vigna. 2017. BOOMERANG: Exploiting the Semantic Gap in Trusted Execution Environments.. In NDSS."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2019.2915318"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_39_1","volume-title":"a proof assistant for higher-order logic","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Markus Wenzel , and Lawrence\u00a0 C Paulson . 2002. Isabelle\/HOL : a proof assistant for higher-order logic . Springer . Tobias Nipkow, Markus Wenzel, and Lawrence\u00a0C Paulson. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. Springer."},{"key":"e_1_3_2_1_40_1","volume-title":"Retrieved","author":"The Linux\u00a0Kernel Organization","year":"2022","unstructured":"The Linux\u00a0Kernel Organization . 2022 . The Linux Kernel Archives . Retrieved June 28, 2022 from http:\/\/www.kernel.org The Linux\u00a0Kernel Organization. 2022. The Linux Kernel Archives. Retrieved June 28, 2022 from http:\/\/www.kernel.org"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3291047"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1975.9939"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453933.3454024"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294294"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Lei Shi Yuming Wu Yubin Xia Nathan Dautenhahn Haibo Chen Binyu Zang and Jinming Li. 2017. Deconstructing Xen.. In NDSS.  Lei Shi Yuming Wu Yubin Xia Nathan Dautenhahn Haibo Chen Binyu Zang and Jinming Li. 2017. Deconstructing Xen.. In NDSS.","DOI":"10.14722\/ndss.2017.23455"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908113"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813608"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134098"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/782814.782838"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483560"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363206"},{"key":"e_1_3_2_1_52_1","volume-title":"25th USENIX Security Symposium (USENIX Security 16)","author":"Vasudevan Amit","year":"2016","unstructured":"Amit Vasudevan , Sagar Chaki , Petros Maniatis , Limin Jia , and Anupam Datta . 2016 . {\u00fcberSpark}: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor . In 25th USENIX Security Symposium (USENIX Security 16) . 87\u2013104. Amit Vasudevan, Sagar Chaki, Petros Maniatis, Limin Jia, and Anupam Datta. 2016. {\u00fcberSpark}: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor. In 25th USENIX Security Symposium (USENIX Security 16). 87\u2013104."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2017.2675991"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243847"},{"key":"e_1_3_2_1_55_1","volume-title":"22nd International Symposium on Research in Attacks, Intrusions and Defenses (RAID","author":"Weiser Samuel","year":"2019","unstructured":"Samuel Weiser , Luca Mayr , Michael Schwarz , and Daniel Gruss . 2019 . {SGXJail}: Defeating Enclave Malware via Confinement . In 22nd International Symposium on Research in Attacks, Intrusions and Defenses (RAID 2019). 353\u2013366. Samuel Weiser, Luca Mayr, Michael Schwarz, and Daniel Gruss. 2019. {SGXJail}: Defeating Enclave Malware via Confinement. In 22nd International Symposium on Research in Attacks, Intrusions and Defenses (RAID 2019). 353\u2013366."},{"key":"e_1_3_2_1_56_1","volume-title":"Retrieved","year":"2022","unstructured":"Wikipedia. 2022 . B-Method . Retrieved June 28, 2022 from https:\/\/en.wikipedia.org\/wiki\/B-Method Wikipedia. 2022. B-Method. Retrieved June 28, 2022 from https:\/\/en.wikipedia.org\/wiki\/B-Method"},{"key":"e_1_3_2_1_57_1","unstructured":"Richard Wilkins and Brian Richardson. 2013. UEFI secure boot in modern computer security solutions. In UEFI forum. 1\u201310.  Richard Wilkins and Brian Richardson. 2013. UEFI secure boot in modern computer security solutions. In UEFI forum. 1\u201310."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2017.10"}],"event":{"name":"ACSAC: Annual Computer Security Applications Conference","location":"Austin TX USA","acronym":"ACSAC"},"container-title":["Proceedings of the 38th Annual Computer Security Applications Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3564625.3567984","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3564625.3567984","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3564625.3567984","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:09:12Z","timestamp":1750183752000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3564625.3567984"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,5]]},"references-count":57,"alternative-id":["10.1145\/3564625.3567984","10.1145\/3564625"],"URL":"https:\/\/doi.org\/10.1145\/3564625.3567984","relation":{},"subject":[],"published":{"date-parts":[[2022,12,5]]},"assertion":[{"value":"2022-12-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}