Thorough Static Analysis of Device Drivers

Bugs in kernel-level device drivers cause 85% of the system
crashes in the Windows XP operating system [44]. One of
the sources of these errors is the complexity of the Windows
driver API itself: programmers must master a complex set
of rules about how to use the driver API in order to create
drivers that are good clients of the kernel. We have built
a static analysis engine that finds API usage errors in C
programs. The Static Driver Verifier tool (SDV) uses this
engine to find kernel API usage errors in a driver. SDV
includes models of the OS and the environment of the device
driver, and over sixty API usage rules. SDV is intended to
be used by driver developers “out of the box.” Thus, it has
stringent requirements: (1) complete automation with no
input from the user; (2) a low rate of false errors. We discuss
the techniques used in SDV to meet these requirements, and
empirical results from running SDV on over one hundred
Windows device drivers.