research-article

Beyond isolation: OS verification as a foundation for correct applications

Authors:

Reto Achermann,

Gerd Zellweger,

Andrea LattuadaAuthors Info & Claims

HOTOS '23: Proceedings of the 19th Workshop on Hot Topics in Operating Systems

Pages 158 - 165

https://doi.org/10.1145/3593856.3595899

Published: 22 June 2023 Publication History

Abstract

Verified systems software has generally had to assume the correctness of the operating system and its provided services (like networking and the file system). Even though there exist verified operating systems and file systems, the specifications for these components do not compose with applications to produce a fully verified high-performance software stack.

In this position paper, we lay out our vision for what it would look like to have a verified OS with verified applications, all with good multi-core performance. We've explored a part of the verification by proving a page table correct already, but the larger goal is to lay out a vision for an ambitious project that supports an application verified from its high-level specification down to the hardware.

References

[1]

Amani, S., Hixon, A., Chen, Z., Rizkallah, C., Chubb, P., O'Connor, L., Beeren, J., Nagashima, Y., Lim, J., Sewell, T., Tuong, J., Keller, G., Murray, T., Klein, G., and Heiser, G. Cogent: Verifying high-assurance file system implementations. SIGPLAN Not. 51, 4 (mar 2016), 175--188.

Digital Library

[2]

Arpaci-Dusseau, R. H., and Arpaci-Dusseau, A. C. Operating Systems: Three Easy Pieces. Arpaci-Dusseau Books, 2018.

[3]

Athalye, A., Belay, A., Kaashoek, M. F., Morris, R., and Zeldovich, N. Notary: A device for secure transaction approval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP 2019) (Hunstville, ON, Canada, Oct. 2019).

Digital Library

[4]

Baumann, A., Barham, P., Dagand, P.-E., Harris, T., Isaacs, R., Peter, S., Roscoe, T., Schüpbach, 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.

[5]

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.

[6]

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.

[7]

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.

[8]

Bornholt, J., Joshi, R., Astrauskas, V., Cully, B., Kragl, B., Markle, S., Sauri, K., Schleit, D., Slatton, G., Tasiran, S., Geffen, J. V., and Warfield, A. Using lightweight formal methods to validate a key-value storage node in amazon S3. In SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles, Virtual Event / Koblenz, Germany, October 26--29, 2021 (2021), R. van Renesse and N. Zeldovich, Eds., ACM, pp. 836--850.

Digital Library

[9]

Calciu, I., Sen, S., Balakrishnan, M., and Aguilera, M. K. Black-box Concurrent Data Structures for NUMA Architectures. In Proceedings of the ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2017).

Digital Library

[10]

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).

[11]

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.

[12]

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).

[13]

Costanzo, D., Shao, Z., and Gu, R. End-to-end verification of information-flow security for C and assembly programs. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13--17, 2016 (2016), C. Krintz and E. D. Berger, Eds., ACM, pp. 648--664.

Digital Library

[14]

Drepper, U. Futexes are tricky. Futexes are Tricky, Red Hat Inc, Japan 4 (2005).

[15]

Fonseca, P., Zhang, K., Wang, X., and Krishnamurthy, A. An empirical study on the correctness of formally verified distributed systems. In Proceedings of the Twelfth European Conference on Computer Systems, EuroSys 2017, Belgrade, Serbia, April 23--26, 2017 (2017), G. Alonso, R. Bianchini, and M. Vukolic, Eds., ACM, pp. 328--343.

Digital Library

[16]

Ghemawat, S., Gobioff, H., and Leung, S.-T. The Google file system. In Proceedings of the Nineteenth ACM Symposium on Operating Systems Principles (New York, NY, USA, 2003), SOSP '03, Association for Computing Machinery, p. 29--43.

Digital Library

[17]

Gu, R., Shao, Z., Chen, H., Wu, X. N., Kim, J., Sjöberg, 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.

[18]

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.

[19]

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).

[20]

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.

[21]

Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., and Dreyer, D. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15--17, 2015 (2015), S. K. Rajamani and D. Walker, Eds., ACM, pp. 637--650.

Digital Library

[22]

Kantee, A. Flexible Operating System Internals: The Design and Implementation of the Anykernel and Rump Kernels. PhD thesis, Aalto University, 2012.

[23]

Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., and Winwood, S. sel4: formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11--14, 2009 (2009), J. N. Matthews and T. E. Anderson, Eds., ACM, pp. 207--220.

Digital Library

[24]

Lattuada, A., Hance, T., Cho, C., Brun, M., Subasinghe, I., Zhou, Y., Howell, J., Parno, B., and Hawblitzel, C. Verus: Verifying rust programs using linear ghost types. Proc. ACM Program. Lang. 7, OOPSLA1 (2023), 286--315.

Digital Library

[25]

