Trustworthy Systems

Our Partners The seL4 Foundation Technology Innovation Institute Breakaway Consulting

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)

Usermode device driver

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.

Related projects

Device virtualisation

Device sharing

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.

Driver verification

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

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.

Collaborations

We are collaborating with Breakaway Consulting on the sDDF.



Latest News

Contact

People

Current

Past

  • Adam Christopher Walker
  • Alexander Legg
  • Courtney Darville
  • Ihor Kuz
  • Jashank Jeremy
  • Leonid Ryzhyk
  • Sidney Amani
  • Yanjin Zhu
  • Andy Bui
  • Patrick Hao

Publications

plain text to be published 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
Abstract
Slides
PDF
Presentation Video
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
Abstract
Slides
PDF Pavol Cerny, Edmund Clarke, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta and Thorsten Tarrach
From non-preemptive to preemptive scheduling using synchronization synthesis
International Conference on Computer Aided Verification, San Francisco, USA, July, 2015
Abstract PDF Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk
SAT-based strategy extraction in reachability games
AAAI, Austin, TX, USA, January, 2015
Abstract
Slides
PDF Leonid Ryzhyk, Adam Christopher Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm and Mona Vij
User-guided device driver synthesis
USENIX Symposium on Operating Systems Design and Implementation, pp. 661–676, Broomfield, CO, USA, October, 2014
Abstract PDF Adam Christopher Walker and Leonid Ryzhyk
Predicate abstraction for reactive synthesis
Conference on Formal Methods in Computer-Aided Design, Lausanne, Switzerland, October, 2014
Abstract PDF Adam Christopher Walker and Leonid Ryzhyk
Predicate abstraction for reactive synthesis
Technical Report NRL-8281, NICTA, August, 2014
Abstract PDF Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach
Regression-free synthesis for concurrency
International Conference on Computer Aided Verification, Vienna, Austria, July, 2014
Abstract PDF Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk
Interpolants in two-player games
Abstract, iPRA workshop, July, 2014.
Abstract PDF Alexander Legg, Nina Narodytska and Leonid Ryzhyk
Practical CNF interpolants via BDDs
Abstract, iPRA workshop, July, 2014.
Abstract PDF Nina Narodytska, Alexander Legg, Fahiem Bacchus, Leonid Ryzhyk and Adam Christopher Walker
Solving games without controllable predecessor
International Conference on Computer Aided Verification, Vienna, Austria, July, 2014
Abstract PDF Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Keng Chai Ong, Leonid Ryzhyk and Yanjin Zhu
Automatic verification of active device drivers
ACM Operating Systems Review, Volume 48, Number 1, May, 2014
Abstract PDF Mona Vij, John Keys, Arun Raghunath, Scott Hahn, Vincent Zimmer, Leonid Ryzhyk, Adam Christopher Walker and Alexander Legg
Device driver synthesis
Intel Technology Journal, Volume 17, Number 2, pp. 136–157, December, 2013
Abstract PDF Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach
Efficient synthesis for concurrency by semantics-preserving transformations
Proceedings of the 25th International Conference on Computer Aided Verification, pp. 1–16, Saint Petersburg, Russia, July, 2013
Abstract PDF Leonid Ryzhyk, Yanjin Zhu and Gernot Heiser
The case for active device drivers
Asia-Pacific Workshop on Systems (APSys), pp. 25–30, New Delhi, India, August, 2010
Abstract PDF Leonid Ryzhyk
On the construction of reliable device drivers
PhD Thesis, UNSW, Sydney, Australia, January, 2010
Abstract PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser
Automatic device driver synthesis with Termite
ACM Symposium on Operating Systems Principles, pp. 73–86, Big Sky, MT, US, October, 2009
Abstract PDF Joshua LeVasseur
Device-driver reuse via virtual machines
PhD Thesis, UNSW, Sydney, Australia, May, 2009
Abstract PDF Myrto Zehnder and Peter Chubb
Virtualising PCI
Gelato ICE, Singapore, October, 2006
Abstract PDF Ben Leslie, Peter Chubb, Nicholas FitzRoy-Dale, Stefan Götz, Charles Gray, Luke Macpherson, Daniel Potts, Yueting (Rita) Shen, Kevin Elphinstone and Gernot Heiser
User-level device drivers: Achieved performance
Journal of Computer Science and Technology, Volume 20, Number 5, pp. 654–664, September, 2005
Abstract PDF Ben Leslie, Peter Chubb, Nicholas FitzRoy-Dale, Stefan Götz, Charles Gray, Luke Macpherson, Daniel Potts, Yueting (Rita) Shen, Kevin Elphinstone and Gernot Heiser
User-level device drivers: Achieved performance
Technical Report PA005043, NICTA, July, 2005
Abstract PDF Peter Chubb
Get more device drivers out of the kernel!
Ottawa Linux Symposium, Ottawa, Canada, July, 2004
Abstract PDF Peter Chubb
Linux kernel infrastructure for user-level device drivers
5th Linux.conf.au, Adelaide, Australia, January, 2004
Abstract PDF Ben Leslie, Nicholas FitzRoy-Dale and Gernot Heiser
Encapsulated user-level device drivers in the Mungi operating system
Proceedings of the Workshop on Object Systems and Software Architectures 2004, Victor Harbor, South Australia, Australia, January, 2004
Abstract PDF Ben Leslie and Gernot Heiser
Towards untrusted device drivers
Technical Report UNSW-CSE-TR-0303, School of Computer Science and Engineering, March, 2003