Metadata only
Date
2023-10-23Type
- Conference Paper
ETH Bibliography
yes
Altmetrics
Abstract
Verification of any operating system is inevitably relative to a model of the underlying hardware. Within the context of kernel verification, the underlying hardware model usually comprises of architectural correctness of the executing cores, but pays little attention to devices underneath barring the assumption that they are "trusted".Recent work has pointed out that the de facto operating system of a machine includes not only the kernel and processes running on top, but the multitude of other devices driving the actual hardware: security (co-)processors, DMA engines, network firmware, and more. The concept of the de facto OS shines light on a critical boundary between a kernel and the rest of hardware which is crucial to reasoning about both kernel isolation, and the security properties of the whole operating system. In this paper we report on our experience to date in specifying the de facto OS environment of a production System-on-Chip, and the implications of this effort so far for assured kernel isolation. Show more
Publication status
publishedExternal links
Book title
KISV '23: Proceedings of the 1st Workshop on Kernel Isolation, Safety and VerificationPages / Article No.
Publisher
Association for Computing MachineryEvent
Organisational unit
03757 - Roscoe, Timothy / Roscoe, Timothy
More
Show all metadata
ETH Bibliography
yes
Altmetrics