Device drivers are programs which allow software or higher-level computer programs to interact with a hardware device. These software components act as a link between the devices and the operating systems, communicating with each of these systems and executing commands. They provide an abstraction layer for the software above and also mediate the communication between the operating system kernel and the devices below.
Usually the operating systems comes with a support for the common device drivers and usually the hardware vendors provide the device driver for their hardware devices for most platforms. The aggressive scaling of the hardware devices and the complex software components has made the device driver development process cumbersome and complex. When the size and functionality of the drivers started increasing the device drivers became a key factor in defining the reliability of the system. This has created an incentive towards automatic synthesis and verification of device drivers. This article sheds some light into some approaches in synthesis and verification of device drivers.
Motivation for automatic driver synthesis and verification Device drivers are the principal failing component in most systems. The Berkeley Open Infrastructure for Network Computing (BOINC) project found that OS crashes are predominantly caused by poorly written device driver code.Archana Ganapathi, Viji Ganapathi and David Patterson. "Windows XP kernel crash analysis". In Proceedings of the 2006 Large Installation System Administration Conference, 2006. In Windows XP, drivers account for 85% of the reported failures. In the Linux kernel 2.4.1 device driver code accounts for about 70% of the code size.A. Chou, J. Yang, B. Chelf, S. Hallem and D. Engler. An Empirical Study of Operating Systems Errors. In SOSP, 2001 The driver fault can crash the whole system as it is running in the kernel mode. These findings resulted in various methodologies and techniques for verification of device drivers. An alternative was to develop techniques which can synthesize device drivers robustly. Less human interaction in the development process and proper specification of the device and operating systems can lead to more reliable drivers.
The other motivation for driver synthesis, is the large number of flavors of operating systems and device combinations. Each of these has its own set of input/output control and specifications which makes support of hardware devices on each of the operating systems difficult. So the ability to use a device with an operating system requires the availability of corresponding device driver combination. Hardware vendors usually supply the drivers for Windows, Linux and Mac OS but due to the high development or porting costs and technical support difficulties they are unable to provide drivers on all platforms. An automated synthesis technique can help the vendors in providing drivers to support any devices on any operating system.
Verification of device drivers There are two challenges that limit testing the device drivers. It is very hard to determine the exact operation or time when there is a fault in the interaction between driver and the kernel. The system could go into some inconsistent state and the crash is reported after a long time, blurring the real cause of the crash. The drivers which work properly in normal circumstances can go wrong in rare and exceptional cases and the traditional testing techniques may not help in detecting the corner case behavior of the drivers.
The wave of verification of device drivers was initiated by Microsoft through their SLAM project as early as the year 2000. The motivation for the project was that 500,000 crashes reported a day were found to be caused by one video driver, leading to concern about the great vulnerability in using complex device drivers. More details can be found here, in the speech delivered by Bill Gates. A large number of static and runtime techniques have since been proposed for bug detection and isolation.
Static analysis Static analysis means analyzing the program to check whether it complies with the safety-critical properties specified. For example, the system software should conform to rules such as "check user permissions before writing to kernel data structures", "don't reference null pointer without check", "prohibit overflowing buffer size" etc. Such checks can be made without actually executing the code being checked. Using the traditional testing process (dynamic execution) requires writing many test cases to exercise these paths and drive the system into error states. This process can take a long time and effort and is not a practical solution. Another theoretically possible approach is manual inspection, but this is impractical in modern systems in which millions of lines of code are involved, making the logic too complex to be analyzed by humans.
Compiler techniques The rules that have a straightforward mapping to source code can be checked using a compiler. Rule violations can be found by checking if the source operation does not make sense. For example, rules like "enabling an interrupt after being disabled" can be checked by looking at the order of function calls. But if the source code type system cannot specify the rules in its semantics, then the compilers cannot catch errors of that kind. Many type-safe languages allow memory safety violations resulting from unsafe type casting to be detected by compiler.
Another approach is to use meta-level compilation (MC).Engler, Dawson and Chelf, Benjamin and Chou, Andy and Hallem, Seth. "Checking system rules using system-specific, programmer-written compiler extensions". In Proceedings of the 4th conference on Symposium on Operating System Design and Implementation, 2000 Metacompilers constructed for this purpose may extend the compilers with lightweight, system specific checkers and optimizers. These extensions need to be written by system implementers in a high level language and dynamically linked to the compilers to do strict static analysis.
Software model checking Software model checking is the algorithmic analysis of programs to prove properties of their executions.Jhala, Ranjit and Majumdar, Rupak. "Software model checking". In ACM Computation Survey. 2009 This automates the reasoning about the program behavior with respect to the given correct specifications. Model checking and symbolic execution are used to verify the safety-critical properties of device drivers. The input to the model checker is the program and the temporal safety properties. The output is the proof that the program is correct or a demonstration that there exists a violation of the specification by means of a counterexample in the form of a specific execution path.
The tool SDV (Static Driver Verifier)Thomas Ball, Ella Bounimova, Byron Cook, Vladimir Levin, Jakob Lichtenberg, Con McGarvey, Bohus Ondrusek, Sriram Rajamani. and Abdullah Ustuner. "Thorough static analysis of device drivers", In SIGOPS Oper. Syst. Rev, Vol. 40, 2006. from Microsoft uses static analysis for windows device drivers. The back end analysis engine SLAM used model checking and symbolic execution for compile time static verification. The rules that are to be observed by the drivers for each API are specified in a C like language SLIC (Specification Language for Interface Checking). The analysis engine finds all paths which can lead to violations of the API usage rules and are presented as source level error paths through the driver source code. Internally, it abstracts the C code into a boolean program and a set of predicates which are rules that are to be observed on this program. Then it uses the symbolic model checkingMcMillan, Kenneth L. "Symbolic Model Checking". Kluwer Academic Publishers, 1993. to validate the predicates on the boolean program.
The model checker BLAST (Berkeley Lazy Abstraction Software verification Tool)Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre. "Software Verification with BLAST". In SPIN, 2003. is used to find memory safety and incorrect locking errors in Linux kernel code. It uses an abstraction algorithm called lazy abstractionThomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre. "Lazy Abstraction", In ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, 2002. to build the model from the driver C code. It has been successful in verifying temporal safety properties of C programs with up to 50K lines of code. It is also used to determine if a change in the source code affects the proof of property in the previous version and is demonstrated on a Windows device driver.
AvinuxH. Post, W. Küchlin. "Integration of static analysis for linux device driver verification". In The 6th Intl. Conf. on Integrated Formal Methods, 2007. is another tool that facilitates the automatic analysis of Linux device drives and is built on top of bounded model checker CBMC.Edmund Clarke, Daniel Kroening and Flavio Lerda. "A Tool for checking ANSI-C Programs". In TACAS, 2004 There exist fault localization methods to find the bug location as these model checking tools return a long counter example trace and it is hard to find the exact faulty location.Thomas Ball, Mayur Naik, and Sriram K. Rajamani. "From symptom to cause: localizing errors in counterexample traces". ACM SIGPLAN Notices, 2003.
Run-time analysis Dynamic program analysis is performed by running the program with sufficient test inputs to produce interesting behaviors. Safe DriveFeng Zhou, Jeremy Condit, Zachary Anderson, Ilya Bagrak, Rob Ennals, Matthew Harren, George Necula and Eric Brewer. "SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques". In 7th OSDI, 2006. is a low overhead system for detecting and recovering from type safety violations in device drivers. With only 4% changes to the source code of Linux network drivers they were able to implement SafeDrive and give better protection and recovery to Linux kernel. A similar project using hardware to isolate the device drivers from the main kernel is Nook.Michael M. Swift, Steven Martin, Henry M. Levy, and Susan J. Eggers. "Nooks: an architecture for reliable device drivers ". In 10th ACM SIGOPS, 2002. They place device drivers in separate hardware protection domain called "nooks" and they have separate permission setting for each pages making sure that a driver does not modify pages which are not in its domain but can read all kernel data since they share the same address space.
Another similar work in this area is on automatic recovery of operating systems due to driver faults. Minix 3Jorrit N. Herder, Herbert Bos, Ben Gras, Philip Homburg, and Andrew S. Tanenbaum. "MINIX 3: a highly reliable, self-repairing operating system". In SIGOPS Oper. Syst. Rev. 40, 2006. is an operating system which can isolate major faults, defects are detected and failing components are replaced on the fly.
Device driver synthesis An alternative to verification and isolation of faults is to deploy techniques in device driver development process to make it more robust. Given a device specification and operating system functions, one method is to synthesize device driver for that device. This helps to reduce the human introduced errors as well as the cost and time involved in developing the system software. All the synthesis methods rely on some form of specification from the hardware device manufacturers and operating system functions.
Interface specification languages