Device driver synthesis and verification

Last updated
The device driver. Driverarch.png
The device driver .

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.

Contents

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. [1] 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. [2] 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.

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),. [3] 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. [4] 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) [5] 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 checking [6] to validate the predicates on the boolean program.

The model checker BLAST (Berkeley Lazy Abstraction Software verification Tool) [7] is used to find memory safety and incorrect locking errors in Linux kernel code. It uses an abstraction algorithm called lazy abstraction [8] 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.

Avinux [9] is another tool that facilitates the automatic analysis of Linux device drives and is built on top of bounded model checker CBMC. [10] 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. [11]

Run Time Analysis

Dynamic program analysis is performed by running the program with sufficient test inputs to produce interesting behaviors. Safe Drive [12] 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. [13] 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 3 [14] 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

Hardware operating code is usually low level and is prone to errors. The code development engineer rely on the hardware documentation which typically contains imprecise or inaccurate information. There are several Interface Definition Languages (IDL) to express the hardware functionalities. The modern OSes uses these IDLs to glue components or to hide heterogeneity, like remote procedural call IDL. The same applies to hardware functionalities as well. In this section we discuss writing device drivers in domain specific languages which helps to abstract the low level coding and use specific compilers to generate the code.

Devil [15] allows high level definition of the communication with the device. The hardware components are expressed as I/O ports and memory-mapped registers. These specifications are then converted to a set of C macros which can be called from the driver code and thus eliminates the error induced by programmer while writing low level functions. NDL [16] is an enhancement to Devil, describing the driver in terms of its operational interface. It uses the Devil's interface definition syntax and includes set of register definitions, protocols for accessing those registers and a collection of device functions. Device functions are then translated into a series of operations on that interface. For a device driver generation, one have to first write the driver functionalities in these interface specification languages and then use a compiler which will generate the low level driver code.

HAIL (Hardware Access Interface Language) [17] is another domain-specific device driver specification language. The driver developer needs to write the following.

  1. Register map description, which describes various device registers and bit fields from the device data sheet.
  2. Address space description for accessing the bus.
  3. Instantiation of the device in the particular system.
  4. Invariant specification, which constraints accessing the device.

The HAIL compiler takes these inputs and translates the specification into C code.

Hardware Software Co-design

In hardware software co-design, the designer specifies the structure and behavior of the system using finite state machines which communicate among themselves. Then a series of testing, simulation and formal verification are done on these state machines before deciding which components go into the hardware and which of these into the software. The hardware is usually done in field programmable gate arrays (FPGAs) or application specific integrated circuits (ASICs), whereas the software part is translated into low-level programming language. This approach mostly applies in embedded systems which is defined as a collection of programmable parts that interact continuously with environment through sensors. Existing techniques [18] are intended for generating simple micro-controllers and their drivers.

Standalone Driver Synthesis

In the standalone synthesis both the device and the system software are done separately. The device is modeled using any Hardware Description Language (HDL) and the software developer does not have access to the HDL specifications. The hardware developers put forth the device interface in the data sheet for the device. From the data sheet, the driver developer extracts register and memory layout of the device and the behavioral model in the form of finite state machines. This is expressed in the domain specific languages described in the Interface language section. Final step involves generating the code from these specifications.

The tool Termite [19] takes three specifications to generate the driver.

  1. Device specification : The device register, memory and interrupt services specification obtained from the device data sheet.
  2. Device class specification : This can be obtained from the relevant device I/O protocol standard. For example, for Ethernet the Ethernet LAN standard describes the common behavior of these controller devices. This is usually encoded as a set of events like packet transmission, completion of auto negotiation and link status change etc.
  3. OS specification : This describes the OS interface with the driver. More specifically the request OS can make to the driver, the order of these requests and what the OS expects the driver in return for these requests. It defines a state machine where each transition corresponds to a driver invocation by OS, the callback made by driver or a protocol specified event.

Given these specifications Termite will generate the driver implementation that translates any valid sequence of OS request into a sequence of device commands. Due to formal specification of the interfaces, Termite can generate the driver code which holds the safety and liveness properties.

Another very interesting hacking effort has been done by RevNIC, [20] which generates a driver state machine by reverse engineering an existing driver to create inter-portable and safe drivers for new platforms. To reverse engineer a driver, it wiretaps the hardware I/O operations by executing the driver using symbolic and concrete executions. The output of the wiretap is fed to a synthesizer, which reconstructs a control flow graph of the original driver from these multiple traces along with the boilerplate template for the corresponding device class. Using these methods, the researchers have ported some Windows drivers for network interfaces to other Linux and embedded operating systems.

Criticism

While many of the static analysis tools are widely used, many of the driver synthesis and verification tools have not seen widespread acceptance in practice. One of the reasons is that drivers tend to support multiple devices and the driver synthesis work usually generates one driver per device supported which can potentially lead to a large number of drivers. Another reason is drivers also do some processing and the state machine model of drivers cannot depict processing. [21]

