Funding

Research on Device Drivers

Overview

A fast and reliable operating system requires fast and reliable device drivers. Most current operating systems sacrifice reliability for speed by executing drivers in kernel mode. Given that drivers account for the bulk of kernel code (70% in Linux), and that driver developers are typically not kernel experts, it does not come as a surprise that the majority of OS failures nowadays are caused by bugs in device drivers.

In a microkernel-based system, such as those based on seL4, device drivers run in user mode, as normal processes, encapsulated in their own address space. This encapsulation can be enforced through hardware mechanisms, such as the memory-management unit (MMU) and an IOMMU for devices performing direct memory access (DMA). Our aim is to have seL4-based I/O that performs comparable to Linux, yet achieving high robustness by encapsulating drivers to achieve fault isolation and ideally formally verify drivers.

seL4 Device Driver Framework (sDDF)

After much activity on (user-level as well as Linux) device drivers, we had for ten or so years mostly focussed on other issues. Drivers had been mostly dealt in an ad-hoc fashion, with some rudimentary frameworks that were complex and not performant.

From 2022 we re-focussed on drivers, and have developed a new seL4 device driver framework (sDDF), which provides a set of interfaces, designs and tools for developing high-performance, encapsulated device drivers for seL4.

sDDF Design

At the core of the sDDF is a transport layer that enables low-overhead, shared-memory communication between the driver and its client (an OS service such as a network protocol stack of a file-system server). The transport layer uses ring buffers for data sharing, concurrency control and flow control.

sDDF observes the lessons learned from our Dingo project: Drivers are schedulable entities but strictly single-threaded, and communicate with the rest of the OS via shared memory, with zero-copy passing of I/O data via simple, bounded, single-producer, single-consumer (SPSC) queues synchronised by semaphores.

Furthermore, sDDF strictly adheres to the principle of separation of concerns, where the one and only concern of a device driver is to translate a hardware-specific device interface to a hardware-independent device-class interface. This leads to drastically simpler device drivers compared to traditional driver models.

Among others, this design philosophy implies that sharing a device between multiple clients is not the driver's job, but we use explicit virtualisers for sharing a device – the virtualisers are also responsible for address translation (between client virtual and device I/O addresses) as well as cache management. In the case of network-like devices, such as Ethernet, we keep the transmit (Tx) and receive (Rx) paths separate, further simplifying the components.

This leads to an the architecture shown for Ethernet in the above diagram: The networking layer consists of several components, each a single-threaded process encapsulated in its own address space. Data buffers are passed between components zero-copy (except for explicit copiers) through SPSC queues, and separate queues are used for returning used buffers.

An advantage of this architecture is that individual components are location-transparent, meaning they can be distributed across processor cores. This eliminates the potential performance penalty from using purely sequential implementations.

Performance

Despite running at user level and handing data through multiple components (triggering a significant number of context switches), sDDF-based I/O performs very well. The graph compares networking performance on an Arm platform with a 1Gb/s NIC running on a single core, compared to Linux. The graph should achieved throughput and CPU utilisation at varying applied loads.

While sDDF has no problem saturating the network with plenty of cycles to spare (CPU load at maximum throughput is about 65%), Linux cannot keep up with the load as it maxes out the CPU at about 500Mb/s applied load.

We get similar results for the multicore configuration, Linux cannot saturate the network link with a single client (it achieves better throughput if the load is distributed over multiple clients at the expense of even higher overall CPU use).

Legacy driver re-use

While the design of sDDF leads to much simplified (and less buggy!) drivers than, say, the Linux driver model, without sacrificing performance, it is unrealistic to re-write all drivers from scratch. Instead, there needs to be an easy way to re-use existing drivers, especially from Linux.

To this end we developed a re-use framework for unmodified Linux drivers. We wrap the driver into a minimally configured Linux kernel running in a virtual machine (VM). The driver is controlled by a usermode Linux component, the UIO driver using the Linux UIO framework.

The UIO driver interacts with the rest of the seL4-based system via standard sDDF protocols, including mapping the sDDF shared memory regions. Semaphores (seL4 Notifications) are mapped onto interrupts using IRQ injection by the per-VM virtual machine monitor (VMM). The driver appears to the rest of the seL4 system like a native sDDF driver.

