arXiv subjects

Gernot Heiser

Publications and source records attributed to Gernot Heiser.

12 recordsLinked to original sources

arXiv2025

Verifying Device Drivers with Pancake

Device driver bugs are the leading cause of OS compromises, and their formal verification is therefore highly desirable. To the best of our knowledge, no realistic and performant driver has been verified for a non-trivial device. We propose Pancake, an imperative language for systems programming that features a well-defined and verification-friendly semantics. Leveraging the verified compiler backend of the CakeML functional language, we develop a compiler for Pancake that guarantees that the binary retains the semantics of the source code. Usng automatic translation of Pancake to the Viper SMT front-end, we verify a performant driver for an Ethernet NIC.

cs.PL↗

arXiv2025

Fast, Secure, Adaptable: LionsOS Design, Implementation and Performance

We present LionsOS, an operating system for security- and safety-critical embedded systems. LionsOS is based on the formally verified seL4 microkernel and designed with verification in mind. It uses a static architecture and features a highly modular design driven by strict separa- tion of concerns and a focus on simplicity. We demonstrate that LionsOS achieves excellent performance on system-call intensive workloads.

cs.OS↗

arXiv2024

fence.t.s: Closing Timing Channels in High-Performance Out-of-Order Cores through ISA-Supported Temporal Partitioning

Microarchitectural timing channels exploit information leakage between security domains that should be isolated, bypassing the operating system's security boundaries. These channels result from contention for shared microarchitectural state. In the RISC-V instruction set, the temporal fence instruction (fence.t) was proposed to close timing channels by providing an operating system with the means to temporally partition microarchitectural state inexpensively in simple in-order cores. This work explores challenges with fence.t in superscalar out-of-order cores featuring large and pervasive microarchitectural state. To overcome these challenges, we propose a novel SW-supported temporal fence (fence.t.s), which reuses existing mechanisms and supports advanced microarchitectural features, enabling full timing channel protection of an exemplary out-of-order core (OpenC910) at negligible hardware costs and a minimal performance impact of 1.0 %.

cs.CR↗

arXiv2023

Proving the Absence of Microarchitectural Timing Channels

Microarchitectural timing channels are a major threat to computer security. A set of OS mechanisms called time protection was recently proposed as a principled way of preventing information leakage through such channels and prototyped in the seL4 microkernel. We formalise time protection and the underlying hardware mechanisms in a way that allows linking them to the information-flow proofs that showed the absence of storage channels in seL4.

cs.OS↗

arXiv2022

Systematic Prevention of On-Core Timing Channels by Full Temporal Partitioning

Microarchitectural timing channels enable unwanted information flow across security boundaries, violating fundamental security assumptions. They leverage timing variations of several state-holding microarchitectural components and have been demonstrated across instruction set architectures and hardware implementations. Analogously to memory protection, Ge et al. have proposed time protection for preventing information leakage via timing channels. They also showed that time protection calls for hardware support. This work leverages the open and extensible RISC-V instruction set architecture (ISA) to introduce the temporal fence instruction fence.t, which provides the required mechanisms by clearing vulnerable microarchitectural state and guaranteeing a history-independent context-switch latency. We propose and discuss three different implementations of fence.t and implement them on an experimental version of the seL4 microkernel and CVA6, an open-source, in-order, application class, 64-bit RISC-V core. We find that a complete, systematic, ISA-supported erasure of all non-architectural core components is the most effective implementation while featuring a low implementation effort, a minimal performance overhead of less than 1%, and negligible hardware costs.

cs.CR↗

arXiv2020

Prevention of Microarchitectural Covert Channels on an Open-Source 64-bit RISC-V Core

Covert channels enable information leakage across security boundaries of the operating system. Microarchitectural covert channels exploit changes in execution timing resulting from competing access to limited hardware resources. We use the recent experimental support for time protection, aimed at preventing covert channels, in the seL4 microkernel and evaluate the efficacy of the mechanisms against five known channels on Ariane, an open-source 64-bit application-class RISC-V core. We confirm that without hardware support, these defences are expensive and incomplete. We show that the addition of a single-instruction extension to the RISC-V ISA, that flushes microarchitectural state, can enable the OS to close all five evaluated covert channels with low increase in context switch costs and negligible hardware overhead. We conclude that such a mechanism is essential for security.

cs.CR↗

arXiv2019

Can We Prove Time Protection?

