Device driver synthesis and verification
The Berkeley Open Infrastructure for Network Computing (BOINC) project found that OS crashes are predominantly caused by poorly written device driver code.
Less human interaction in the development process and proper specification of the device and operating systems can lead to more reliable drivers.
An automated synthesis technique can help the vendors in providing drivers to support any devices on any operating system.
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.
Many type-safe languages allow memory safety violations resulting from unsafe type casting to be detected by compiler.
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.
The back end analysis engine SLAM used model checking and symbolic execution for compile time static verification.
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 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.
Safe Drive[12] is a low overhead system for detecting and recovering from type safety violations in device drivers.
Minix 3[14] is an operating system which can isolate major faults, defects are detected and failing components are replaced on the fly.
An alternative to verification and isolation of faults is to deploy techniques in device driver development process to make it more robust.
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.
In hardware software co-design, the designer specifies the structure and behavior of the system using finite state machines which communicate among themselves.
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.
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.
Due to formal specification of the interfaces, Termite can generate the driver code which holds the safety and liveness properties.
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.
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.
