{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:52:12Z","timestamp":1773193932555,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":67,"publisher":"ACM","funder":[{"DOI":"10.13039\/100008536","name":"Amazon Web Services","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100008536","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.3764821","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:43:24Z","timestamp":1759322604000},"page":"752-767","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Atmosphere: Practical Verified Kernels with Rust and Verus"],"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"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-0450-1297","authenticated-orcid":false,"given":"Jerry","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6274-9242","authenticated-orcid":false,"given":"Vikram","family":"Narayanan","sequence":"additional","affiliation":[{"name":"Palo Alto Networks, Santa Clara, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,12]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP)","author":"Klein Gerwin","year":"2009","unstructured":"Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Raftal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP), October 11, 2009."},{"key":"e_1_3_2_1_2_1","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","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), 2016."},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (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 Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2010."},{"key":"e_1_3_2_1_4_1","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation (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 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI), October 2014."},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the 25th Symposium on Operating Systems Principles (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. Iron-Fleet: Proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles (SOSP), 2015."},{"key":"e_1_3_2_1_6_1","volume-title":"Logic for Programming, Artificial Intelligence","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, 2010."},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the 26th 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: Pushbutton verification of an OS kernel. In Proceedings of the 26th Symposium on Operating Systems Principles (SOSP), October 14, 2017."},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the 12th USENIX Symposium on Operating Systems 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 USENIX Symposium on Operating Systems Design and Implementation (OSDI), November 2016."},{"key":"e_1_3_2_1_9_1","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), 2019."},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"Padon Oded","year":"2016","unstructured":"Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. Ivy: Safety verification by interactive generalization. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2016."},{"key":"e_1_3_2_1_11_1","volume-title":"Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (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 Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI), October 2018."},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles (SOSP)","author":"Cebeci Can","year":"2024","unstructured":"Can Cebeci, Yonghao Zou, Diyu Zhou, George Candea, and Cl\u00e9ment Pit-Claudel. Practical verification of system-software components written in standard C. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles (SOSP), 2024."},{"key":"e_1_3_2_1_13_1","volume-title":"Linear types can change the world! In Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, number 4","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler. Linear types can change the world! In Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, number 4, 1990."},{"key":"e_1_3_2_1_14_1","volume-title":"OOPSLA1","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, OOPSLA1, April 6, 2023."},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of the ACM on Programming Languages, (OOPSLA1)","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, (OOPSLA1), April 2022."},{"key":"e_1_3_2_1_16_1","volume-title":"Proc. ACM Program. Lang., (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. Proc. ACM Program. Lang., (OOPSLA), October 2019."},{"key":"e_1_3_2_1_17_1","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"Bornat Richard","year":"2005","unstructured":"Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. Permission accounting in separation logic. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2005."},{"key":"e_1_3_2_1_18_1","volume-title":"Verification, Model Checking","author":"M\u00fcller Peter","year":"2016","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In Verification, Model Checking, and Abstract Interpretation, 2016."},{"key":"e_1_3_2_1_19_1","volume-title":"NASA Formal Methods","author":"Astrauskas Vytautas","year":"2022","unstructured":"Vytautas Astrauskas, Aurel B\u00edl\u00fd, Jon\u00e1\u0161 Fiala, Zachary Grannan, Christoph Matheja, Peter M\u00fcller, Federico Poli, and Alexander J. Summers. The Prusti Project: Formal verification for Rust. In NASA Formal Methods, 2022."},{"key":"e_1_3_2_1_20_1","volume-title":"Proc. ACM Program. Lang., POPL","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. Proc. ACM Program. Lang., POPL, December 27, 2017."},{"key":"e_1_3_2_1_21_1","volume-title":"April 27, 2025. url: https:\/\/microkerneldude.org\/2025\/04\/27\/benchmarking-crimes-meet-formal-verification\/.","author":"Heiser Gernot","unstructured":"Gernot Heiser. Benchmarking crimes meet formal verification, April 27, 2025. url: https:\/\/microkerneldude.org\/2025\/04\/27\/benchmarking-crimes-meet-formal-verification\/."},{"key":"e_1_3_2_1_22_1","unstructured":"Verus-Lang. Recursive exec and proof functions proofs by induction. url: https:\/\/verus-lang.github.io\/verus\/guide\/induction.html."},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of the 26th Symposium on Operating Systems Principles","author":"Levy Amit","year":"2017","unstructured":"Amit Levy, Bradford Campbell, Branden Ghena, Daniel B. Giffin, Pat Pannuto, Prabal Dutta, and Philip Levis. Multiprogramming a 64kB computer safely and efficiently. In Proceedings of the 26th Symposium on Operating Systems Principles (Shanghai, China) (SOSP), 2017."},{"key":"e_1_3_2_1_24_1","volume-title":"18th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zhou Ziqiao","year":"2024","unstructured":"Ziqiao Zhou, Anjali, Weiteng Chen, Sishuai Gong, Chris Hawblitzel, and Weidong Cui. VeriSMo: A verified security module for Confidential VMs. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2024."},{"key":"e_1_3_2_1_25_1","volume-title":"Proceedings of the 19th Workshop on Hot Topics in Operating Systems (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 Proceedings of the 19th Workshop on Hot Topics in Operating Systems (HOTOS), June 22, 2023."},{"key":"e_1_3_2_1_26_1","unstructured":"Verus-Lang. A verified doubly-linked list example in Verus. url: https:\/\/github.com\/verus-lang\/verus\/blob\/main\/examples\/doubly_linked.rs."},{"key":"e_1_3_2_1_27_1","unstructured":"The Rust Project. Reference cycles can leak memory. url: https:\/\/doc.rust-lang.org\/book\/ch15-06-reference-cycles.html."},{"key":"e_1_3_2_1_28_1","unstructured":"The Coq proof assistant. url: https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_29_1","volume-title":"A Proof Assistant for Higher-Order Logic (Lecture Notes in Computer Science)","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic (Lecture Notes in Computer Science). 2002."},{"key":"e_1_3_2_1_30_1","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 Automated Deduction - CADE-25, 2015."},{"key":"e_1_3_2_1_31_1","volume-title":"Proceedings of the 30th Symposium on Operating Systems Principles (SOSP). ACM","author":"Lattuada Andrea","year":"2024","unstructured":"Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. Verus: A practical foundation for systems verification. In Proceedings of the 30th Symposium on Operating Systems Principles (SOSP). ACM, November 2024."},{"key":"e_1_3_2_1_32_1","volume-title":"Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"Swamy Nikhil","year":"2016","unstructured":"Nikhil Swamy, C\u0103t\u0103lin 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), 2016."},{"key":"e_1_3_2_1_33_1","volume-title":"Proceedings of the 4th international conference on Formal Methods for Components and Objects (FMCO)","author":"Barnett Mike","year":"2005","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 Proceedings of the 4th international conference on Formal Methods for Components and Objects (FMCO), 2005."},{"key":"e_1_3_2_1_34_1","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science)","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) (Lecture Notes in Computer Science), 2008."},{"key":"e_1_3_2_1_35_1","volume-title":"Journal of Functional Programming","author":"O'Connor Liam","year":"2021","unstructured":"Liam O'Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sidney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, and Gabriele Keller. Cogent: Uniqueness types and certifying compilation. Journal of Functional Programming, 2021."},{"key":"e_1_3_2_1_36_1","volume-title":"Formal Methods and Software Engineering","author":"Denis Xavier","year":"2022","unstructured":"Xavier Denis, Jacques-Henri Jourdan, and Claude March\u00e9. Creusot: A foundry for the deductive verification of Rust programs. In Formal Methods and Software Engineering, 2022."},{"key":"e_1_3_2_1_37_1","volume-title":"Proc. ACM Program. Lang., (ICFP)","author":"Ho Son","year":"2022","unstructured":"Son Ho and Jonathan Protzenko. Aeneas: Rust verification by functional translation. Proc. ACM Program. Lang., (ICFP), August 2022."},{"key":"e_1_3_2_1_38_1","volume-title":"Static Analysis","author":"Boyland John","year":"2003","unstructured":"John Boyland. Checking interference with fractional permissions. In Static Analysis, 2003."},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the Applied Networking Research Workshop (ANRW)","author":"Emmerich Paul","year":"2018","unstructured":"Paul Emmerich, Maximilian Pudelko, Simon Bauer, and Georg Carle. User space network drivers. In Proceedings of the Applied Networking Research Workshop (ANRW), 2018."},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation (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 Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2020."},{"key":"e_1_3_2_1_41_1","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (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 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), November 2016."},{"key":"e_1_3_2_1_42_1","volume-title":"1st Workshop on Operating System and Architectural Support for the on Demand IT InfraStructure (OASIS)","author":"Fraser Keir","year":"2004","unstructured":"Keir Fraser, Steven Hand, Rolf Neugebauer, Ian Pratt, Andrew Warfield, Mark Williamson, et al. 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_43_1","volume-title":"INFOCOM","author":"de Bruijn Willem","year":"2008","unstructured":"Willem de Bruijn and Herbert Bos. Beltway buffers: Avoiding the OS traffic jam. In INFOCOM, 2008."},{"key":"e_1_3_2_1_44_1","volume-title":"2009 USENIX Annual Technical Conference (ATC)","author":"Burtsev Anton","year":"2009","unstructured":"Anton Burtsev, Kiran Srinivasan, Prashanth Radhakrishnan, Kaladhar Voruganti, and Garth R. Goodson. Fido: Fast inter-virtual-machine communication for enterprise appliances. In 2009 USENIX Annual Technical Conference (ATC), June 2009."},{"key":"e_1_3_2_1_45_1","volume-title":"Proceedings of the 26th 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 Symposium on Operating Systems Principles (SOSP), 2017."},{"key":"e_1_3_2_1_46_1","volume-title":"transitivity, and channel-control security policies","author":"Rushby John","year":"1992","unstructured":"John Rushby. Noninterference, transitivity, and channel-control security policies. 1992."},{"key":"e_1_3_2_1_47_1","volume-title":"1984 IEEE Symposium on Security and Privacy","author":"Joseph","year":"1984","unstructured":"Joseph A. Goguen and Jose Meseguer. Unwinding and inference control. In 1984 IEEE Symposium on Security and Privacy, 1984."},{"key":"e_1_3_2_1_48_1","author":"Nelson Luke","year":"2020","unstructured":"Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Noninterference specifications for secure systems. SIGOPS Oper. Syst. Rev., (1), August 2020.","journal-title":"SIGOPS Oper. Syst. Rev., (1)"},{"key":"e_1_3_2_1_49_1","volume-title":"December","author":"Ricci Robert","year":"2014","unstructured":"Robert Ricci, Eric Eide, and The CloudLab Team. Introducing Cloud-Lab: Scientific infrastructure for advancing cloud architectures and applications. USENIX ;login: (6), December 2014."},{"key":"e_1_3_2_1_50_1","unstructured":"CloudLab hardware info. url: https:\/\/docs.cloudlab.us\/hardware.html."},{"key":"e_1_3_2_1_51_1","volume-title":"Proceedings of the 30th USENIX Security Symposium. 30th USENIX Security Symposium (USENIX Security)","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. 30th USENIX Security Symposium (USENIX Security), 2021."},{"key":"e_1_3_2_1_52_1","unstructured":"Recursive proof in Verified NrOS page table. url: https:\/\/github.com\/matthias-brun\/verified-nrkernel\/blob\/8f30cf0f910e7606c3a0f633821acfdfde410cf4\/page-table\/impl_u\/l2_impl.rs#L947-L1562."},{"key":"e_1_3_2_1_53_1","unstructured":"DPDK: Data Plane Development Kit. url: https:\/\/www.dpdk.org."},{"key":"e_1_3_2_1_54_1","unstructured":"Intel Corporation. Storage Performance Development Kit (SPDK). url: https:\/\/spdk.io."},{"key":"e_1_3_2_1_55_1","volume-title":"Proceedings of the 13th USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Eisenbud Daniel E.","year":"2016","unstructured":"Daniel E. Eisenbud, Cheng Yi, Carlo Contavalli, Cody Smith, Roman Kononov, Eric Mann-Hielscher, Ardas Cilingiroglu, Bin Cheyney, Wentao Shang, and Jinnah Dylan Hosein. Maglev: A fast and reliable software network load balancer. In Proceedings of the 13th USENIX Symposium on Networked Systems Design and Implementation (NSDI), March 2016."},{"key":"e_1_3_2_1_56_1","volume-title":"Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Nishtala Rajesh","year":"2013","unstructured":"Rajesh Nishtala, Hans Fugal, Steven Grimm, Marc Kwiatkowski, Herman Lee, Harry C. Li, Ryan McElroy, Mike Paleczny, Daniel Peek, Paul Saab, David Stafford, Tony Tung, and Venkateshwaran Venkataramani. Scaling memcache at Facebook. In Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI), April 2013."},{"key":"e_1_3_2_1_57_1","volume-title":"Proceedings of the 21st ACM SIGOPS Symposium on Operating Systems Principles (SOSP)","author":"DeCandia Giuseppe","year":"2007","unstructured":"Giuseppe DeCandia, Deniz Hastorun, Madan Jampani, Gunavardhan Kakulapati, Avinash Lakshman, Alex Pilchin, Swaminathan Sivasubramanian, Peter Vosshall, and Werner Vogels. Dynamo: Amazon's highly available key-value store. In Proceedings of the 21st ACM SIGOPS Symposium on Operating Systems Principles (SOSP), 2007."},{"key":"e_1_3_2_1_58_1","unstructured":"NGINX. NGINX: High performance load balancer web server and reverse proxy. url: https:\/\/www.nginx.com."},{"key":"e_1_3_2_1_59_1","unstructured":"wrk - a HTTP benchmarking tool. url: https:\/\/github.com\/wg\/wrk."},{"key":"e_1_3_2_1_60_1","volume-title":"The 'Orange Book' Series.","author":"Department of defense trusted computer system evaluation criteria.","year":"1985","unstructured":"Department of defense trusted computer system evaluation criteria. In The 'Orange Book' Series. 1985."},{"key":"e_1_3_2_1_61_1","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, 1984."},{"key":"e_1_3_2_1_62_1","author":"Karger P.A.","year":"1991","unstructured":"P.A. Karger, M.E. Zurko, D.W. Bonin, A.H. Mason, and C.E. Kahn. A retrospective on the VAX VMM security kernel. IEEE Transactions on Software Engineering, (11), 1991.","journal-title":"A retrospective on the VAX VMM security kernel. IEEE Transactions on Software Engineering, (11)"},{"key":"e_1_3_2_1_63_1","volume-title":"July","author":"Fraim L. J.","year":"1983","unstructured":"L. J. Fraim. Scomp: A solution to the multilevel security problem. Computer, (7), July 1983."},{"key":"e_1_3_2_1_64_1","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, October 1988."},{"key":"e_1_3_2_1_65_1","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 Computer Aided Verification, 2016."},{"key":"e_1_3_2_1_66_1","unstructured":"The UNSAT group. Hyperkernel git repository. url: https:\/\/github.com\/uw-unsat\/hyperkernel."},{"key":"e_1_3_2_1_67_1","volume-title":"15th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","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), July 2021."}],"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:11Z","timestamp":1759323251000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3731569.3764821"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,12]]},"references-count":67,"alternative-id":["10.1145\/3731569.3764821","10.1145\/3731569"],"URL":"https:\/\/doi.org\/10.1145\/3731569.3764821","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"}}]}}