ABSTRACT

Faulty device drivers cause significant damage through down time and data loss. The problem can be mitigated by an improved driver development process that guarantees correctness by construction. We achieve this by synthesising drivers automatically from formal specifications of device interfaces, thus reducing the impact of human error on driver reliability and potentially cutting down on development costs.

We present a concrete driver synthesis approach and tool called Termite. We discuss the methodology, the technical and practical limitations of driver synthesis, and provide an evaluation of nontrivial drivers for Linux, generated using our tool. We show that the performance of the generated drivers is on par with the equivalent manually developed drivers. Furthermore, we demonstrate that device specifications can be reused across different operating systems by generating a driver for FreeBSD from the same specification as used for Linux.

Categories and Subject Descriptors

D.4.4 [Operating Systems]: Input/Output; B.4.2 [Input/Output and Data Communications]: Input/Output Devices

General Terms

Languages, Reliability, Verification

Keywords

Device Drivers, Software Synthesis, Domain-Specific Languages, Two-Player Games.

1. INTRODUCTION

Faulty device drivers are a major source of operating system failures, causing significant damage through downtime and data loss [10, 24]. A number of static [1, 3, 8] and runtime [9, 12, 15, 16, 24, 28] techniques have been proposed to detect and isolate driver faults. These techniques, however, suffer from serious limitations. Existing static analysis tools are capable of detecting a limited subset of errors, such as common OS API rule violations [1] and certain memory allocation and synchronisation errors [8]. Stronger correctness properties, such as memory safety, race-freedom, and correct use of device interfaces, are currently beyond the reach of these tools. Runtime isolation architectures are capable of detecting broader classes of errors, but do so at the cost of introducing a CPU overhead in the order of 100% [4, 9, 24].