"Automatic Device Driver Isolation Protects Against Bugs in Operating Systems"

The kernel of an operating system serves as a translator between the user and the machine. Developers can isolate the operating system's device drivers to improve kernel reliability and prevent a failure in one component from affecting other components. However, isolation necessitates impractical amounts of human effort. A group of Penn State researchers created a framework that could automate and reduce the amount of manual work required for device driver isolation in the presence of challenging kernel patterns. To effectively isolate device drivers while maintaining kernel-driver communication, developers had to inspect the large and complex communication interface between a driver and the kernel. They had to determine what data needed to be synchronized by examining all interactions between the driver and the kernel. They also had to deal with difficult synchronization patterns like data concurrency, requiring writing thousands of lines of code to keep operations running smoothly. The team created KSplit, a method for automatically analyzing the shared driver-kernel state and computing any synchronization requirements for only this shared state. The program also identifies areas that require manual intervention, reducing manual workload to coding and data marshaling. The solution was tested with 354 device drivers on nine subsystems of a Linux kernel. KSplit required manual updates to 53 of 2,476 lines of code, which were automatically generated interface specifications, and 19 additional changes to the driver's code for one complex driver. That is less than 3 percent of the manual labor required in the absence of KSplit. This article continues to discuss the purpose, testing, and support behind the KSplit framework. 

Penn State reports "Automatic Device Driver Isolation Protects Against Bugs in Operating Systems"