Timing channels are a significant and growing security threat in computer systems, with no established solution. We have recently argued that the OS must provide time protection, in analogy to the established memory protection, to protect applications from information leakage through timing channels. Based on a recently-proposed implementation of time protection in the seL4 microkernel, we investigate how such an implementation could be formally proved to prevent timing channels. We postulate that this should be possible by reasoning about a highly abstracted representation of the shared hardware resources that cause timing channels.

cs.OS↗

arXiv2018

Time Protection: the Missing OS Abstraction

Timing channels enable data leakage that threatens the security of computer systems, from cloud platforms to smartphones and browsers executing untrusted third-party code. Preventing unauthorised information flow is a core duty of the operating system, however, present OSes are unable to prevent timing channels. We argue that OSes must provide time protection in addition to the established memory protection. We examine the requirements of time protection, present a design and its implementation in the seL4 microkernel, and evaluate its efficacy as well as performance overhead on Arm and x86 processors.

cs.OS↗

arXiv2018

Benchmarking Crimes: An Emerging Threat in Systems Security

Properly benchmarking a system is a difficult and intricate task. Unfortunately, even a seemingly innocuous benchmarking mistake can compromise the guarantees provided by a given systems security defense and also put its reproducibility and comparability at risk. This threat is particularly insidious as it is generally not a result of malice and can easily go undetected by both authors and reviewers. Moreover, as modern defenses often trade off security for performance in an attempt to find an ideal design point in the performance-security space, the damage caused by benchmarking mistakes is increasingly worrisome. To analyze the magnitude of the phenomenon, we identify a set of 22 "benchmarking crimes" that threaten the validity of systems security evaluations and perform a survey of 50 defense papers published in top venues. To ensure the validity of our results, we perform the complete survey twice, with two independent readers. We find only a very small number of disagreements between readers, showing that our assessment of benchmarking crimes is highly reproducible. We show that benchmarking crimes are widespread even in papers published at tier-1 venues. We find that tier-1 papers commit an average of five benchmarking crimes and we find only a single paper in our sample that committed no benchmarking crimes. Moreover, we find that the scale of the problem is constant over time, suggesting that the community is not yet addressing it despite the problem being now more relevant than ever. This threatens the scientific process, which relies on reproducibility and comparability to ensure that published research advances the state of the art. We hope to raise awareness of these issues and provide recommendations to improve benchmarking quality and safeguard the scientific process in our community.

cs.CR↗

arXiv2017

Your Processor Leaks Information - and There's Nothing You Can Do About It

Timing channels are information flows, encoded in the relative timing of events, that bypass the system's protection mechanisms. Any microarchitectural state that depends on execution history and affects the rate of progress of later executions potentially establishes a timing channel, unless explicit steps are taken to close it. Such state includes CPU caches, TLBs, branch predictors and prefetchers; removing the channels requires that the OS can partition such state or flush it on a switch of security domains. We measure the capacities of channels based on these microarchitectural features on several generations of processors across the two mainstream ISAs, x86 and ARM, and investigate the effectiveness of the flushing mechanisms provided by the respective ISA.We find that in all processors we studied, at least one significant channel remains. This implies that closing all timing channels seems impossible on contemporary mainstream processors.

cs.CR↗

arXiv2016

An Evaluation of Coarse-Grained Locking for Multicore Microkernels

The trade-off between coarse- and fine-grained locking is a well understood issue in operating systems. Coarse-grained locking provides lower overhead under low contention, fine-grained locking provides higher scalability under contention, though at the expense of implementation complexity and re- duced best-case performance. We revisit this trade-off in the context of microkernels and tightly-coupled cores with shared caches and low inter-core migration latencies. We evaluate performance on two architectures: x86 and ARM MPCore, in the former case also utilising transactional memory (Intel TSX). Our thesis is that on such hardware, a well-designed microkernel, with short system calls, can take advantage of coarse-grained locking on modern hardware, avoid the run-time and complexity cost of multiple locks, enable formal verification, and still achieve scalability comparable to fine-grained locking.

cs.OS↗

arXiv2016

It's Time: OS Mechanisms for Enforcing Asymmetric Temporal Integrity

Mixed-criticality systems combine real-time components of different levels of criticality, i.e. severity of failure, on the same processor, in order to obtain good resource utilisation. They must guarantee deadlines of highly-critical tasks at the expense of lower-criticality ones in the case of overload. Present operating systems provide inadequate support for this kind of system, which is of growing importance in avionics and other verticals. We present an approach that provides the required asymmetric integrity and its implementation in the high-assurance seL4 microkernel.

cs.OS↗