Reto Achermann

Assistant Professor
Systems Research Group
TUM School of Computation, Information and Technology

Beyond isolation: OS verification as a foundation for correct applications

Authors

Matthias Brun, Reto Achermann, Tej Chajed, Jon Howell, Gerd Zellweger and Andrea Lattuada

Venue

Proceedings of the 19th Workshop on Hot Topics in Operating Systems (HotOS'23)

Links

[ .doi ] [ .pdf ] [ .bib ]

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.

Bibtex

@inproceedings{Brun:2023:BIOS,
 author = {Brun, Matthias and Achermann, Reto and Chajed, Tej and Howell, Jon  and Zellweger, Gerd   and Lattuada, Andrea  },
 booktitle = {Proceedings of the 19th Workshop on Hot Topics in Operating Systems},
 doi = {10.1145/3593856.3595899},
 id = {Brun:2023:BIOS},
 isbn = {979-8-4007-0195-5},
 location = {Providence, Rhode Island, USA},
 pages = {158--165},
 publisher = {Association for Computing Machinery},
 series = {HotOS'23},
 title = {Beyond isolation: OS verification as a foundation for correct applications},
 url = {https://doi.org/10.1145/3593856.3595899},
 year = {2023}
}

Contact

Prof. Reto Achermann
I01: Chair of Distributed Systems and Operating Systems (aka Systems Research Group)
1st Floor, 7th Finger
School of Computation, Information, and Technology (CIT)
Technical University of Munich (TUM)
Boltzmannstr. 3
85748 Garching bei München
Germany

firstname.lastname [at] cit.tum.de