The re-use framework requires developing one UIO driver per device class, which is typically a few days of work, with a few extra weeks spent on optimisation (mostly reducing the driver VM's memory footprint).

Status

sDDF presently supports a number of mature device classes with native driver implementations, including serial, timer, clock, Pinmux, I²C, SPI, Ethernet, SDHC storage, and NFC card reader. In addition, GPU (for 2-d graphics), storage and sound (ALSA) are supported via Linux driver VMs. New device classes are added frequently.

Driver verification

sDDF dramatically simplifies driver design. For example, the Ethernet driver from the above performance graph is less than 600 lines of code, while the LInux driver for the same device is close to 5,000 lines.

This simplicity is greatly simplifies driver verification. We further simplify the verification problem by using the Pancake language for driver implementation, Pancake is designed to be easier to verify than C, by having a simple and well-define semantics. Pancake also has a verified compiler, meaning that correctness proofs performed in Pancake code are guaranteed to hold for the binary as well.

Device formalisation

As mentioned in the Overview, device driver bugs are the leading cause of operating-system exploits, and the lack of accurate specifications of device interfaces is a leading cause of driver bugs.

The Device formalisation project aims to address this specification issue by deriving formal specifications of devices from their Verilog implementation, and prove the correctness of the specification against the implementation. We will use such formal specifications as the device model for device verification as well as basis for writing device drivers.

Our past work on drivers

Our research on high-performance user-level device drivers predates seL4. In addition we explored a number of approaches in the past, including:

Dingo

The Dingo project investigated how existing operating systems, such as Linux, can be made more driver-friendly without radically changing their architecture.

Hardware/Software Co-Verification

In this project we developed a methodology that integrates driver development in the hardware design and (informal) verification workflow. This approach allows leveraging the enormous effort that hardware vendors put into hardware quality assurance in order to improve the device-driver reliability.

Termite

In the Termite project we explored synthesising drivers from their (device and OS) interface specs. The project combined game-theory approaches with user guidance to produce performant driver code.

Support

We gratefully acknowledge the financial support for the development of LionsOS by:

• Cyberagentur as part of the PISTIs-V Project under the Ecosystem formally verifiable IT – Provable cybersecurity (EvIT) program
• DARPA under the PROVERS program

Work on the sDDF was formerly supported by the seL4 Foundation and the Technology Innovation Institute.

Documentation

• sDDF Design — current version 0.6.0

Availability

The seL4 device driver framework is open source and available on the TS GitHub under a BSD License.

Latest News

• 2025-03-21: TS releases version 0.6.0 of the sDDF.
• 2024-08-06: TS releases version 0.5.0 of the sDDF.
• 2024-03-27: TS releases version 0.4 of the sDDF on the TS GitHub.
• 2023-10-19: Lucy Parker presents an update on the sDDF at the seL4 Summit.
• 2022-10-10: Lucy Parker presents the sDDF at the seL4 Summit.
• 2022-10-07: Release of Revision 0.2 of the sDDF is released for comment. The source code is available on GitHub.

Contact

• Gernot Heiser, gernot<at>unsw.edu.au

People

Publications

		Liam Murphy, Albert Rizaldi, Lesley Rossouw, Chen George, James Treloar, Hammond Pearce, Miki Tanaka and Gernot Heiser High-fidelity specification of real-world devices Workshop on Programming Languages and Operating Systems (PLOS), October, 2025
		Junming Zhao, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Miki Tanaka, Johannes \AAman Pohjola, Thomas Sewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish and Gernot Heiser Verifying device drivers with Pancake arXiv preprint, January, 2025
		Gernot Heiser, Peter Chubb, Alex Brown, Courtney Darville and Lucy Parker sDDF design: design, implementation and evaluation of the seL4 device driver framework 2024
		Lucy Parker High-performance networking on seL4 BSc(Hons) Thesis, School of Computer Science and Engineering, Sydney, Australia, November, 2023
		Johannes \AAman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Tsun Wang Sau, Benjamin Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus O. Myreen, Michael Norrish and Gernot Heiser Pancake: verified systems programming made sweeter Workshop on Programming Languages and Operating Systems (PLOS), Koblenz, DE, October, 2023
		Lucy Parker The seL4 device driver framework Talk at the 5th seL4 Summit, September, 2023
		Gernot Heiser, Lucy Parker, Peter Chubb, Ivan Velickovic and Ben Leslie Can we put the "S" into IoT? IEEE World Forum on Internet of Things, Yokohama, JP, November, 2022
		Lucy Parker The seL4 device driver framework Talk at the 4th seL4 Summit, October, 2022