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 the past 10 years mostly focussed on other issues. With the maturing and increasing deployment of seL4, drivers have come to the forefront again, and we are working on a driver framework for seL4 and issues arising from that.

The seL4 device driver framework provides a set of interfaces, designs and tools for developing high-performance, encapsulated device drivers for seL4.

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. 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.

Device virtualisation

The sDDF is also the base for sharing devices between multiple clients, some of which might be virtual machines running a Linux guest. Here each device has a single driver, encapsulated either in a native component or a virtual machine, and is multiplexed securely between clients. The multiplexing is done by a virtualised (Virt) component, that is also responsible for address translation and cache management.

A Linux VM interfaces with the Virt via a VirtIO interface and shared memory. The same principle also allows us to re-use Linux drivers by encapsulating them into a per-device driver VM. The driver VM uses Linux UIO to interface between the sDDF framework and the in-kernel Linux driver.

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 a few cycles to spare (CPU load at maximum throughput is about 95%), Linux cannot keep up with the load as it maxes out the CPU at about 600Mb/s applied load.

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.

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.4

Availability

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

Latest News

• 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

		Junming Zhao, Alessandro Legnani, Tiana Tsang Ung, H. Truong, Tsun Wang Sau, Miki Tanaka, Johannes Åman 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 Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Gordon Sau, Ben Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus 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, Ivan Velickovic, Peter Chubb 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