{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:58:54Z","timestamp":1750309134326,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T00:00:00Z","timestamp":1698019200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/https:\/\/doi.org\/10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2130257","2112562"],"award-info":[{"award-number":["2130257","2112562"]}],"id":[{"id":"10.13039\/https:\/\/doi.org\/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":[[2023,10,23]]},"DOI":"10.1145\/3625275.3625398","type":"proceedings-article","created":{"date-parts":[[2023,10,20]],"date-time":"2023-10-20T13:09:57Z","timestamp":1697807397000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Leveraging Rust for Lightweight OS Correctness"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-6184-5298","authenticated-orcid":false,"given":"Ramla","family":"Ijaz","sequence":"first","affiliation":[{"name":"Yale University, New Haven, CT, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-6423-214X","authenticated-orcid":false,"given":"Kevin","family":"Boos","sequence":"additional","affiliation":[{"name":"Theseus Systems, Bellevue, WA, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0840-167X","authenticated-orcid":false,"given":"Lin","family":"Zhong","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,23]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Prose Proofs for Invariants in the Theseus OS. https:\/\/github.com\/Ramla-I\/theseus_proofs. Accessed: 2023-10-07.  Prose Proofs for Invariants in the Theseus OS. https:\/\/github.com\/Ramla-I\/theseus_proofs. Accessed: 2023-10-07."},{"key":"e_1_3_2_1_2_1","unstructured":"Struct std::sync::Arc. https:\/\/doc.rust-lang.org\/std\/sync\/struct.Arc.html. Accessed: 2023-08-02.  Struct std::sync::Arc. https:\/\/doc.rust-lang.org\/std\/sync\/struct.Arc.html. Accessed: 2023-08-02."},{"key":"e_1_3_2_1_3_1","unstructured":"Struct std::sync::Mutex. https:\/\/doc.rust-lang.org\/std\/sync\/struct.Mutex.html. Accessed: 2023-08-02.  Struct std::sync::Mutex. https:\/\/doc.rust-lang.org\/std\/sync\/struct.Mutex.html. Accessed: 2023-08-02."},{"key":"e_1_3_2_1_4_1","unstructured":"Struct std::vec::Vec. https:\/\/doc.rust-lang.org\/std\/vec\/struct.Vec.html. Accessed: 2023-08-02.  Struct std::vec::Vec. https:\/\/doc.rust-lang.org\/std\/vec\/struct.Vec.html. Accessed: 2023-08-02."},{"key":"e_1_3_2_1_5_1","unstructured":"Verus Tutorial and Reference. https:\/\/verus-lang.github.io\/verus\/guide\/. Accessed: 2023-08-04.  Verus Tutorial and Reference. https:\/\/verus-lang.github.io\/verus\/guide\/. Accessed: 2023-08-04."},{"key":"e_1_3_2_1_6_1","volume-title":"Proc. ACM OOPSLA","author":"Astrauskas Vytautas","year":"2019","unstructured":"Vytautas Astrauskas , Peter M\u00fcller , Federico Poli , and Alexander J Summers . Leveraging Rust types for modular specification and verification . In Proc. ACM OOPSLA , 2019 . Vytautas Astrauskas, Peter M\u00fcller, Federico Poli, and Alexander J Summers. Leveraging Rust types for modular specification and verification. In Proc. ACM OOPSLA, 2019."},{"key":"e_1_3_2_1_7_1","volume-title":"Proc. Workshp. Hot Topics in Operating Systems (HotOS)","author":"Balasubramanian Abhiram","year":"2017","unstructured":"Abhiram Balasubramanian , Marek S. Baranowski , Anton Burtsev , Aurojit Panda , Zvonimir Rakamari\u0107 , and Leonid Ryzhyk . System programming in Rust: Beyond safety . In Proc. Workshp. Hot Topics in Operating Systems (HotOS) , 2017 . Abhiram Balasubramanian, Marek S. Baranowski, Anton Burtsev, Aurojit Panda, Zvonimir Rakamari\u0107, and Leonid Ryzhyk. System programming in Rust: Beyond safety. In Proc. Workshp. Hot Topics in Operating Systems (HotOS), 2017."},{"key":"e_1_3_2_1_8_1","volume-title":"Proc. USENIX OSDI","author":"Boos Kevin","year":"2020","unstructured":"Kevin Boos , Namitha Liyanage , Ramla Ijaz , and Lin Zhong . Theseus : an experiment in operating system structure and state management . In Proc. USENIX OSDI , 2020 . Kevin Boos, Namitha Liyanage, Ramla Ijaz, and Lin Zhong. Theseus: an experiment in operating system structure and state management. In Proc. USENIX OSDI, 2020."},{"key":"e_1_3_2_1_9_1","volume-title":"HotOS","author":"Brun Matthias","year":"2023","unstructured":"Matthias Brun , Reto Achermann , Tej Chajed , Jon Howell , Gerd Zellweger , and Andrea Lattuada . Beyond isolation : Os verification as a foundation for correct applications . In HotOS , 2023 . Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger, and Andrea Lattuada. Beyond isolation: Os verification as a foundation for correct applications. In HotOS, 2023."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512532"},{"key":"e_1_3_2_1_11_1","volume-title":"Proc. USENIX OSDI","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan Newman Wu , Jieung Kim , Vilhelm Sjoberg , and David Costanzo . CertiKOS : An extensible architecture for building certified concurrent OS kernels . In Proc. USENIX OSDI , 2016 . Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sjoberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proc. USENIX OSDI, 2016."},{"key":"e_1_3_2_1_12_1","volume-title":"Proc. ACM SOSP","author":"Hawblitzel Chris","year":"2015","unstructured":"Chris Hawblitzel , Jon Howell , Manos Kapritsos , Jacob R Lorch , Bryan Parno , Michael L Roberts , Srinath Setty , and Brian Zill . IronFleet : proving practical distributed systems correct . In Proc. ACM SOSP , 2015 . Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Michael L Roberts, Srinath Setty, and Brian Zill. IronFleet: proving practical distributed systems correct. In Proc. ACM SOSP, 2015."},{"key":"e_1_3_2_1_13_1","volume-title":"Proc. USENIX OSDI","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel , Jon Howell , Jacob R Lorch , Arjun Narayan , Bryan Parno , Danfeng Zhang , and Brian Zill . Ironclad apps : End-to-end security via automated full-system verification . In Proc. USENIX OSDI , 2014 . Chris Hawblitzel, Jon Howell, Jacob R Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. Ironclad apps: End-to-end security via automated full-system verification. In Proc. USENIX OSDI, 2014."},{"key":"e_1_3_2_1_14_1","volume":"200","author":"Hunt Galen C.","unstructured":"Galen C. Hunt and James R. Larus . Singularity: Rethinking the software stack. ACM SIGOPS Operating Systems Review , 200 7. Galen C. Hunt and James R. Larus. Singularity: Rethinking the software stack. ACM SIGOPS Operating Systems Review, 2007.","journal-title":"ACM SIGOPS Operating Systems Review"},{"key":"e_1_3_2_1_15_1","volume-title":"Proc ACM SIGPLAN Wrkshp. Generic Programming","author":"Laumann Jespersen Thomas Bracht","year":"2015","unstructured":"Thomas Bracht Laumann Jespersen , Philip Munksgaard , and Ken Friis Larsen . Session types for Rust . In Proc ACM SIGPLAN Wrkshp. Generic Programming , 2015 . Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. Session types for Rust. In Proc ACM SIGPLAN Wrkshp. Generic Programming, 2015."},{"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","volume-title":"Proc. USENIX OSDI","author":"Kulkarni Chinmay","year":"2018","unstructured":"Chinmay Kulkarni , Sara Moore , Mazhar Naqvi , Tian Zhang , Robert Ricci , and Ryan Stutsman . Splinter:bare-metal extensions for multi-tenant low-latency storage . In Proc. USENIX OSDI , 2018 . Chinmay Kulkarni, Sara Moore, Mazhar Naqvi, Tian Zhang, Robert Ricci, and Ryan Stutsman. Splinter:bare-metal extensions for multi-tenant low-latency storage. In Proc. USENIX OSDI, 2018."},{"key":"e_1_3_2_1_18_1","volume-title":"Proc. ACM OOPSLA","author":"Lattuada Andrea","year":"2023","unstructured":"Andrea Lattuada , Travis Hance , Chanhee Cho , Matthias Brun , Isitha Subasinghe , Yi Zhou , Jon Howell , Bryan Parno , and Chris Hawblitzel . Verus : Verifying rust programs using linear ghost types . In Proc. ACM OOPSLA , 2023 . Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying rust programs using linear ghost types. In Proc. ACM OOPSLA, 2023."},{"key":"e_1_3_2_1_19_1","volume-title":"Proc. ACM OOPSLA","author":"Li Jialin","year":"2022","unstructured":"Jialin Li , Andrea Lattuada , Yi Zhou , Jonathan Cameron , Jon Howell , Bryan Parno , and Chris Hawblitzel . Linear types for large-scale systems verification . In Proc. ACM OOPSLA , 2022 . Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel. Linear types for large-scale systems verification. In Proc. ACM OOPSLA, 2022."},{"key":"e_1_3_2_1_20_1","volume-title":"Proc. USENIX Security","author":"Liu Jian","year":"2022","unstructured":"Jian Liu , Lin Yi , Weiteng Chen , Chengyu Song , Zhiyun Qian , and Qiuping Yi. LinKRID : Vetting imbalance reference counting in linux kernel with symbolic execution . In Proc. USENIX Security , 2022 . Jian Liu, Lin Yi, Weiteng Chen, Chengyu Song, Zhiyun Qian, and Qiuping Yi. LinKRID: Vetting imbalance reference counting in linux kernel with symbolic execution. In Proc. USENIX Security, 2022."},{"key":"e_1_3_2_1_21_1","volume-title":"Proc. ACM ASPLOS","author":"Mao Junjie","year":"2016","unstructured":"Junjie Mao , Yu Chen , Qixue Xiao , and Yuanchun Shi . RID : finding reference count bugs with inconsistent path pair checking . In Proc. ACM ASPLOS , 2016 . Junjie Mao, Yu Chen, Qixue Xiao, and Yuanchun Shi. RID: finding reference count bugs with inconsistent path pair checking. In Proc. ACM ASPLOS, 2016."},{"key":"e_1_3_2_1_22_1","volume-title":"USENIX ATC","author":"McVoy Larry W","year":"1996","unstructured":"Larry W McVoy , Carl Staelin , : Portable tools for performance analysis . In USENIX ATC , 1996 . Larry W McVoy, Carl Staelin, et al. lmbench: Portable tools for performance analysis. In USENIX ATC, 1996."},{"key":"e_1_3_2_1_24_1","volume-title":"Proc. USENIX OSDI","author":"Narayanan Vikram","year":"2020","unstructured":"Vikram Narayanan , Tianjiao Huang , David Detweiler , Dan Appel , Zhaofeng Li , Gerd Zellweger , and Anton Burtsev. RedLeaf : Isolation and communication in a safe operating system . In Proc. USENIX OSDI , 2020 . Vikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel, Zhaofeng Li, Gerd Zellweger, and Anton Burtsev. RedLeaf: Isolation and communication in a safe operating system. In Proc. USENIX OSDI, 2020."},{"key":"e_1_3_2_1_25_1","volume-title":"Proc. ACM 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 Proc. ACM SOSP , 2019 . 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 Proc. ACM SOSP, 2019."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_27_1","volume-title":"Proc. USENIX OSDI","author":"Panda Aurojit","year":"2016","unstructured":"Aurojit Panda , Sangjin Han , Keon Jang , Melvin Walls , Sylvia Ratnasamy , and Scott Shenker . NetBricks : Taking the V out of NFV . In Proc. USENIX OSDI , 2016 . Aurojit Panda, Sangjin Han, Keon Jang, Melvin Walls, Sylvia Ratnasamy, and Scott Shenker. NetBricks: Taking the V out of NFV. In Proc. USENIX OSDI, 2016."},{"key":"e_1_3_2_1_28_1","volume-title":"Proc. USENIX 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 Proc. USENIX OSDI , 2016 . Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. Push-Button verification of file systems via crash refinement. In Proc. USENIX OSDI, 2016."},{"key":"e_1_3_2_1_29_1","volume-title":"Proc. USENIX OSDI","author":"Sigurbjarnarson Helgi","year":"2018","unstructured":"Helgi Sigurbjarnarson , Luke Nelson , Bruno Castro-Karney , James Bornholt , Emina Torlak , and Xi Wang . Nickel : A framework for design and verification of information flow control systems . In Proc. USENIX OSDI , 2018 . Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. Nickel: A framework for design and verification of information flow control systems. In Proc. USENIX OSDI, 2018."},{"key":"e_1_3_2_1_30_1","volume-title":"J-Kernel: A capability-based operating system for Java. Secure Internet programming","author":"Eicken Thorsten Von","year":"1999","unstructured":"Thorsten Von Eicken , Chi-Chao Chang , Grzegorz Czajkowski , Chris Hawblitzel , Deyu Hu , and Dan Spoonhower . J-Kernel: A capability-based operating system for Java. Secure Internet programming , 1999 . Thorsten Von Eicken, Chi-Chao Chang, Grzegorz Czajkowski, Chris Hawblitzel, Deyu Hu, and Dan Spoonhower. J-Kernel: A capability-based operating system for Java. Secure Internet programming, 1999."},{"key":"e_1_3_2_1_31_1","volume-title":"Proc. ACM ASPLOS","author":"Xu Chao","year":"2015","unstructured":"Chao Xu , Xiaozhu Lin , Yuyang Wang , and Lin Zhong . Automated OS-level device runtime power management . In Proc. ACM ASPLOS , 2015 . Chao Xu, Xiaozhu Lin, Yuyang Wang, and Lin Zhong. Automated OS-level device runtime power management. In Proc. ACM ASPLOS, 2015."},{"key":"e_1_3_2_1_32_1","volume-title":"Proc. ACM PLDI","author":"Yang Jean","year":"2010","unstructured":"Jean Yang and Chris Hawblitzel . Safe to the last instruction: automated verification of a type-safe operating system . In Proc. ACM PLDI , 2010 . Jean Yang and Chris Hawblitzel. Safe to the last instruction: automated verification of a type-safe operating system. In Proc. ACM PLDI, 2010."},{"key":"e_1_3_2_1_33_1","volume-title":"Proc. ACM SOSP","author":"Zaostrovnykh Arseniy","year":"2019","unstructured":"Arseniy Zaostrovnykh , Solal Pirelli , Rishabh Iyer , Matteo Rizzo , Luis Pedrosa , Katerina Argyraki , and George Candea . Verifying software network functions with no verification expertise . In Proc. ACM SOSP , 2019 . Arseniy Zaostrovnykh, Solal Pirelli, Rishabh Iyer, Matteo Rizzo, Luis Pedrosa, Katerina Argyraki, and George Candea. Verifying software network functions with no verification expertise. In Proc. ACM SOSP, 2019."}],"event":{"name":"KISV '23: 1st Workshop on Kernel Isolation, Safety and Verification","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"],"location":"Koblenz Germany","acronym":"KISV '23"},"container-title":["Proceedings of the 1st Workshop on Kernel Isolation, Safety and Verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3625275.3625398","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:50:04Z","timestamp":1750287004000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3625275.3625398"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,23]]},"references-count":32,"alternative-id":["10.1145\/3625275.3625398","10.1145\/3625275"],"URL":"https:\/\/doi.org\/10.1145\/3625275.3625398","relation":{},"subject":[],"published":{"date-parts":[[2023,10,23]]},"assertion":[{"value":"2023-10-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}