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 one 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, for devices performing direct memory access (DMA) an I/O MMU. In our previous research we showed that this approach, if done right, does not impose much overhead, and allows isolating the rest of the system from device-driver failures.

While this approach removes a device driver from the trusted computing base (TCB) of a subsystem which does not use the device, many devices are essential to the overall system function, and a system may be unable to operate correctly if a critical driver fails even temporarily.

We are therefore continuing to work on making the drivers themselves reliable. We are pursuing a number of approaches, distinguished by the time to practical deployment:

Dingo
The first (short-term) approach investigates how existing operating systems, such as Linux, can be made more driver-friendly without radically changing their architecture.
Hardware/Software Co-Verification
The second (medium-term) approach, integrates driver development in the hardware design and 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
The third (long-term) approach aims to create device drivers which are bug-free by construction, by synthesising them automatically from a formal specification of the device.

People

Publications

plain text PDF Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu
Automatic verification of message-based device drivers
Systems Software Verification, Sydney, Australia, November, 2012
plain text PDF Sidney Amani, Peter Chubb, Alastair Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu
Active device drivers
Technical Report , NICTA, October, 2012
plain text PDF Sidney Amani, Leonid Ryzhyk, Alastair Donaldson, Gernot Heiser, Alexander Legg and Yanjin Zhu
Static analysis of device drivers: we can do better!
Proceedings of the 2nd Asia-Pacific Workshop on Systems (APSys), Shanghai, China, July, 2011
plain text PDF Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor Kuz and Leonid Ryzhyk
The road to trustworthy systems
Proceedings of the 5th ACM Workshop on Scalable Trusted Computing (ACMSTC), Chicago, IL, USA, October, 2010
Invited paper
plain text PDF Leonid Ryzhyk, Yanjin Zhu and Gernot Heiser
The case for active device drivers
Proceedings of the 1st Asia-Pacific Workshop on Systems (APSys), New Delhi, India, August, 2010
plain text PDF Leonid Ryzhyk
On the construction of reliable device drivers, PhD Thesis, School of Computer Science and Engineering, Sydney, Australia, 2010
plain text PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser
Automatic device driver synthesis with Termite
Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA, October, 2009
plain text PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz and Gernot Heiser
Dingo: Taming device drivers
Proceedings of the 4th EuroSys Conference, Nuremberg, Germany, April, 2009
plain text PDF Leonid Ryzhyk, Ihor Kuz and Gernot Heiser
Formalising device driver interfaces
Proceedings of the 4th Workshop on Programming Languages and Operating Systems (PLOS), Stevenson, Washington, USA, October, 2007
plain text PDF Leonid Ryzhyk, Timothy Bourke and Ihor Kuz
Reliable device drivers require well-defined protocols
Proceedings of the 3rd Workshop on Hot Topics in System Dependability, Edinburgh, UK, June, 2007