Li, J., Lattuada, A., Zhou, Y., Cameron, J., Howell, J., Parno, B., and Hawblitzel, C. Linear types for large-scale systems verification. Proc. ACM Program. Lang. 6, OOPSLA1 (2022), 1--28.

Digital Library

[26]

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.

[27]

Li, S., Li, X., Gu, R., Nieh, J., and Hui, J. Z. A secure and formally verified Linux KVM hypervisor. In 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24--27 May 2021 (2021), IEEE, pp. 1782--1799.

[28]

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.

[29]

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.

[30]

Murray, T. C., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., and Klein, G. sel4: From general purpose to a proof of information flow enforcement. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19--22, 2013 (2013), IEEE Computer Society, pp. 415--429.

Digital Library

[31]

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.

[32]

Nelson, L., Sigurbjarnarson, H., Zhang, K., Johnson, D., Bornholt, J., Torlak, E., and Wang, X. Hyperkernel: Push-button verification of an OS kernel. In Proceedings of the 26th Symposium on Operating Systems Principles, Shanghai, China, October 28--31, 2017 (2017), ACM, pp. 252--269.

Digital Library

[33]

Nikita Koval, Dmitry Khalanskiy, and Dan Alistarh. A formally-verified framework for fair synchronization in kotlin coroutines. CoRR (2021).

[34]

Pirelli, S., Valentukonytė, 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.

[35]

Tao, R., Yao, J., Li, X., Li, S., Nieh, J., and Gu, R. Formal verification of a multiprocessor hypervisor on arm relaxed memory hardware. In SOSP '21: ACM SIGOPS 28th Symposium on Operating Systems Principles, Virtual Event / Koblenz, Germany, October 26--29, 2021 (2021), R. van Renesse and N. Zeldovich, Eds., ACM, pp. 866--881.

Digital Library

[36]

Wentzlaff, D., and Agarwal, A. Factored operating systems (fos): The case for a scalable operating system for multicores. SIGOPS Oper. Syst. Rev. 43, 2 (apr 2009), 76--85.

Digital Library

[37]

Yang, J., and Hawblitzel, C. Safe to the last instruction: automated verification of a type-safe operating system. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5--10, 2010 (2010), B. G. Zorn and A. Aiken, Eds., ACM, pp. 99--110.

Digital Library

Cited By

Liu JHao XArpaci-Dusseau AArpaci-Dusseau RChajed T(2024)Shadow Filesystems: Recovering from Filesystem Runtime Errors via Robust Alternative ExecutionProceedings of the 16th ACM Workshop on Hot Topics in Storage and File Systems10.1145/3655038.3665942(15-22)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3655038.3665942

Recommendations

Beyond verification: leveraging formal for debugging
DAC '09: Proceedings of the 46th Annual Design Automation Conference

The latest advancements in the commercial formal model checkers have enabled the integration of formal property verification with the conventional testbench based methods in the overall verification plan. This has led to significant verification ...
Beyond safety: customized SAT-based model checking
DAC '05: Proceedings of the 42nd annual Design Automation Conference

Model checking of safety properties has taken a significant lead over non-safety properties in recent years. To bridge the gap, we propose dedicated SAT-based model checking algorithms for properties beyond safety. Previous bounded model checking (BMC) ...
Software Verification of Hyperproperties Beyond k-Safety
Computer Aided Verification
Abstract
Temporal hyperproperties are system properties that relate multiple execution traces. For (finite-state) hardware, temporal hyperproperties are supported by model checking algorithms, and tools for general temporal logics like HyperLTL exist. For (... $^{}^{}$ $^{}^{}$

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

HOTOS '23: Proceedings of the 19th Workshop on Hot Topics in Operating Systems

June 2023

247 pages

ISBN:9798400701955

DOI:10.1145/3593856

General Chair:
Malte Schwarzkopf,
Program Chairs:
Andrew Baumann,
Natacha Crooks

Copyright © 2023 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGOPS: ACM Special Interest Group on Operating Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 June 2023

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

HOTOS '23

Sponsor:

SIGOPS

HOTOS '23: 19th Workshop on Hot Topics in Operating Systems

June 22 - 24, 2023

RI, Providence, USA

Upcoming Conference

HOTOS '25

Sponsor:
sigops

Workshop on Hot Topics in Operating Systems

May 14 - 16, 2025

Banff or Lake Louise , AB , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
224
Total Downloads

Downloads (Last 12 months)128
Downloads (Last 6 weeks)15

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Liu JHao XArpaci-Dusseau AArpaci-Dusseau RChajed T(2024)Shadow Filesystems: Recovering from Filesystem Runtime Errors via Robust Alternative ExecutionProceedings of the 16th ACM Workshop on Hot Topics in Storage and File Systems10.1145/3655038.3665942(15-22)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3655038.3665942

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents