{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,21]],"date-time":"2026-04-21T03:43:55Z","timestamp":1776743035011,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":99,"publisher":"ACM","funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N68335-22-C-0411"],"award-info":[{"award-number":["N68335-22-C-0411"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["W912CG-23-C-0032"],"award-info":[{"award-number":["W912CG-23-C-0032"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3731569.3764826","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:43:24Z","timestamp":1759322604000},"page":"85-100","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["The Design and Implementation of a Virtual Firmware Monitor"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-7021-158X","authenticated-orcid":false,"given":"Charly","family":"Castes","sequence":"first","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-3785-0366","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Costa","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-1507-5787","authenticated-orcid":false,"given":"Neelu S.","family":"Kalani","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8298-1126","authenticated-orcid":false,"given":"Timothy","family":"Roscoe","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6557-684X","authenticated-orcid":false,"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell, Ithaca, USA"},{"name":"Jane Street, New York, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8468-8409","authenticated-orcid":false,"given":"Thomas","family":"Bourgeat","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7237-6929","authenticated-orcid":false,"given":"Edouard","family":"Bugnion","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,12]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Memtier benchmark. https:\/\/github.com\/RedisLabs\/memtier_benchmark."},{"key":"e_1_3_2_1_2_1","unstructured":"RISC-V IOPMP specification. https:\/\/github.com\/riscv-non-isa\/iopmp-spec."},{"key":"e_1_3_2_1_3_1","unstructured":"RISC-V profiles. https:\/\/github.com\/riscv\/riscv-profiles."},{"key":"e_1_3_2_1_4_1","unstructured":"RISC-V Sail model. https:\/\/github.com\/riscv\/sail-riscv."},{"key":"e_1_3_2_1_5_1","unstructured":"RustSBI: RISC-V supervisor binary interface library in Rust. https:\/\/github.com\/rustsbi\/rustsbi."},{"key":"e_1_3_2_1_6_1","unstructured":"Zephyr project: Scalable real-time operating system (RTOS). https:\/\/www.zephyrproject.org."},{"key":"e_1_3_2_1_7_1","volume-title":"https:\/\/www.darkreading.com\/endpoint-security\/millions-of-devices-vulnerable-to-pkfail-secure-boot-bypass-issue","author":"Devices Millions","year":"2024","unstructured":"Millions of Devices Vulnerable to 'PKFail' Secure Boot Bypass Issue. https:\/\/www.darkreading.com\/endpoint-security\/millions-of-devices-vulnerable-to-pkfail-secure-boot-bypass-issue, 2024."},{"key":"e_1_3_2_1_8_1","volume-title":"https:\/\/www.techpowerup.com\/325488\/sinkclose-vulnerability-affects-every-amd-cpu-dating-back-to-2006","author":"Dating Vulnerability Affects","year":"2024","unstructured":"\"Sinkclose\" Vulnerability Affects Every AMD CPU Dating Back to 2006. https:\/\/www.techpowerup.com\/325488\/sinkclose-vulnerability-affects-every-amd-cpu-dating-back-to-2006, 2024."},{"key":"e_1_3_2_1_9_1","volume-title":"How bad OEM firmware ruins TPM security. https:\/\/mkukri.xyz\/2024\/06\/01\/tpm-gpio-fail.html","author":"TPM GPIO","year":"2024","unstructured":"TPM GPIO fail: How bad OEM firmware ruins TPM security. https:\/\/mkukri.xyz\/2024\/06\/01\/tpm-gpio-fail.html, 2024."},{"key":"e_1_3_2_1_10_1","volume-title":"Widespread Impact from Vulnerability in Popular PC and Server Firmware. https:\/\/eclypsium.com\/blog\/","year":"2024","unstructured":"UEFIcanhazbufferoverflow: Widespread Impact from Vulnerability in Popular PC and Server Firmware. https:\/\/eclypsium.com\/blog\/, 2024."},{"key":"e_1_3_2_1_11_1","volume-title":"Microcode Signature Verification Vulnerability. https:\/\/github.com\/google\/security-research\/security\/advisories\/GHSA-4xq7-4mgh-gp6w","author":"AMD","year":"2025","unstructured":"AMD: Microcode Signature Verification Vulnerability. https:\/\/github.com\/google\/security-research\/security\/advisories\/GHSA-4xq7-4mgh-gp6w, 2025."},{"key":"e_1_3_2_1_12_1","volume-title":"https:\/\/developer.arm.com\/documentation\/den0129\/latest\/","author":"Management Arm Realm","year":"2025","unstructured":"Arm Realm Management Extension (RME) System Architecture. https:\/\/developer.arm.com\/documentation\/den0129\/latest\/, 2025."},{"key":"e_1_3_2_1_13_1","volume-title":"https:\/\/aws.amazon.com\/ec2\/nitro\/nitro-enclaves\/","author":"Aws","year":"2025","unstructured":"Aws nitro enclaves. https:\/\/aws.amazon.com\/ec2\/nitro\/nitro-enclaves\/, 2025."},{"key":"e_1_3_2_1_14_1","volume-title":"https:\/\/github.com\/riscv-software-src\/opensbi","author":"Open Source Supervisor Binary RISC-V","year":"2025","unstructured":"RISC-V Open Source Supervisor Binary Interface (OpenSBI). https:\/\/github.com\/riscv-software-src\/opensbi, 2025."},{"key":"e_1_3_2_1_15_1","volume-title":"https:\/\/github.com\/riscv\/riscv-smmtt","author":"Supervisor Domains Access Protection RISC-V","year":"2025","unstructured":"RISC-V Supervisor Domains Access Protection. https:\/\/github.com\/riscv\/riscv-smmtt, 2025."},{"key":"e_1_3_2_1_16_1","volume-title":"https:\/\/trustedfirmware-a.readthedocs.io\/en\/latest\/","author":"Trusted","year":"2025","unstructured":"Trusted Firmware-A. https:\/\/trustedfirmware-a.readthedocs.io\/en\/latest\/, 2025."},{"key":"e_1_3_2_1_17_1","volume-title":"https:\/\/trustedfirmware-a.readthedocs.io\/en\/latest\/security_advisories\/index.html","author":"Trusted","year":"2025","unstructured":"Trusted Firmware-A, Security Advisories. https:\/\/trustedfirmware-a.readthedocs.io\/en\/latest\/security_advisories\/index.html, 2025."},{"key":"e_1_3_2_1_18_1","first-page":"183","volume-title":"Proceeedings of the International Workshop on Current Trends in Applied Formal Method","author":"Agerholm Sten","year":"1998","unstructured":"Sten Agerholm and Peter Gorm Larsen. A Lightweight Approach to Formal Methods. In Proceeedings of the International Workshop on Current Trends in Applied Formal Method, pages 168\u2013183, 1998."},{"key":"e_1_3_2_1_19_1","first-page":"54","volume-title":"Proceedings of the 3rd International Conference on Verified Software, Theories, Tools and Experiments (VSTTE)","author":"Alkassar Eyad","year":"2010","unstructured":"Eyad Alkassar, Mark A. Hillebrand, Wolfgang J. Paul, and Elena Petrova. Automated Verification of a Small Hypervisor. In Proceedings of the 3rd International Conference on Verified Software, Theories, Tools and Experiments (VSTTE), pages 40\u201354, 2010."},{"key":"e_1_3_2_1_20_1","unstructured":"AMD. Secure virtual machine architecture reference manual 2005."},{"key":"e_1_3_2_1_21_1","volume-title":"White Paper","author":"AMD.","year":"2020","unstructured":"AMD. Sev-snp: Strengthening vm isolation with integrity protection and more. White Paper, January, 2020."},{"key":"e_1_3_2_1_22_1","first-page":"327","volume-title":"Proceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP)","author":"Amit Nadav","year":"2015","unstructured":"Nadav Amit, Dan Tsafrir, Assaf Schuster, Ahmad Ayoub, and Eran Shlomo. Virtual CPU validation. In Proceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP), pages 311\u2013327, 2015."},{"key":"e_1_3_2_1_23_1","volume-title":"White Paper","author":"Building ARM.","year":"2009","unstructured":"ARM. Building a secure system using trustzone technology. White Paper, April, 2009."},{"key":"e_1_3_2_1_24_1","volume-title":"Proc. ACM Program. Lang., 3(POPL):71:1\u201371:31","author":"Armstrong Alasdair","year":"2019","unstructured":"Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS. Proc. ACM Program. Lang., 3(POPL):71:1\u201371:31, 2019."},{"key":"e_1_3_2_1_25_1","first-page":"1090","volume-title":"Emmanuel Stapf. CURE: A Security Architecture with CUstomizable and Resilient Enclaves. In Proceedings of the 30th USENIX Security Symposium","author":"Bahmani Raad","year":"2021","unstructured":"Raad Bahmani, Ferdinand Brasser, Ghada Dessouky, Patrick Jauernig, Matthias Klimmek, Ahmad-Reza Sadeghi, and Emmanuel Stapf. CURE: A Security Architecture with CUstomizable and Resilient Enclaves. In Proceedings of the 30th USENIX Security Symposium, pages 1073\u20131090, 2021."},{"key":"e_1_3_2_1_26_1","first-page":"177","volume-title":"Proceedings of the 19th ACM Symposium on Operating Systems Principles (SOSP)","author":"Barham Paul","year":"2003","unstructured":"Paul Barham, Boris Dragovic, Keir Fraser, Steven Hand, Tim Harris, Alex Ho, Rolf Neugebauer, Ian Pratt, and Andrew Warfield. Xen and the art of virtualization. In Proceedings of the 19th ACM Symposium on Operating Systems Principles (SOSP), pages 164\u2013177, 2003."},{"key":"e_1_3_2_1_27_1","first-page":"137","volume-title":"Proceedings of The 16th Workshop on Hot Topics in Operating Systems (HotOS-XVI)","author":"Baumann Andrew","year":"2017","unstructured":"Andrew Baumann. Hardware is the new Software. In Proceedings of The 16th Workshop on Hot Topics in Operating Systems (HotOS-XVI), pages 132\u2013137, 2017."},{"key":"e_1_3_2_1_28_1","first-page":"265","volume-title":"Proceedings of the 2022 EuroSys Conference","author":"Behrens Jonathan","year":"2022","unstructured":"Jonathan Behrens, Adam Belay, and M. Frans Kaashoek. Performance evolution of mitigating transient execution attacks. In Proceedings of the 2022 EuroSys Conference, pages 251\u2013265, 2022."},{"key":"e_1_3_2_1_29_1","unstructured":"Jonathan Behrens Cel Skeggs Samuel Ortiz and Frans Kaashoek. RVirt. https:\/\/github.com\/mit-pdos\/RVirt."},{"key":"e_1_3_2_1_30_1","first-page":"850","volume-title":"Proceedings of the 28th ACM Symposium on Operating Systems Principles (SOSP)","author":"Bornholt James","year":"2021","unstructured":"James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, and Andrew Warfield. Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3. In Proceedings of the 28th ACM Symposium on Operating Systems Principles (SOSP), pages 836\u2013850, 2021."},{"issue":"4","key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1145\/265924.265930","article-title":"Running Commodity Operating Systems on Scalable Multiprocessors","volume":"15","author":"Bugnion Edouard","year":"1997","unstructured":"Edouard Bugnion, Scott Devine, Kinshuk Govil, and Mendel Rosenblum. Disco: Running Commodity Operating Systems on Scalable Multiprocessors. ACM Trans. Comput. Syst., 15(4):412\u2013447, 1997.","journal-title":"ACM Trans. Comput. Syst."},{"issue":"4","key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2382553.2382554","article-title":"Bringing Virtualization to the x86 Architecture with the Original VMware Workstation","volume":"30","author":"Bugnion Edouard","year":"2012","unstructured":"Edouard Bugnion, Scott Devine, Mendel Rosenblum, Jeremy Sugerman, and Edward Y. Wang. Bringing Virtualization to the x86 Architecture with the Original VMware Workstation. ACM Trans. Comput. Syst., 30(4):12:1\u201312:51, 2012.","journal-title":"ACM Trans. Comput. Syst."},{"key":"e_1_3_2_1_33_1","first-page":"72","volume-title":"Proceedings of the 41st IEEE Symposium on Security and Privacy (S&P)","author":"Bulck Jo Van","year":"2020","unstructured":"Jo Van Bulck, Daniel Moghimi, Michael Schwarz, Moritz Lipp, Marina Minkin, Daniel Genkin, Yuval Yarom, Berk Sunar, Daniel Gruss, and Frank Piessens. LVI: Hijacking Transient Execution through Microarchitectural Load Value Injection. In Proceedings of the 41st IEEE Symposium on Security and Privacy (S&P), pages 54\u201372, 2020."},{"key":"e_1_3_2_1_34_1","first-page":"238","volume-title":"Proceedings of The 19th Workshop on Hot Topics in Operating Systems (HotOS-XIX)","author":"Castes Charly","year":"2023","unstructured":"Charly Castes, Adrien Ghosn, Neelu Shivprakash Kalani, Yuchen Qian, Marios Kogias, Mathias Payer, and Edouard Bugnion. Creating Trust by Abolishing Hierarchies. In Proceedings of The 19th Workshop on Hot Topics in Operating Systems (HotOS-XIX), pages 231\u2013238, 2023."},{"key":"e_1_3_2_1_35_1","first-page":"472","volume-title":"Cl\u00e9ment Pit-Claudel. Practical Verification of System-Software Components Written in Standard C. In Proceedings of the 30th ACM Symposium on Operating Systems Principles (SOSP)","author":"Cebeci Can","year":"2024","unstructured":"Can Cebeci, Yong-Hao Zou, Diyu Zhou, George Candea, and Cl\u00e9ment Pit-Claudel. Practical Verification of System-Software Components Written in Standard C. In Proceedings of the 30th ACM Symposium on Operating Systems Principles (SOSP), pages 455\u2013472, 2024."},{"key":"e_1_3_2_1_36_1","first-page":"1432","volume-title":"Sandro Pinto. SoK: Understanding the Prevailing Security Vulnerabilities in TrustZone-assisted TEE Systems. In Proceedings of the 41st IEEE Symposium on Security and Privacy (S&P)","author":"Cerdeira David","year":"2020","unstructured":"David Cerdeira, Nuno Santos, Pedro Fonseca, and Sandro Pinto. SoK: Understanding the Prevailing Security Vulnerabilities in TrustZone-assisted TEE Systems. In Proceedings of the 41st IEEE Symposium on Security and Privacy (S&P), pages 1416\u20131432, 2020."},{"key":"e_1_3_2_1_37_1","first-page":"13","volume-title":"Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-XIII)","author":"Chen Xiaoxin","year":"2008","unstructured":"Xiaoxin Chen, Tal Garfinkel, E. Christopher Lewis, Pratap Subrahmanyam, Carl A. Waldspurger, Dan Boneh, Jeffrey S. Dwoskin, and Dan R. K. Ports. Overshadow: a virtualization-based approach to retrofitting protection in commodity operating systems. In Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-XIII), pages 2\u201313, 2008."},{"issue":"9","key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3652597","article-title":"Intel TDX Demystified","volume":"56","author":"Cheng Pau-Chen","year":"2024","unstructured":"Pau-Chen Cheng, Wojciech Ozga, Enriquillo Valdez, Salman Ahmed, Zhongshu Gu, Hani Jamjoom, Hubertus Franke, and James Bottomley. Intel TDX Demystified: A Top-Down Approach. ACM Comput. Surv., 56(9):238:1\u2013238:33, 2024.","journal-title":"A Top-Down Approach. ACM Comput. Surv."},{"key":"e_1_3_2_1_39_1","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","year":"2013","unstructured":"Adam Chlipala. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013."},{"key":"e_1_3_2_1_40_1","first-page":"154","volume-title":"Proceedings of the 2010 ACM Symposium on Cloud Computing (SOCC)","author":"Cooper Brian F.","year":"2010","unstructured":"Brian F. Cooper, Adam Silberstein, Erwin Tam, Raghu Ramakrishnan, and Russell Sears. Benchmarking cloud serving systems with YCSB. In Proceedings of the 2010 ACM Symposium on Cloud Computing (SOCC), pages 143\u2013154, 2010."},{"key":"e_1_3_2_1_41_1","volume-title":"IACR Cryptol. ePrint Arch","author":"Costan Victor","year":"2016","unstructured":"Victor Costan and Srinivas Devadas. Intel SGX Explained. IACR Cryptol. ePrint Arch., 2016:86, 2016."},{"key":"e_1_3_2_1_42_1","first-page":"874","volume-title":"Srinivas Devadas. Sanctum: Minimal Hardware Extensions for Strong Software Isolation. In Proceedings of the 25th USENIX Security Symposium","author":"Costan Victor","year":"2016","unstructured":"Victor Costan, Ilia A. Lebedev, and Srinivas Devadas. Sanctum: Minimal Hardware Extensions for Strong Software Isolation. In Proceedings of the 25th USENIX Security Symposium, pages 857\u2013874, 2016."},{"key":"e_1_3_2_1_43_1","first-page":"206","volume-title":"Proceedings of the 20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-XX)","author":"Dautenhahn Nathan","year":"2015","unstructured":"Nathan Dautenhahn, Theodoros Kasampalis, Will Dietz, John Criswell, and Vikram S. Adve. Nested Kernel: An Operating System Architecture for Intra-Kernel Privilege Separation. In Proceedings of the 20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-XX), pages 191\u2013206, 2015."},{"key":"e_1_3_2_1_44_1","first-page":"478","volume-title":"Somesh Jha. FIE on Firmware: Finding Vulnerabilities in Embedded Systems Using Symbolic Execution. In Proceedings of the 22nd USENIX Security Symposium","author":"Davidson Drew","year":"2013","unstructured":"Drew Davidson, Benjamin Moench, Thomas Ristenpart, and Somesh Jha. FIE on Firmware: Finding Vulnerabilities in Embedded Systems Using Symbolic Execution. In Proceedings of the 22nd USENIX Security Symposium, pages 463\u2013478, 2013."},{"key":"e_1_3_2_1_45_1","first-page":"340","volume-title":"Proceeedings of 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS)","author":"de Moura Leonardo Mendon\u00e7a","year":"2008","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj S. Bj\u00f8rner. Z3: An Efficient SMT Solver. In Proceeedings of 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pages 337\u2013340, 2008."},{"key":"e_1_3_2_1_46_1","unstructured":"EEMBC. CoreMark PRO July 2019. v1.1.2743 https:\/\/www.eembc.org\/coremark-pro."},{"key":"e_1_3_2_1_47_1","first-page":"1254","volume-title":"Proceedings of the 29th USENIX Security Symposium","author":"Feng Bo","year":"2020","unstructured":"Bo Feng, Alejandro Mera, and Long Lu. P2IM: Scalable and Hardware-independent Firmware Testing via Automatic Peripheral Interface Modeling. In Proceedings of the 29th USENIX Security Symposium, pages 1237\u20131254, 2020."},{"key":"e_1_3_2_1_48_1","first-page":"294","volume-title":"Haibo Chen. Scalable Memory Protection in the PENGLAI Enclave. In Proceedings of the 15th Symposium on Operating System Design and Implementation (OSDI)","author":"Feng Erhu","year":"2021","unstructured":"Erhu Feng, Xu Lu, Dong Du, Bicheng Yang, Xueqiang Jiang, Yubin Xia, Binyu Zang, and Haibo Chen. Scalable Memory Protection in the PENGLAI Enclave. In Proceedings of the 15th Symposium on Operating System Design and Implementation (OSDI), pages 275\u2013294, 2021."},{"key":"e_1_3_2_1_49_1","first-page":"305","volume-title":"Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP)","author":"Ferraiuolo Andrew","year":"2017","unstructured":"Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pages 287\u2013305, 2017."},{"key":"e_1_3_2_1_50_1","first-page":"25","volume-title":"Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (KISV)","author":"Fiedler Ben","year":"2023","unstructured":"Ben Fiedler, Roman Meier, Jasmin Schult, Daniel Schwyn, and Timothy Roscoe. Specifying the de-facto OS of a production SoC. In Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification (KISV), pages 18\u201325, 2023."},{"key":"e_1_3_2_1_51_1","first-page":"52","volume-title":"Proceedings of The 19th Workshop on Hot Topics in Operating Systems (HotOS-XIX)","author":"Fiedler Ben","year":"2023","unstructured":"Ben Fiedler, Daniel Schwyn, Constantin Gierczak-Galle, David A. Cock, and Timothy Roscoe. Putting out the hardware dumpster fire. In Proceedings of The 19th Workshop on Hot Topics in Operating Systems (HotOS-XIX), pages 46\u201352, 2023."},{"key":"e_1_3_2_1_52_1","first-page":"700","volume-title":"Proceedings of the 16th Symposium on Operating System Design and Implementation (OSDI)","author":"Hof Alexander Van't","year":"2022","unstructured":"Alexander Van't Hof and Jason Nieh. BlackBox: A Container Security Monitor for Protecting Containers on Untrusted Operating Systems. In Proceedings of the 16th Symposium on Operating System Design and Implementation (OSDI), pages 683\u2013700, 2022."},{"key":"e_1_3_2_1_53_1","first-page":"278","volume-title":"Proceedings of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-XVIII)","author":"Hofmann Owen S.","year":"2013","unstructured":"Owen S. Hofmann, Sangman Kim, Alan M. Dunn, Michael Z. Lee, and Emmett Witchel. InkTag: secure applications on an untrusted operating system. In Proceedings of the 18th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-XVIII), pages 265\u2013278, 2013."},{"key":"e_1_3_2_1_54_1","volume-title":"Architecture specification: Intel trust domain extensions (intel tdx) module. https:\/\/software.intel.com\/content\/dam\/develop\/external\/us\/en\/documents\/intel-tdx-module-1eas.pdf","year":"2023","unstructured":"Intel. Architecture specification: Intel trust domain extensions (intel tdx) module. https:\/\/software.intel.com\/content\/dam\/develop\/external\/us\/en\/documents\/intel-tdx-module-1eas.pdf, 2023."},{"key":"e_1_3_2_1_55_1","volume-title":"Intel software guard extensions (intel sgx). https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/software-guard-extensions\/overview.html","year":"2023","unstructured":"Intel. Intel software guard extensions (intel sgx). https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/software-guard-extensions\/overview.html, 2023."},{"key":"e_1_3_2_1_56_1","volume-title":"IOzone Filesystem Benchmark","year":"2006","unstructured":"IOzone.org. IOzone Filesystem Benchmark, 2006."},{"key":"e_1_3_2_1_57_1","first-page":"1","volume-title":"Jackson. Lightweight Formal Methods. In Proceedings of the 2001 International Symposium on Formal Methods Europe","author":"Daniel","year":"2001","unstructured":"Daniel Jackson. Lightweight Formal Methods. In Proceedings of the 2001 International Symposium on Formal Methods Europe, page 1, 2001."},{"key":"e_1_3_2_1_58_1","first-page":"220","volume-title":"Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP)","author":"Klein Gerwin","year":"2009","unstructured":"Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), pages 207\u2013220, 2009."},{"key":"e_1_3_2_1_59_1","first-page":"19","volume-title":"Yuval Yarom. Spectre Attacks: Exploiting Speculative Execution. In IEEE Symposium on Security and Privacy","author":"Kocher Paul","year":"2019","unstructured":"Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. Spectre Attacks: Exploiting Speculative Execution. In IEEE Symposium on Security and Privacy, pages 1\u201319, 2019."},{"key":"e_1_3_2_1_60_1","unstructured":"Alexey Kopytov. Sysbench: Scriptable database and system performance benchmark. https:\/\/github.com\/akopytov\/sysbench."},{"key":"e_1_3_2_1_61_1","volume-title":"Dorami: Privilege Separating Security Monitor on RISC-V TEEs. CoRR, abs\/2410.03653","author":"Kuhne Mark","year":"2024","unstructured":"Mark Kuhne, Stavros Volos, and Shweta Shinde. Dorami: Privilege Separating Security Monitor on RISC-V TEEs. CoRR, abs\/2410.03653, 2024."},{"key":"e_1_3_2_1_62_1","first-page":"16","volume-title":"Proceedings of the 2020 EuroSys Conference","author":"Lee Dayeol","year":"2020","unstructured":"Dayeol Lee, David Kohlbrenner, Shweta Shinde, Krste Asanovic, and Dawn Song. Keystone: an open framework for architecting trusted execution environments. In Proceedings of the 2020 EuroSys Conference, pages 38:1\u201338:16, 2020."},{"key":"e_1_3_2_1_63_1","first-page":"809","volume-title":"Leinenbach and Thomas Santen. Verifying the Microsoft Hyper-V Hypervisor with VCC. In Proceedings of the 16th International Symposium on Formal Methods (FM)","author":"Dirk","year":"2009","unstructured":"Dirk Leinenbach and Thomas Santen. Verifying the Microsoft Hyper-V Hypervisor with VCC. In Proceedings of the 16th International Symposium on Formal Methods (FM), pages 806\u2013809, 2009."},{"key":"e_1_3_2_1_64_1","first-page":"251","volume-title":"Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP)","author":"Levy Amit","year":"2017","unstructured":"Amit Levy, Bradford Campbell, Branden Ghena, Daniel B. Giffin, Pat Pannuto, Prabal Dutta, and Philip Alexander Levis. Multiprogramming a 64kB Computer Safely and Efficiently. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pages 234\u2013251, 2017."},{"key":"e_1_3_2_1_65_1","first-page":"654","volume-title":"Haibing Guan. TwinVisor: Hardware-isolated Confidential Virtual Machines for ARM. In Proceedings of the 28th ACM Symposium on Operating Systems Principles (SOSP)","author":"Li Dingji","year":"2021","unstructured":"Dingji Li, Zeyu Mi, Yubin Xia, Binyu Zang, Haibo Chen, and Haibing Guan. TwinVisor: Hardware-isolated Confidential Virtual Machines for ARM. In Proceedings of the 28th ACM Symposium on Operating Systems Principles (SOSP), pages 638\u2013654, 2021."},{"key":"e_1_3_2_1_66_1","first-page":"1374","volume-title":"Proceedings of the 28th USENIX Security Symposium","author":"Li Shih-Wei","year":"2019","unstructured":"Shih-Wei Li, John S. Koh, and Jason Nieh. Protecting Cloud Virtual Machines from Hypervisor and Host Operating System Exploits. In Proceedings of the 28th USENIX Security Symposium, pages 1357\u20131374, 2019."},{"key":"e_1_3_2_1_67_1","first-page":"3970","volume-title":"Proceedings of the 30th USENIX Security Symposium","author":"Li Shih-Wei","year":"2021","unstructured":"Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. In Proceedings of the 30th USENIX Security Symposium, pages 3953\u20133970, 2021."},{"key":"e_1_3_2_1_68_1","first-page":"484","volume-title":"Gareth Stockwell. Design and Verification of the Arm Confidential Compute Architecture. In Proceedings of the 16th Symposium on Operating System Design and Implementation (OSDI)","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 Proceedings of the 16th Symposium on Operating System Design and Implementation (OSDI), pages 465\u2013484, 2022."},{"key":"e_1_3_2_1_69_1","first-page":"250","volume-title":"Proceedings of the 15th ACM Symposium on Operating Systems Principles (SOSP)","author":"Liedtke Jochen","year":"1995","unstructured":"Jochen Liedtke. On micro-Kernel Construction. In Proceedings of the 15th ACM Symposium on Operating Systems Principles (SOSP), pages 237\u2013250, 1995."},{"key":"e_1_3_2_1_70_1","volume-title":"Proceedings of the 33rd USENIX Security Symposium","author":"Lindenmeier Christian","year":"2024","unstructured":"Christian Lindenmeier, Mathias Payer, and Marcel Busch. EL3XIR: Fuzzing COTS Secure Monitors. In Proceedings of the 33rd USENIX Security Symposium, 2024."},{"key":"e_1_3_2_1_71_1","volume-title":"abs\/1801.01207","author":"Lipp Moritz","year":"2018","unstructured":"Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. Meltdown. CoRR, abs\/1801.01207, 2018."},{"key":"e_1_3_2_1_72_1","first-page":"348","volume-title":"Proceedings of the 17th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-XVII)","author":"Martignoni Lorenzo","year":"2012","unstructured":"Lorenzo Martignoni, Stephen McCamant, Pongsin Poosankam, Dawn Song, and Petros Maniatis. Path-exploration lifting: hi-fi tests for lo-fi emulators. In Proceedings of the 17th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-XVII), pages 337\u2013348, 2012."},{"key":"e_1_3_2_1_73_1","first-page":"158","volume-title":"Adrian Perrig. TrustVisor: Efficient TCB Reduction and Attestation. In IEEE Symposium on Security and Privacy","author":"McCune Jonathan M.","year":"2010","unstructured":"Jonathan M. McCune, Yanlin Li, Ning Qu, Zongwei Zhou, Anupam Datta, Virgil D. Gligor, and Adrian Perrig. TrustVisor: Efficient TCB Reduction and Attestation. In IEEE Symposium on Security and Privacy, pages 143\u2013158, 2010."},{"key":"e_1_3_2_1_74_1","unstructured":"Thomas Meyer-Lehnert. Towards a unified firmware for enzian. B.S. thesis 2024."},{"key":"e_1_3_2_1_75_1","first-page":"7193","volume-title":"Moghimi. Downfall: Exploiting Speculative Data Gathering. In Proceedings of the 32nd USENIX Security Symposium","author":"Daniel","year":"2023","unstructured":"Daniel Moghimi. Downfall: Exploiting Speculative Data Gathering. In Proceedings of the 32nd USENIX Security Symposium, pages 7179\u20137193, 2023."},{"key":"e_1_3_2_1_76_1","first-page":"242","volume-title":"Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP)","author":"Nelson Luke","year":"2019","unstructured":"Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. Scaling symbolic evaluation for automated verification of systems code with Serval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), pages 225\u2013242, 2019."},{"key":"e_1_3_2_1_77_1","first-page":"269","volume-title":"Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP)","author":"Nelson Luke","year":"2017","unstructured":"Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-Button Verification of an OS Kernel. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pages 252\u2013269, 2017."},{"key":"e_1_3_2_1_78_1","volume-title":"Lecture Notes in Computer Science","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science. Springer, 2002."},{"key":"e_1_3_2_1_79_1","volume-title":"Proceedings of the 12th International Workshop on Hardware and Architectural Support for Security and Privacy, HASP2023","author":"Ozga Wojciech","year":"2023","unstructured":"Wojciech Ozga, Guerney D. H. Hunt, Michael V. Le, Elaine R. Palmer, and Avraham Shinnar. Towards a formally verified security monitor for vm-based confidential computing. In Proceedings of the 12th International Workshop on Hardware and Architectural Support for Security and Privacy, HASP2023, 2023."},{"key":"e_1_3_2_1_80_1","first-page":"600","volume-title":"George Candea. Automated Verification of Network Function Binaries. In Proceedings of the 19th Symposium on Networked Systems Design and Implementation (NSDI)","author":"Pirelli Solal","year":"2022","unstructured":"Solal Pirelli, Akvile Valentukonyte, Katerina J. Argyraki, and George Candea. Automated Verification of Network Function Binaries. In Proceedings of the 19th Symposium on Networked Systems Design and Implementation (NSDI), pages 585\u2013600, 2022."},{"issue":"7","key":"e_1_3_2_1_81_1","first-page":"412","volume":"17","author":"Popek Gerald J.","year":"1974","unstructured":"Gerald J. Popek and Robert P. Goldberg. Formal Requirements for Virtualizable Third Generation Architectures. Commun. ACM, 17(7):412\u2013421, 1974.","journal-title":"Goldberg. Formal Requirements for Virtualizable Third Generation Architectures. Commun. ACM"},{"key":"e_1_3_2_1_82_1","first-page":"1867","volume-title":"Cristiano Giuffrida. CrossTalk: Speculative Data Leaks Across Cores Are Real. In Proceedings of the 42nd IEEE Symposium on Security and Privacy (S&P)","author":"Ragab Hany","year":"2021","unstructured":"Hany Ragab, Alyssa Milburn, Kaveh Razavi, Herbert Bos, and Cristiano Giuffrida. CrossTalk: Speculative Data Leaks Across Cores Are Real. In Proceedings of the 42nd IEEE Symposium on Security and Privacy (S&P), pages 1852\u20131867, 2021."},{"key":"e_1_3_2_1_83_1","first-page":"168","volume-title":"Proceedings of the 2016 Formal Methods in Computer-Aided Design Conferenc (FMCAD)","author":"Reid Alastair","year":"2016","unstructured":"Alastair Reid. Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture. In Proceedings of the 2016 Formal Methods in Computer-Aided Design Conferenc (FMCAD), pages 161\u2013168, 2016."},{"key":"e_1_3_2_1_84_1","volume-title":"RISC-V SBI specification. https:\/\/github.com\/riscvnon-isa\/riscv-sbi-doc","author":"Foundation RISC-V","year":"2023","unstructured":"RISC-V Foundation. RISC-V SBI specification. https:\/\/github.com\/riscvnon-isa\/riscv-sbi-doc, 2023."},{"key":"e_1_3_2_1_85_1","volume-title":"RISC-V Supervisor Binary Interface Specification","author":"International RISC-V","year":"2024","unstructured":"RISC-V International. RISC-V Supervisor Binary Interface Specification, 2024. https:\/\/github.com\/riscv-non-isa\/riscv-sbi-doc\/releases\/tag\/vv3.0-rc1."},{"key":"e_1_3_2_1_86_1","first-page":"321","volume-title":"Rajnesh Kanwal. CoVE: Towards Confidential Computing on RISC-V Platforms. In Proceedings of the 20th ACM International Conference on Computing Frontiers (CF)","author":"Sahita Ravi","year":"2023","unstructured":"Ravi Sahita, Vedvyas Shanbhogue, Andrew Bresticker, Atul Khare, Atish Patra, Samuel Ortiz, Dylan Reid, and Rajnesh Kanwal. CoVE: Towards Confidential Computing on RISC-V Platforms. In Proceedings of the 20th ACM International Conference on Computing Frontiers (CF), pages 315\u2013321, 2023."},{"key":"e_1_3_2_1_87_1","first-page":"840","volume-title":"Proceedings of the ACM SIGPLAN 2022 Conference on Programming Language Design and Implementation (PLDI)","author":"Sammler Michael","year":"2022","unstructured":"Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell. Islaris: verification of machine code against authoritative ISA semantics. In Proceedings of the ACM SIGPLAN 2022 Conference on Programming Language Design and Implementation (PLDI), pages 825\u2013840, 2022."},{"key":"e_1_3_2_1_88_1","first-page":"1256","volume-title":"Ali Abbasi. Fuzzware: Using Precise MMIO Modeling for Effective Firmware Fuzzing. In Proceedings of the 31st USENIX Security Symposium","author":"Scharnowski Tobias","year":"2022","unstructured":"Tobias Scharnowski, Nils Bars, Moritz Schloegel, Eric Gustafson, Marius Muench, Giovanni Vigna, Christopher Kruegel, Thorsten Holz, and Ali Abbasi. Fuzzware: Using Precise MMIO Modeling for Effective Firmware Fuzzing. In Proceedings of the 31st USENIX Security Symposium, pages 1239\u20131256, 2022."},{"key":"e_1_3_2_1_89_1","volume-title":"January, 53: 1450\u20131465","author":"Sev-Snp AMD","year":"2020","unstructured":"AMD Sev-Snp. Strengthening vm isolation with integrity protection and more. White Paper, January, 53:1450\u20131465, 2020."},{"key":"e_1_3_2_1_90_1","first-page":"16","volume-title":"Proceedings of the 12th Symposium on Operating System Design and Implementation (OSDI)","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-Button Verification of File Systems via Crash Refinement. In Proceedings of the 12th Symposium on Operating System Design and Implementation (OSDI), pages 1\u201316, 2016."},{"key":"e_1_3_2_1_91_1","first-page":"881","volume-title":"Proceedings of the 28th ACM Symposium on Operating Systems Principles (SOSP)","author":"Tao Runzhou","year":"2021","unstructured":"Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, and Ronghui Gu. Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware. In Proceedings of the 28th ACM Symposium on Operating Systems Principles (SOSP), pages 866\u2013881, 2021."},{"key":"e_1_3_2_1_92_1","first-page":"152","volume-title":"Proceedings of the 2013 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!)","author":"Torlak Emina","year":"2013","unstructured":"Emina Torlak and Rastislav Bod\u00edk. Growing solver-aided languages with rosette. In Proceedings of the 2013 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!), pages 135\u2013152, 2013."},{"issue":"5","key":"e_1_3_2_1_93_1","first-page":"48","volume":"38","author":"Uhlig Richard","year":"2005","unstructured":"Richard Uhlig, Gil Neiger, Dion Rodgers, Amy L. Santoni, Fernando C. M. Martins, Andrew V. Anderson, Steven M. Bennett, Alain K\u00e4gi, Felix H. Leung, and Larry Smith. Intel Virtualization Technology. Computer, 38(5):48\u201356, 2005.","journal-title":"Intel Virtualization Technology. Computer"},{"key":"e_1_3_2_1_94_1","first-page":"330","volume-title":"ICSE (SEIP)","author":"VanHattum Alexa","year":"2022","unstructured":"Alexa VanHattum, Daniel Schwartz-Narbonne, Nathan Chong, and Adrian Sampson. Verifying Dynamic Trait Objects in Rust. In ICSE (SEIP), pages 321\u2013330, 2022."},{"key":"e_1_3_2_1_95_1","first-page":"444","volume-title":"IEEE Symposium on Security and Privacy","author":"Vasudevan Amit","year":"2013","unstructured":"Amit Vasudevan, Sagar Chaki, Limin Jia, Jonathan M. McCune, James Newsome, and Anupam Datta. Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework. In IEEE Symposium on Security and Privacy, pages 430\u2013444, 2013."},{"key":"e_1_3_2_1_96_1","volume-title":"Document Version 20211203. https:\/\/github.com\/riscv\/riscv-isa-manual","author":"Waterman Andrew","year":"2021","unstructured":"Andrew Waterman, Krste Asanovi\u0107, and John Hauser. The RISC-V Instruction Set Manual, Volume II: Privileged Architecture, Document Version 20211203. https:\/\/github.com\/riscv\/riscv-isa-manual, Dec 2021."},{"key":"e_1_3_2_1_97_1","volume-title":"Proceedings of the 1st Safety and Security in Heterogeneous Open System-on-Chip Platforms Workshop (SSH-SoC 2023","author":"Wistoff Nils","year":"2023","unstructured":"Nils Wistoff, Andreas Kuster, Michael Rogenmoser, Robert Balas, Moritz Schneider, and Luca Benini. Protego: A low-overhead open-source i\/o physical memory protection unit for risc-v. In Proceedings of the 1st Safety and Security in Heterogeneous Open System-on-Chip Platforms Workshop (SSH-SoC 2023). SSH-SoC, 2023."},{"key":"e_1_3_2_1_98_1","first-page":"290","volume-title":"Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP)","author":"Zaostrovnykh Arseniy","year":"2019","unstructured":"Arseniy Zaostrovnykh, Solal Pirelli, Rishabh R. Iyer, Matteo Rizzo, Luis Pedrosa, Katerina J. Argyraki, and George Candea. Verifying software network functions with no verification expertise. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), pages 275\u2013290, 2019."},{"key":"e_1_3_2_1_99_1","first-page":"216","volume-title":"Proceedings of the 23rd ACM Symposium on Operating Systems Principles (SOSP)","author":"Zhang Fengzhe","year":"2011","unstructured":"Fengzhe Zhang, Jin Chen, Haibo Chen, and Binyu Zang. CloudVisor: retrofitting protection of virtual machines in multi-tenant cloud with nested virtualization. In Proceedings of the 23rd ACM Symposium on Operating Systems Principles (SOSP), pages 203\u2013216, 2011."}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","location":"Lotte Hotel World Seoul Republic of Korea","acronym":"SOSP '25","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles"],"original-title":[],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:54:56Z","timestamp":1759323296000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3731569.3764826"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,12]]},"references-count":99,"alternative-id":["10.1145\/3731569.3764826","10.1145\/3731569"],"URL":"https:\/\/doi.org\/10.1145\/3731569.3764826","relation":{},"subject":[],"published":{"date-parts":[[2025,10,12]]},"assertion":[{"value":"2025-10-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}