Beyond isolation: OS verification as a foundation for correct applications
OPEN ACCESS
Loading...
Author / Producer
Date
2023
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
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.
Permanent link
Publication status
published
External links
Editor
Book title
HOTOS '23: Proceedings of the 19th Workshop on Hot Topics in Operating Systems
Journal / series
Volume
Pages / Article No.
158 - 165
Publisher
Association for Computing Machinery
Event
19th Workshop on Hot Topics in Operating Systems (HotOS'23)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03634 - Basin, David / Basin, David
Notes
Conference lecture held on June 23, 2023