Conclusion

The various verification and synthesis techniques surveyed in this article have their own advantages and disadvantages. For example, runtime fault isolation has performance overhead, whereas the static analysis does not cover all classes of errors. The complete automation of device driver synthesis is still in its early stages and has a promising future research direction. Progress will be facilitated if the many languages available today for interface specification can eventually consolidate into a single format, which is supported universally by device vendors and operating systems teams. The payoff from such a standardization effort could be the realization of completely automated synthesis of reliable device drivers in the future.

Related Research Articles

<span class="mw-page-title-main">Device driver</span> Software interface to attached devices

In computing, a device driver is a computer program that operates or controls a particular type of device that is attached to a computer or automaton. A driver provides a software interface to hardware devices, enabling operating systems and other computer programs to access hardware functions without needing to know precise details about the hardware being used.

In computer science, static program analysis is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution.

<span class="mw-page-title-main">Embedded system</span> Computer system with a dedicated function

An embedded system is a computer system—a combination of a computer processor, computer memory, and input/output peripheral devices—that has a dedicated function within a larger mechanical or electronic system. It is embedded as part of a complete device often including electrical or electronic hardware and mechanical parts. Because an embedded system typically controls physical operations of the machine that it is embedded within, it often has real-time computing constraints. Embedded systems control many devices in common use. In 2009, it was estimated that ninety-eight percent of all microprocessors manufactured were used in embedded systems.

In computer engineering, a hardware description language (HDL) is a specialized computer language used to describe the structure and behavior of electronic circuits, most commonly to design ASICs and program FPGAs.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

System software is software designed to provide a platform for other software. Examples of system software include operating systems (OS).

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.

<span class="mw-page-title-main">Model checking</span> Computer science field

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

Hardware abstractions are sets of routines in software that provide programs with access to hardware resources through programming interfaces. The programming interface allows all devices in a particular class C of hardware devices to be accessed through identical interfaces even though C may contain different subclasses of devices that each provide a different hardware interface.

<span class="mw-page-title-main">Linux kernel interfaces</span> An overview and comparison of the Linux kernal APIs and ABIs.

The Linux kernel provides multiple interfaces to user-space and kernel-mode code that are used for varying purposes and that have varying properties by design. There are two types of application programming interface (API) in the Linux kernel:

  1. the "kernel–user space" API; and
  2. the "kernel internal" API.

In software engineering, profiling is a form of dynamic program analysis that measures, for example, the space (memory) or time complexity of a program, the usage of particular instructions, or the frequency and duration of function calls. Most commonly, profiling information serves to aid program optimization, and more specifically, performance engineering.

Advanced Configuration and Power Interface (ACPI) is an open standard that operating systems can use to discover and configure computer hardware components, to perform power management, auto configuration, and status monitoring. It was first released in December 1996. ACPI aims to replace Advanced Power Management (APM), the MultiProcessor Specification, and the Plug and Play BIOS (PnP) Specification. ACPI brings power management under the control of the operating system, as opposed to the previous BIOS-centric system that relied on platform-specific firmware to determine power management and configuration policies. The specification is central to the Operating System-directed configuration and Power Management (OSPM) system. ACPI defines hardware abstraction interfaces between the device's firmware, the computer hardware components, and the operating systems.

This is an alphabetical list of articles pertaining specifically to software engineering.

Runtime verification is a computing system analysis and execution approach based on extracting information from a running system and using it to detect and possibly react to observed behaviors satisfying or violating certain properties. Some very particular properties, such as datarace and deadlock freedom, are typically desired to be satisfied by all systems and may be best implemented algorithmically. Other properties can be more conveniently captured as formal specifications. Runtime verification specifications are typically expressed in trace predicate formalisms, such as finite state machines, regular expressions, context-free patterns, linear temporal logics, etc., or extensions of these. This allows for a less ad-hoc approach than normal testing. However, any mechanism for monitoring an executing system is considered runtime verification, including verifying against test oracles and reference implementations. When formal requirements specifications are provided, monitors are synthesized from them and infused within the system by means of instrumentation. Runtime verification can be used for many purposes, such as security or safety policy monitoring, debugging, testing, verification, validation, profiling, fault protection, behavior modification, etc. Runtime verification avoids the complexity of traditional formal verification techniques, such as model checking and theorem proving, by analyzing only one or a few execution traces and by working directly with the actual system, thus scaling up relatively well and giving more confidence in the results of the analysis, at the expense of less coverage. Moreover, through its reflective capabilities runtime verification can be made an integral part of the target system, monitoring and guiding its execution during deployment.

In Linux systems, initrd is a scheme for loading a temporary root file system into memory, to be used as part of the Linux startup process. initrd and initramfs refer to two different methods of achieving this. Both are commonly used to make preparations before the real root file system can be mounted.

