Making Device Drivers Safer

Motivation

The Systems group has developed their own device specification language, called Mackerel, which is used at large scale within our research operating system Barrelfish [3]. Mackerel already supports most of the features of Devil and some additional ones.

On the other hand, systems specification languages, like TLA+ [4], and device/driver interaction specification languages [5] have been developed that allow system designers to specify (and verify) even the most complex interactions within software and hardware systems.

Goals

The goal of this project is to extend Mackerel by TLA+ or some subset thereof, allowing complex interactions between the device driver and the device itself to be specified. Once a specification is in place, it can be automatically checked for soundness by TLA's integrated model-checker, which is already provided. Furthermore, it would be desirable if more sophisticated checks could be implemented at run-time to test correct behavior of a device driver. It should be possible to enable these checks on demand.

References

[1] Michael M. Swift, Steven Martin, Henry M. Levy, and Susan J. Eggers. Nooks: An Architecture for Reliable Device Drivers. In Proceedings of the 10th SIGOPS European Workshop, 2002.

[2] F. Merillon, L. Reveillere, C. Consel, R. Marlet, and G. Muller. Devil: An IDL for hardware programming. In Proc. 4th OSDI, pages 17­30, San Diego, CA, Oct. 2000.

[3] http://www.barrelfish.org/

[4] http://research.microsoft.com/users/lamport/tla/book.html

[5] Leonid Ryzhyk, Ihor Kuz, Gernot Heiser. Formalising Device Driver Interfaces. In Proceedings of the 4th workshop on Programming languages and operating systems, Stevenson, WA, 2007.

Contact

Simon Peter