{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T01:45:20Z","timestamp":1740102320650,"version":"3.37.3"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","funder":[{"DOI":"10.13039\/https:\/\/doi.org\/10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2313411","1837127"],"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.3625401","type":"proceedings-article","created":{"date-parts":[[2023,10,20]],"date-time":"2023-10-20T13:09:57Z","timestamp":1697807397000},"page":"9-17","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Atmosphere: Towards Practical Verified Kernels in Rust"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-4001-9105","authenticated-orcid":false,"given":"Xiangdong","family":"Chen","sequence":"first","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7789-8005","authenticated-orcid":false,"given":"Zhaofeng","family":"Li","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-3259-1282","authenticated-orcid":false,"given":"Lukas","family":"Mesicek","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6274-9242","authenticated-orcid":false,"given":"Vikram","family":"Narayanan","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8769-8373","authenticated-orcid":false,"given":"Anton","family":"Burtsev","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, United States of America"}]}],"member":"320","published-online":{"date-parts":[[2023,10,23]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"The Coq proof assistant. https:\/\/coq.inria.fr\/. The Coq proof assistant. https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_2_1","volume-title":"London","author":"Department of Defense Trusted Computer System Evaluation Criteria, pages 1--129.","year":"1985","unstructured":"Department of Defense Trusted Computer System Evaluation Criteria, pages 1--129. Palgrave Macmillan UK , London , 1985 . Department of Defense Trusted Computer System Evaluation Criteria, pages 1--129. Palgrave Macmillan UK, London, 1985."},{"key":"e_1_3_2_1_3_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1007\/978-3-030-01090-4_32","volume-title":"Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA)","author":"Baranowski Marek","year":"2018","unstructured":"Marek Baranowski , Shaobo He , and Zvonimir Rakamaric . Verifying rust programs with smack . In Shuvendu K. Lahiri and Chao Wang, editors, Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA) , volume 11138 of Lecture Notes in Computer Science , pages 528 -- 535 . Springer , 2018 . Marek Baranowski, Shaobo He, and Zvonimir Rakamaric. Verifying rust programs with smack. In Shuvendu K. Lahiri and Chao Wang, editors, Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 11138 of Lecture Notes in Computer Science, pages 528--535. Springer, 2018."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005","author":"Barnett Mike","year":"2006","unstructured":"Mike Barnett , Bor-Yuh Evan Chang , Robert DeLine , Bart Jacobs , and K. Rustan M. Leino . Boogie : A modular reusable verifier for object-oriented programs. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors , Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005 , pages 364 -- 387 , Berlin, Heidelberg , 2006 . Springer Berlin Heidelberg. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, pages 364--387, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg."},{"key":"e_1_3_2_1_5_1","first-page":"295","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 . Nros : Effective replication and sharing in an operating system . In 15th USENIX Symposium on Operating Systems Design and Implementation, OSDI '21 , pages 295 -- 312 . USENIX Association , July 2021 . Ankit Bhardwaj, Chinmay Kulkarni, Reto Achermann, Irina Calciu, Sanidhya Kashyap, Ryan Stutsman, Amy Tai, and Gerd Zellweger. Nros: Effective replication and sharing in an operating system. In 15th USENIX Symposium on Operating Systems Design and Implementation, OSDI '21, pages 295--312. USENIX Association, July 2021."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3593856.3595899"},{"key":"e_1_3_2_1_7_1","first-page":"313","volume-title":"Proceedings of the 2009 USENIX Annual Technical Conference (USENIX ATC'09)","author":"Burtsev Anton","year":"2009","unstructured":"Anton Burtsev , Kiran Srinivasan , Prashanth Radhakrishnan , Lakshmi N Bairavasundaram , Kaladhar Voruganti , and Garth R Goodson . Fido : Fast inter-virtual-machine communication for enterprise appliances . In Proceedings of the 2009 USENIX Annual Technical Conference (USENIX ATC'09) , pages 313 -- 326 , 2009 . Anton Burtsev, Kiran Srinivasan, Prashanth Radhakrishnan, Lakshmi N Bairavasundaram, Kaladhar Voruganti, and Garth R Goodson. Fido: Fast inter-virtual-machine communication for enterprise appliances. In Proceedings of the 2009 USENIX Annual Technical Conference (USENIX ATC'09), pages 313--326, 2009."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1109\/INFOCOM.2008.36","volume-title":"IEEE INFOCOM 2008 - The 27th Conference on Computer Communications","author":"de Bruijn W.","year":"2008","unstructured":"W. de Bruijn and H. Bos . Beltway buffers: Avoiding the os traffic jam . In IEEE INFOCOM 2008 - The 27th Conference on Computer Communications , pages 136 -- 140 , 2008 . W. de Bruijn and H. Bos. Beltway buffers: Avoiding the os traffic jam. In IEEE INFOCOM 2008 - The 27th Conference on Computer Communications, pages 136--140, 2008."},{"key":"e_1_3_2_1_9_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","volume":"4963","author":"de Moura Leonardo","year":"2008","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . Z3 : An efficient SMT solver . In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , volume 4963 of Lecture Notes in Computer Science, pages 337--340. Springer , 2008 . Leonardo de Moura and Nikolaj Bj\u00f8rner. Z3: An efficient SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of Lecture Notes in Computer Science, pages 337--340. Springer, 2008."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"de Moura Leonardo","year":"2015","unstructured":"Leonardo de Moura , Soonho Kong , Jeremy Avigad , Floris van Doorn , and Jakob von Raumer . The lean theorem prover (system description) . In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 , pages 378 -- 388 , Cham, 2015 . Springer International Publishing . Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, pages 378--388, Cham, 2015. Springer International Publishing."},{"key":"e_1_3_2_1_11_1","first-page":"133","volume-title":"Proceedings of the 24th ACM Symposium on Operating Systems Principles, SOSP '13","author":"Elphinstone Kevin","year":"2013","unstructured":"Kevin Elphinstone and Gernot Heiser . From L3 to SeL4 What Have We Learnt in 20 Years of L4 Microkernels? In Proceedings of the 24th ACM Symposium on Operating Systems Principles, SOSP '13 , pages 133 -- 150 , 2013 . Kevin Elphinstone and Gernot Heiser. From L3 to SeL4 What Have We Learnt in 20 Years of L4 Microkernels? In Proceedings of the 24th ACM Symposium on Operating Systems Principles, SOSP '13, pages 133--150, 2013."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ANCS.2019.8901892"},{"key":"e_1_3_2_1_13_1","unstructured":"Mozilla Foundation. The Rust programming language. https:\/\/doc.rust-lang.org\/book\/. Mozilla Foundation. The Rust programming language. https:\/\/doc.rust-lang.org\/book\/."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1983.1654440"},{"key":"e_1_3_2_1_15_1","volume-title":"1st Workshop on Operating System and Architectural Support for the on demand IT InfraStructure, OASIS","author":"Fraser K.","year":"2004","unstructured":"K. Fraser , S. Hand , R. Neugebauer , I. Pratt , A. Warfield , and M. Williamson . Safe hardware access with the Xen virtual machine monitor . In 1st Workshop on Operating System and Architectural Support for the on demand IT InfraStructure, OASIS 2004 . K. Fraser, S. Hand, R. Neugebauer, I. Pratt, A. Warfield, and M. Williamson. Safe hardware access with the Xen virtual machine monitor. In 1st Workshop on Operating System and Architectural Support for the on demand IT InfraStructure, OASIS 2004."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1109\/SP.1984.10002","volume-title":"1984 IEEE Symposium on Security and Privacy","author":"Gold B. D.","year":"1984","unstructured":"B. D. Gold , R. R. Linde , and P. F. Cudney . Kvm\/370 in retrospect . In 1984 IEEE Symposium on Security and Privacy , pages 13 -- 23 , 1984 . B. D. Gold, R. R. Linde, and P. F. Cudney. Kvm\/370 in retrospect. In 1984 IEEE Symposium on Security and Privacy, pages 13--23, 1984."},{"key":"e_1_3_2_1_17_1","first-page":"3","volume-title":"Proceedings of the Second Asia-Pacific Workshop on Systems, APSys '11","author":"Gu L.","year":"2011","unstructured":"L. Gu , A. Vaynberg , B. Ford , Z. Shao , and D. Costanzo . CertiKOS: a certified kernel for secure cloud computing . In Proceedings of the Second Asia-Pacific Workshop on Systems, APSys '11 , page 3 , 2011 . L. Gu, A. Vaynberg, B. Ford, Z. Shao, and D. Costanzo. CertiKOS: a certified kernel for secure cloud computing. In Proceedings of the Second Asia-Pacific Workshop on Systems, APSys '11, page 3, 2011."},{"key":"e_1_3_2_1_18_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 , Savannah, GA , November 2016 . USENIX Association. 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, Savannah, GA, November 2016. USENIX Association."},{"key":"e_1_3_2_1_19_1","first-page":"911","volume-title":"17th USENIX Symposium on Operating Systems Design and Implementation, OSDI '23","author":"Hance Travis","year":"2023","unstructured":"Travis Hance , Yi Zhou , Andrea Lattuada , Reto Achermann , Alex Conway , Ryan Stutsman , Gerd Zellweger , Chris Hawblitzel , Jon Howell , and Bryan Parno . Sharding the state machine: Automated modular reasoning for complex concurrent systems . In 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI '23 , pages 911 -- 929 , Boston, MA , July 2023 . USENIX Association. Travis Hance, Yi Zhou, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell, and Bryan Parno. Sharding the state machine: Automated modular reasoning for complex concurrent systems. In 17th USENIX Symposium on Operating Systems Design and Implementation, OSDI '23, pages 911--929, Boston, MA, July 2023. USENIX Association."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_21_1","first-page":"165","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation, OSDI '14","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 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI '14 , pages 165 -- 181 , Broomfield, CO , October 2014 . USENIX Association. 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 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI '14, pages 165--181, Broomfield, CO, October 2014. USENIX Association."},{"key":"e_1_3_2_1_22_1","volume-title":"Rustbelt: Securing the foundations of the rust programming language","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 . volume 2 , New York, NY , USA, December 2017 . Association for Computing Machinery . Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. Rustbelt: Securing the foundations of the rust programming language. volume 2, New York, NY, USA, December 2017. Association for Computing Machinery."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.106971"},{"key":"e_1_3_2_1_24_1","volume-title":"No Starch Press","author":"Klabnik Steve","year":"2019","unstructured":"Steve Klabnik and Carol Nichols . The Rust Programming Language . No Starch Press , 2019 . Steve Klabnik and Carol Nichols. The Rust Programming Language. No Starch Press, 2019."},{"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","volume-title":"Proceedings of the ACM on Programming Languages, 7(OOPSLA1):85:286--85:315","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 . Proceedings of the ACM on Programming Languages, 7(OOPSLA1):85:286--85:315 , April 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. Proceedings of the ACM on Programming Languages, 7(OOPSLA1):85:286--85:315, April 2023."},{"key":"e_1_3_2_1_27_1","volume-title":"16th International Conference, LPAR-16","author":"Leino Rustan","year":"2010","unstructured":"Rustan Leino . Dafny : An automatic program verifier for functional correctness . In 16th International Conference, LPAR-16 , Dakar, Senegal, pages 348--370. Springer Berlin Heidelberg , April 2010 . Rustan Leino. Dafny: An automatic program verifier for functional correctness. In 16th International Conference, LPAR-16, Dakar, Senegal, pages 348--370. Springer Berlin Heidelberg, April 2010."},{"key":"e_1_3_2_1_28_1","volume-title":"The compcert c verified compiler: Documentation and user's manual","author":"Leroy Xavier","year":"2014","unstructured":"Xavier Leroy . The compcert c verified compiler: Documentation and user's manual . September 2014 . Xavier Leroy. The compcert c verified compiler: Documentation and user's manual. September 2014."},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the ACM on Programming Languages, 6(OOPSLA1):1--28","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 . Proceedings of the ACM on Programming Languages, 6(OOPSLA1):1--28 , April 2022 . Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, and Chris Hawblitzel. Linear types for large-scale systems verification. Proceedings of the ACM on Programming Languages, 6(OOPSLA1):1--28, April 2022."},{"key":"e_1_3_2_1_30_1","first-page":"3953","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 Zhuang Hui . Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor . In 30th USENIX Security Symposium (USENIX Security 21) , pages 3953 -- 3970 , August 2021 . Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, and John Zhuang Hui. Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. In 30th USENIX Security Symposium (USENIX Security 21), pages 3953--3970, August 2021."},{"key":"e_1_3_2_1_31_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. 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_32_1","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1145\/3132747.3132748","volume-title":"Proceedings of the 26th Symposium on Operating Systems Principles, SOSP '17","author":"Nelson Luke","year":"2017","unstructured":"Luke Nelson , Helgi Sigurbjarnarson , Kaiyuan Zhang , Dylan Johnson , James Bornholt , Emina Torlak , and Xi Wang . Hyperkernel : Pushbutton verification of an os kernel . In Proceedings of the 26th Symposium on Operating Systems Principles, SOSP '17 , page 252 -- 269 , New York, NY, USA , 2017 . Association for Computing Machinery. Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Pushbutton verification of an os kernel. In Proceedings of the 26th Symposium on Operating Systems Principles, SOSP '17, page 252--269, New York, NY, USA, 2017. Association for Computing Machinery."},{"key":"e_1_3_2_1_33_1","first-page":"203","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation, OSDI '16","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 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI '16 , pages 203 -- 216 , Savannah, GA , November 2016 . Aurojit Panda, Sangjin Han, Keon Jang, Melvin Walls, Sylvia Ratnasamy, and Scott Shenker. NetBricks: Taking the V out of NFV. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI '16, pages 203--216, Savannah, GA, November 2016."},{"key":"e_1_3_2_1_34_1","volume-title":"Proceedings of the 6th Asia-Pacific Workshop on Systems, APSys '15","author":"Peters Sean","year":"2015","unstructured":"Sean Peters , Adrian Danis , Kevin Elphinstone , and Gernot Heiser . For a Microkernel, a Big Lock Is Fine . In Proceedings of the 6th Asia-Pacific Workshop on Systems, APSys '15 , New York, NY, USA , 2015 . Association for Computing Machinery. Sean Peters, Adrian Danis, Kevin Elphinstone, and Gernot Heiser. For a Microkernel, a Big Lock Is Fine. In Proceedings of the 6th Asia-Pacific Workshop on Systems, APSys '15, New York, NY, USA, 2015. Association for Computing Machinery."},{"key":"e_1_3_2_1_35_1","volume-title":"December","author":"Ricci Robert","year":"2014","unstructured":"Robert Ricci , Eric Eide , and The CloudLab Team . Introducing CloudLab: Scientific infrastructure for advancing cloud architectures and applications. USENIX ;login:, 39(6) , December 2014 . Robert Ricci, Eric Eide, and The CloudLab Team. Introducing CloudLab: Scientific infrastructure for advancing cloud architectures and applications. USENIX ;login:, 39(6), December 2014."},{"key":"e_1_3_2_1_36_1","first-page":"238","volume-title":"Proceedings of the 11th National Computer Security Conference","author":"Schockley W. R.","year":"1988","unstructured":"W. R. Schockley , T. F. Tao , and M. F. Thompson . An overview of the gemsos class a1 technology and application experience . In Proceedings of the 11th National Computer Security Conference , pages 238 -- 245 , October 1988 . W. R. Schockley, T. F. Tao, and M. F. Thompson. An overview of the gemsos class a1 technology and application experience. In Proceedings of the 11th National Computer Security Conference, pages 238--245, October 1988."},{"key":"e_1_3_2_1_37_1","first-page":"256","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16","author":"Swamy Nikhil","year":"2016","unstructured":"Nikhil Swamy , Catalin Hri\u0163cu , Chantal Keller , Aseem Rastogi , Antoine Delignat-Lavaud , Simon Forest , Karthikeyan Bhargavan , C\u00e9dric Fournet , Pierre-Yves Strub , Markulf Kohlweiss , Jean-Karim Zinzindohoue , and Santiago Zanella-B\u00e9guelin . Dependent types and multi-monadic effects in f* . In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16 , page 256 -- 270 , New York, NY, USA , 2016 . Association for Computing Machinery. Nikhil Swamy, Catalin Hri\u0163cu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, C\u00e9dric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-B\u00e9guelin. Dependent types and multi-monadic effects in f*. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, page 256--270, New York, NY, USA, 2016. Association for Computing Machinery."},{"key":"e_1_3_2_1_38_1","volume-title":"New Type Idiom. https:\/\/doc.rust-lang.org\/rust-by-example\/generics\/new_types.html","author":"Project The Rust","year":"2023","unstructured":"The Rust Project . New Type Idiom. https:\/\/doc.rust-lang.org\/rust-by-example\/generics\/new_types.html , 2023 . The Rust Project. New Type Idiom. https:\/\/doc.rust-lang.org\/rust-by-example\/generics\/new_types.html, 2023."},{"key":"e_1_3_2_1_39_1","volume-title":"Returning mutable references. https:\/\/github.com\/verus-lang\/verus\/discussions\/35","author":"Contributors The Verus","year":"2023","unstructured":"The Verus Contributors . Returning mutable references. https:\/\/github.com\/verus-lang\/verus\/discussions\/35 , 2023 . The Verus Contributors. Returning mutable references. https:\/\/github.com\/verus-lang\/verus\/discussions\/35, 2023."},{"key":"e_1_3_2_1_40_1","first-page":"59","volume-title":"Computer Aided Verification","author":"Xu Fengwei","year":"2016","unstructured":"Fengwei Xu , Ming Fu , Xinyu Feng , Xiaoran Zhang , Hui Zhang , and Zhaohui Li . A practical verification framework for preemptive os kernels . In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification , pages 59 -- 79 , Cham, 2016 . Springer International Publishing . Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang, and Zhaohui Li. A practical verification framework for preemptive os kernels. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification, pages 59--79, Cham, 2016. Springer International Publishing."},{"key":"e_1_3_2_1_41_1","first-page":"99","volume-title":"Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '10","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 Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '10 , pages 99 -- 110 , New York, NY, USA , 2010 . Jean Yang and Chris Hawblitzel. Safe to the last instruction: Automated verification of a type-safe operating system. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '10, pages 99--110, New York, NY, USA, 2010."},{"key":"e_1_3_2_1_42_1","first-page":"275","volume-title":"George Candea. Verifying Software Network Functions with No Verification Expertise. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19","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 Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19 , page 275 -- 290 , New York, NY, USA , 2019 . Association for Computing Machinery. Arseniy Zaostrovnykh, Solal Pirelli, Rishabh Iyer, Matteo Rizzo, Luis Pedrosa, Katerina Argyraki, and George Candea. Verifying Software Network Functions with No Verification Expertise. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19, page 275--290, New York, NY, USA, 2019. Association for Computing Machinery."}],"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":[],"deposited":{"date-parts":[[2023,10,20]],"date-time":"2023-10-20T13:10:20Z","timestamp":1697807420000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3625275.3625401"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,23]]},"references-count":42,"alternative-id":["10.1145\/3625275.3625401","10.1145\/3625275"],"URL":"https:\/\/doi.org\/10.1145\/3625275.3625401","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"}}]}}