In the context of free and open-source software, proprietary software only available as a binary executable is referred to as a blob or binary blob. The term usually refers to a device driver module loaded into the kernel of an open-source operating system, and is sometimes also applied to code running outside the kernel, such as system firmware images, microcode updates, or userland programs. The term blob was first used in database management systems to describe a collection of binary data stored as a single entity.

In computer science, fault injection is a testing technique for understanding how computing systems behave when stressed in unusual ways. This can be achieved using physical- or software-based means, or using a hybrid approach. Widely studied physical fault injections include the application of high voltages, extreme temperatures and electromagnetic pulses on electronic components, such as computer memory and central processing units. By exposing components to conditions beyond their intended operating limits, computing systems can be coerced into mis-executing instructions and corrupting critical data.

Binary-code compatibility is a property of a computer system, meaning that it can run the same executable code, typically machine code for a general-purpose computer Central processing unit (CPU), that another computer system can run. Source-code compatibility, on the other hand, means that recompilation or interpretation is necessary before the program can be run on the compatible system.

<span class="mw-page-title-main">Kernel (operating system)</span> Core of a computer operating system

The kernel is a computer program at the core of a computer's operating system and generally has complete control over everything in the system. The kernel is also responsible for preventing and mitigating conflicts between different processes. It is the portion of the operating system code that is always resident in memory and facilitates interactions between hardware and software components. A full kernel controls all hardware resources via device drivers, arbitrates conflicts between processes concerning such resources, and optimizes the utilization of common resources e.g. CPU & cache usage, file systems, and network sockets. On most systems, the kernel is one of the first programs loaded on startup. It handles the rest of startup as well as memory, peripherals, and input/output (I/O) requests from software, translating them into data-processing instructions for the central processing unit.

In computer science, dynamic software updating (DSU) is a field of research pertaining to upgrading programs while they are running. DSU is not currently widely used in industry. However, researchers have developed a wide variety of systems and techniques for implementing DSU. These systems are commonly tested on real-world programs.

References

  1. ↑ Archana Ganapathi, Viji Ganapathi and David Patterson. "Windows XP kernel crash analysis". In Proceedings of the 2006 Large Installation System Administration Conference, 2006.
  2. ↑ A. Chou, J. Yang, B. Chelf, S. Hallem and D. Engler. An Empirical Study of Operating Systems Errors. In SOSP, 2001
  3. ↑ 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
  4. ↑ Jhala, Ranjit and Majumdar, Rupak. "Software model checking". In ACM Computation Survey. 2009
  5. ↑ 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.
  6. ↑ McMillan, Kenneth L. "Symbolic Model Checking". Kluwer Academic Publishers, 1993.
  7. ↑ Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre. "Software Verification with BLAST". In SPIN, 2003.
  8. ↑ Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar and Gregoire Sutre. "Lazy Abstraction", In ACM SIGPLAN-SIGACT Conference on Principles of Programming Languages, 2002.
  9. ↑ H. Post,W. Küchlin. "Integration of static analysis for linux device driver verification". In The 6th Intl. Conf. on Integrated Formal Methods, 2007.
  10. ↑ Edmund Clarke, Daniel Kroening and Flavio Lerda. "A Tool for checking ANSI-C Programs". In TACAS, 2004
  11. ↑ Thomas Ball, Mayur Naik, and Sriram K. Rajamani. "From symptom to cause: localizing errors in counterexample traces". ACM SIGPLAN Notices, 2003.
  12. ↑ Feng 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.
  13. ↑ Michael M. Swift, Steven Martin, Henry M. Levy, and Susan J. Eggers. "Nooks: an architecture for reliable device drivers ". In 10th ACM SIGOPS, 2002.
  14. ↑ Jorrit 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.
  15. ↑ Fabrice Merillon, Laurent Reveillere, Charles Consel, Renaud Marlet, and Gilles Muller. " Devil: an IDL for hardware programming". In Proceedings of the 4th conference on Symposium on Operating System Design & Implementation, Vol. 4, 2000.
  16. ↑ Christopher L. Conway and Stephen A. Edwards. "NDL: a domain-specific language for device drivers". ACM SIGPLAN Notices 39, 2004.
  17. ↑ J. Sun, W. Yuan, M. Kallahalla, and N. Islam. "HAIL: A Language for Easy and Correct Device Access". In Proc. of ACM Conference on Embedded Software, 2005.
  18. ↑ Felice Balarin et al. "Hardware-Software Co-design of Embedded Systems. The POLIS Approach." Kluwer Academic Publishers, 1997.
  19. ↑ Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur, and Gernot Heiser. "Automatic device driver synthesis with Termite". In Proceedings of the 22nd ACM Symposium on Operating Systems Principles, 2009.
  20. ↑ Vitaly Chipounov and George Candea. "Reverse Engineering of Binary Device Drivers with RevNIC". 5th ACM SIGOPS/EuroSys, 2010.
  21. ↑ Asim Kadav and Michael M. Swift "Understanding Modern Device Drivers" In Proceedings of the 17th ACM Conference on Architectural Support for Programming Languages and Operating Systems
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.