Skip to main content


Improved device driver reliability through verification reuse


Leonid Ryzhyk, John Keys, Balachandra Mirla, Arun Raghunath, Mona Vij and Gernot Heiser



Intel Corporation

Open Kernel Labs


Faulty device drivers are a major source of operating system failures. We argue that the underlying cause of many driver faults is the separation of two highly-related tasks: device verification and driver development. These two tasks have a lot in common, and result in software that is conceptually and functionally similar, yet kept totally separate. The result is a particularly bad case of duplication of effort: the verification code is correct, but is discarded after the device has been manufactured; the driver code is inferior, but used in actual device operation. We claim that the two tasks, and the software they produce, can and should be unified, and this will result in drastic improvement of device-driver quality and reduction in the development cost and time to market.

In this paper we discuss technical issues involved in achieving such unification and present our solutions to these issues. We report the results of a case study that applies this approach to implement a driver for an Ethernet controller device.

BibTeX Entry

    author           = {Ryzhyk, Leonid and Keys, John and Mirla, Balachandra and Raghunath, Arun and Vij, Mona and Heiser,
    month            = oct,
    year             = {2010},
    keywords         = {device drivers, reliability, testing},
    title            = {Improved Device Driver Reliability Through Verification Reuse},
    booktitle        = {Workshop on Hot Topics in System Dependability},
    pages            = {1-6},
    address          = {Vancouver, Canada}


Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.