{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:56:47Z","timestamp":1756000607531,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,6,22]],"date-time":"2023-06-22T00:00:00Z","timestamp":1687392000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,6,22]]},"DOI":"10.1145\/3593856.3595899","type":"proceedings-article","created":{"date-parts":[[2023,6,22]],"date-time":"2023-06-22T22:20:41Z","timestamp":1687472441000},"page":"158-165","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Beyond isolation: OS verification as a foundation for correct applications"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-5349-4347","authenticated-orcid":false,"given":"Matthias","family":"Brun","sequence":"first","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3263-7236","authenticated-orcid":false,"given":"Reto","family":"Achermann","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9889-4828","authenticated-orcid":false,"given":"Tej","family":"Chajed","sequence":"additional","affiliation":[{"name":"VMware Research, Palo Alto, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1781-2473","authenticated-orcid":false,"given":"Jon","family":"Howell","sequence":"additional","affiliation":[{"name":"VMware Research, Seattle, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1197-595X","authenticated-orcid":false,"given":"Gerd","family":"Zellweger","sequence":"additional","affiliation":[{"name":"VMware Research, Palo Alto, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9303-452X","authenticated-orcid":false,"given":"Andrea","family":"Lattuada","sequence":"additional","affiliation":[{"name":"VMware Research, Z\u00fcrich, Switzerland"}]}],"member":"320","published-online":{"date-parts":[[2023,6,22]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_1_1","DOI":"10.1145\/2954679.2872404"},{"key":"e_1_3_2_1_2_1","volume-title":"Operating Systems: Three Easy Pieces","author":"Arpaci-Dusseau R. H.","year":"2018","unstructured":"Arpaci-Dusseau, R. H., and Arpaci-Dusseau, A. C. Operating Systems: Three Easy Pieces. Arpaci-Dusseau Books, 2018."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1145\/3341301.3359661"},{"key":"e_1_3_2_1_4_1","first-page":"29","volume-title":"Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (New York, NY, USA, 2009), SOSP '09, Association for Computing Machinery","author":"Baumann A.","unstructured":"Baumann, A., Barham, P., Dagand, P.-E., Harris, T., Isaacs, R., Peter, S., Roscoe, T., Sch\u00fcpbach, A., and Singhania, A. The multikernel: A new os architecture for scalable multicore systems. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (New York, NY, USA, 2009), SOSP '09, Association for Computing Machinery, p. 29--44."},{"key":"e_1_3_2_1_5_1","first-page":"207","volume-title":"Proceedings of the 24th USENIX Conference on Security Symposium (USA, 2015), SEC'15, USENIX Association","author":"Beringer L.","unstructured":"Beringer, L., Petcher, A., Ye, K. Q., and Appel, A. W. Verified correctness and security of openssl hmac. In Proceedings of the 24th USENIX Conference on Security Symposium (USA, 2015), SEC'15, USENIX Association, p. 207--221."},{"key":"e_1_3_2_1_6_1","first-page":"295","volume-title":"15th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2021","author":"Bhardwaj A.","year":"2021","unstructured":"Bhardwaj, A., Kulkarni, C., Achermann, R., Calciu, I., Kashyap, S., Stutsman, R., Tai, A., and Zellweger, G. Nros: Effective replication and sharing in an operating system. In 15th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2021, July 14--16, 2021 (2021), A. D. Brown and J. R. Lorch, Eds., USENIX Association, pp. 295--312."},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the USENIX Security Symposium (August","author":"Bond B.","year":"2017","unstructured":"Bond, B., Hawblitzel, C., Kapritsos, M., Leino, R., Lorch, J., Parno, B., Rane, A., Setty, S., and Thompson, L. Vale: Verifying high-performance cryptographic assembly code. In Proceedings of the USENIX Security Symposium (August 2017), USENIX."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1145\/3477132.3483540"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.1145\/3037697.3037721"},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI '22)","author":"Chajed T.","year":"2022","unstructured":"Chajed, T., Tassarotti, J., Theng, M., Kaashoek, M. F., and Zeldovich, N. Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning. In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI '22) (July 2022)."},{"key":"e_1_3_2_1_11_1","first-page":"18","volume-title":"Proceedings of the 25th Symposium on Operating Systems Principles (New York, NY, USA, 2015), SOSP '15, Association for Computing Machinery","author":"Chen H.","unstructured":"Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M. F., and Zeldovich, N. Using crash hoare logic for certifying the fscq file system. In Proceedings of the 25th Symposium on Operating Systems Principles (New York, NY, USA, 2015), SOSP '15, Association for Computing Machinery, p. 18--37."},{"key":"e_1_3_2_1_12_1","volume":"32","author":"Clements A. T.","unstructured":"Clements, A. T., Kaashoek, M. F., Zeldovich, N., Morris, R. T., and Kohler, E. The scalable commutativity rule: Designing scalable software for multicore processors. ACM Trans. Comput. Syst. 32, 4 (jan 2015).","journal-title":"ACM Trans. Comput. Syst."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.1145\/2908080.2908100"},{"key":"e_1_3_2_1_14_1","first-page":"4","author":"Drepper U.","year":"2005","unstructured":"Drepper, U. Futexes are tricky. Futexes are Tricky, Red Hat Inc, Japan 4 (2005).","journal-title":"Japan"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_15_1","DOI":"10.1145\/3064176.3064183"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_16_1","DOI":"10.1145\/945445.945450"},{"key":"e_1_3_2_1_17_1","first-page":"653","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016","author":"Gu R.","year":"2016","unstructured":"Gu, R., Shao, Z., Chen, H., Wu, X. N., Kim, J., Sj\u00f6berg, V., and Costanzo, D. Certikos: An extensible architecture for building certified concurrent OS kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2--4, 2016 (2016), K. Keeton and T. Roscoe, Eds., USENIX Association, pp. 653--669."},{"key":"e_1_3_2_1_18_1","first-page":"99","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020","author":"Hance T.","year":"2020","unstructured":"Hance, T., Lattuada, A., Hawblitzel, C., Howell, J., Johnson, R., and Parno, B. Storage systems are distributed systems (so verify them that way!). In 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020, Virtual Event, November 4--6, 2020 (2020), USENIX Association, pp. 99--115."},{"key":"e_1_3_2_1_19_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) [To Appear] (July","author":"Hance T.","year":"2023","unstructured":"Hance, T., Zhou, Y., Lattuada, A., Achermann, R., Conway, A., Stutsman, R., Zellweger, G., Hawblitzel, C., Howell, J., and Parno, B. Sharding the state machine: Automated modular reasoning for complex concurrent systems. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI) [To Appear] (July 2023)."},{"key":"e_1_3_2_1_20_1","first-page":"1","volume-title":"Proceedings of the 25th Symposium on Operating Systems Principles (New York, NY, USA, 2015), SOSP '15, ACM","author":"Hawblitzel C.","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J. R., Parno, B., Roberts, M. L., Setty, S., and Zill, B. IronFleet: Proving practical distributed systems correct. In Proceedings of the 25th Symposium on Operating Systems Principles (New York, NY, USA, 2015), SOSP '15, ACM, pp. 1--17."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_21_1","DOI":"10.1145\/2676726.2676980"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1145\/1629575.1629596"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.1145\/3586037"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_25_1","DOI":"10.1145\/3527313"},{"key":"e_1_3_2_1_26_1","first-page":"3953","volume-title":"30th USENIX Security Symposium, USENIX Security 2021","author":"Li S.","year":"2021","unstructured":"Li, S., Li, X., Gu, R., Nieh, J., and Hui, J. Z. Formally verified memory protection for a commodity multiprocessor hypervisor. In 30th USENIX Security Symposium, USENIX Security 2021, August 11--13, 2021 (2021), M. Bailey and R. Greenstadt, Eds., USENIX Association, pp. 3953--3970."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_27_1","DOI":"10.1109\/SP40001.2021.00049"},{"key":"e_1_3_2_1_28_1","first-page":"197","volume-title":"Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (New York, NY, USA, 2020), PLDI 2020, Association for Computing Machinery","author":"Lorch J. R.","unstructured":"Lorch, J. R., Chen, Y., Kapritsos, M., Parno, B., Qadeer, S., Sharma, U., Wilcox, J. R., and Zhao, X. Armada: Low-effort verification of high-performance concurrent programs. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (New York, NY, USA, 2020), PLDI 2020, Association for Computing Machinery, p. 197--210."},{"key":"e_1_3_2_1_29_1","first-page":"103","volume-title":"Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology (New York, NY, USA, 2014), HILT '14, ACM","author":"Matsakis N. D.","unstructured":"Matsakis, N. D., and Klock, II, F. S. The rust language. In Proceedings of the 2014 ACM SIGAda Annual Conference on High Integrity Language Technology (New York, NY, USA, 2014), HILT '14, ACM, pp. 103--104."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_30_1","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_2_1_31_1","first-page":"225","volume-title":"ACM","author":"Nelson L.","unstructured":"Nelson, L., Bornholt, J., Gu, R., Baumann, A., Torlak, E., and Wang, X. Scaling symbolic evaluation for automated verification of systems code with serval. In SOSP (2019), ACM, pp. 225--242."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_32_1","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_33_1","volume-title":"A formally-verified framework for fair synchronization in kotlin coroutines. CoRR","author":"Nikita Koval","year":"2021","unstructured":"Nikita Koval, Dmitry Khalanskiy, and Dan Alistarh. A formally-verified framework for fair synchronization in kotlin coroutines. CoRR (2021)."},{"key":"e_1_3_2_1_34_1","first-page":"585","volume-title":"19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22)","author":"Pirelli S.","year":"2022","unstructured":"Pirelli, S., Valentukonyt\u0117, A., Argyraki, K., and Candea, G. Automated verification of network function binaries. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22) (Renton, WA, Apr. 2022), USENIX Association, pp. 585--600."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_35_1","DOI":"10.1145\/3477132.3483560"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_36_1","DOI":"10.1145\/1531793.1531805"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_37_1","DOI":"10.1145\/1806596.1806610"}],"event":{"sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"acronym":"HOTOS '23","name":"HotOS '23: 19th Workshop on Hot Topics in Operating Systems","location":"Providence RI USA"},"container-title":["Proceedings of the 19th Workshop on Hot Topics in Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3593856.3595899","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3593856.3595899","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:50Z","timestamp":1750178870000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3593856.3595899"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,22]]},"references-count":36,"alternative-id":["10.1145\/3593856.3595899","10.1145\/3593856"],"URL":"https:\/\/doi.org\/10.1145\/3593856.3595899","relation":{},"subject":[],"published":{"date-parts":[[2023,6,22]]},"assertion":[{"value":"2023-06-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}