{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:23:42Z","timestamp":1763054622359,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","funder":[{"DOI":"10.13039\/100018696","name":"HORIZON EUROPE Health","doi-asserted-by":"publisher","award":["10109421"],"award-info":[{"award-number":["10109421"]}],"id":[{"id":"10.13039\/100018696","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\/3764860.3768324","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T13:54:43Z","timestamp":1759326883000},"page":"34-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Applying Modern Verification Techniques to a Root-of-Trust Bootloader"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4878-9827","authenticated-orcid":false,"given":"Nicholas","family":"Gordon","sequence":"first","affiliation":[{"name":"Barkhausen Institut, Dresden, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-5124-9513","authenticated-orcid":false,"given":"Carsten","family":"Weinhold","sequence":"additional","affiliation":[{"name":"Barkhausen Institut, Dresden, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/SMC.2017.8122942"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507741"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872371"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729289"},{"key":"e_1_3_2_1_6_1","volume-title":"15th USENIX Symposium on Operating Systems Design and Implementation (OSDI) 21)","author":"Bhardwaj Ankit","year":"2021","unstructured":"Ankit Bhardwaj, Chinmay Kulkarni, Reto Achermann, Irina Calciu, Sanidhya Kashyap, Ryan Stutsman, Amy Tai, and Gerd Zellweger. 2021. NrOS: Effective replication and sharing in an operating system. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI) 21). 295--312."},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the USENIX Security Symposium.","author":"Cai Yi","year":"2025","unstructured":"Yi Cai, Pratap Singh, Zhengyao Lin, Jay Bosamiya, Joshua Gancher, Milijana Surbatovich, Bryan Parno, and Reviewing Model. 2025. Vest: Verified, secure, high-performance parsing and serialization for Rust. In Proceedings of the USENIX Security Symposium."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3625275.3625401"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3698576.3698766"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Chanhee Cho Yi Zhou Jay Bosamiya and Bryan Parno. 2024. A Framework for Debugging Automated Program Verification Proofs via Proof Actions. In Computer Aided Verification Arie Gurfinkel and Vijay Ganesh (Eds.). Springer Nature Switzerland Cham 348--361.","DOI":"10.1007\/978-3-031-65627-9_17"},{"key":"e_1_3_2_1_11_1","volume-title":"Creusot: A Foundry for the Deductive Verification of Rust Programs","author":"Denis Xavier","year":"2022","unstructured":"Xavier Denis, Jacques-Henri Jourdan, and Claude March\u00e9. 2022. Creusot: A Foundry for the Deductive Verification of Rust Programs. In Formal Methods and Software Engineering, Adrian Riesco and Min Zhang (Eds.). Springer International Publishing, Cham, 90--105."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_1_13_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 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. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). USENIX Association, Savannah, GA, 653--669. https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695952"},{"key":"e_1_3_2_1_18_1","volume-title":"PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection. In USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX, USENIX, 839--857","author":"LeBlanc Hayley","year":"2025","unstructured":"Hayley LeBlanc, Jay Lorch, Chris Hawblitzel, Cheng Huang, Yiheng Tao, Nickolai Zeldovich, and Vijay Chidambaram. 2025. PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection. In USENIX Symposium on Operating Systems Design and Implementation (OSDI). USENIX, USENIX, 839--857. https:\/\/www.microsoft.com\/en-us\/research\/publication\/power-never-corrupts-tool-agnostic-verification-of-crash-consistency-and-corruption-detection\/"},{"volume-title":"a proof assistant for higher-order logic","author":"Nipkow Tobias","key":"e_1_3_2_1_19_1","unstructured":"Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. Springer."},{"key":"e_1_3_2_1_20_1","volume-title":"Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"Sun Xudong","year":"2024","unstructured":"Xudong Sun, Wenjie Ma, Jiawei Tyler Gu, Zicheng Ma, Tej Chajed, Jon Howell, Andrea Lattuada, Oded Padon, Lalith Suresh, Adriana Szekeres, and Tianyin Xu. 2024. Anvil: Verifying Liveness of Cluster Management Controllers. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX Association, Santa Clara, CA, 649--666. https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/sun-xudong"},{"key":"e_1_3_2_1_21_1","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Tao Zhe","year":"2021","unstructured":"Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani, and Aditya V Thakur. 2021. DICE*: A formally verified implementation of DICE measured boot. In 30th USENIX Security Symposium (USENIX Security 21). 1091--1107."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2024. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.14542673","DOI":"10.5281\/zenodo.14542673"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510457.3513031"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-99984-0_5"},{"key":"e_1_3_2_1_25_1","volume-title":"VeriSMo: A Verified Security Module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"Zhou Ziqiao","year":"2024","unstructured":"Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, and Weidong Cui. 2024. VeriSMo: A Verified Security Module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24). USENIX Association, Santa Clara, CA, 599--614. https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/zhou"}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Seoul Republic of Korea","acronym":"SOSP '25"},"container-title":["Proceedings of the 13th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764860.3768324","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:20:30Z","timestamp":1763054430000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3764860.3768324"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,13]]},"references-count":25,"alternative-id":["10.1145\/3764860.3768324","10.1145\/3764860"],"URL":"https:\/\/doi.org\/10.1145\/3764860.3768324","relation":{},"subject":[],"published":{"date-parts":[[2025,10,13]]},"assertion":[{"value":"2025-10-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}