Our Partners
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.
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.
The sDDF is as yet incomplete. It currently provides some guidance for designing systems using drivers (device discovery, separation of control and data planes), and has some libraries for high-throughput, low latency data-plane communication.
The sDDF is also the base for sharing devices between virtual machines and native clients. Here each device has a single driver, encapsulated either in a native component or a virtual machine, and is multiplexed securely between clients.
Formal verification of device drivers is our long-term goal, which is enabled by the strong isolation provided for usermode drivers on seL4, which allows verifying drivers in isolation. We had some limited success at verifying simple drivers in the Cogent project. Our latest attempt at verifying drivers is the Pancake project, which is developing a new low-level programming language reusing the verification framework of CakeML.
Our research on high-performance user-level device drivers predates seL4. In addition we explored a number of approaches in the past, including:
The current sDDF work is financially supported by the seL4 Foundation and the Technology Innovation Institute. See the relevant sub-project pages for supporters and collaborators on those.
We are collaborating with Breakaway Consulting on the sDDF.
Current |
Past
|
|
 |
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 |