Publication

Matthew J. Renzelmann, Asim Kadav, and Michael M. Swift. SymDrive: Testing Drivers without Devices. In OSDI'12.

PDF: here.

Overview

Device-driver development and testing is a complex and error-prone undertaking. For example, a single driver may support dozens of devices, and a developer may not have access to any of them. As a result, many Linux driver patches include the comment "compile tested only." Furthermore, testing error-handling code is difficult, as it requires faulty inputs from the device.

SymDrive is a system for testing Linux and FreeBSD drivers without their devices. The system uses symbolic execution to remove the need for hardware, and provides three new features beyond prior symbolic-testing tools. First, SymDrive greatly reduces the effort of testing a new driver with a static-analysis and source-to-source transformation tool. Second, SymDrive allows checkers to be written as ordinary C and execute in the kernel, where they have full access to kernel and driver state. Finally, SymDrive provides an execution-tracing tool to identify how a patch changes I/O to the device and to compare device driver implementations. In applying SymDrive to 21 Linux drivers and 5 FreeBSD drivers, we found 39 bugs.

The figure below outlines the architecture of SymDrive.

More Information

If you'd like more information about SymDrive, please visit the links at the top of each page, or email us.

This work is supported by the National Science Foundation grants CNS-0745517 and CNS-0915363 and by a gift from Google.