| Static verification tool "slams" Windows driver bugs |
Nov. 30, 2005
A five-year-old Microsoft project is starting to yield higher quality Windows device drivers, Microsoft researchers say. The Static Driver Verifier tool, included in the beta release of the Windows Driver Foundation, analyzes code paths in a device driver by symbolically executing the source code within a "hostile environment," according to the tool's developers.
When Windows crashes or presents the user with a problem dialog, the end user naturally perceives it to be a failure of the operating system. But, in many cases, the crash actually results from a fault in a device driver, rather than in the operating system itself. Consequently, Microsoft considers enhanced device driver quality to be a key aspect of improving Windows user satisfaction, especially because many Windows drivers originate with third party hardware suppliers.
About the Static Driver Verifier
The Static Driver Verifier (SDV) tool is a product of the SLAM project that is investigating the relationships between software specifications, languages, analysis, and model checking. The project uses ideas from symbolic model checking, program analysis, and theorem proving to check that a C program correctly uses the interface to an external library.
SDV uses the SLAM analysis engine to check device driver source code against a set of rules that define what it means for a device driver to properly interact with the Windows operating system kernel. Basically, SDV consists of three parts: a set of rules; a model of the operating system; and a verification engine.
Editor's note: after searching in vain for a definition of what SLAM -- obviously an acronym -- stands for, we found the following interesting statement in the SLAM history whitepaper on Microsoft's website: "SLAM originally was an acronym but we found it too cumbersome to explain. We now prefer to think of 'slamming' the bugs in a program." Actually, rumor has it that "SLAM" originally stood for "Software, Languages, Analysis, and Modeling."
Version 1.3 of SDV was publicly demonstrated at the Driver Developer's Conference in November of 2003. Attendees were given an opportunity to run SDV on their own drivers. SDV's developers reported that almost everyone who did so found at least one bug in their drivers. Furthermore, according to Microsoft, about 70 percent of the errors that SDV finds are true driver errors.
Currently, SDV is distributed as part of the Beta3 CD of the WDF Beta program.
What's WDF?
Microsoft Research describes the Windows Driver Foundation (WDF) as Microsoft's strategy for next-generation Windows drivers. "WDF defines a single driver model that supports the creation of object-oriented, event-driven drivers for either kernel mode or user mode," the WDF website states. "It simplifies driver development and maintenance by implementing common features, providing intelligent defaults, and managing most interactions with the operating system. With WDF, driver writers can focus on their device hardware, rather than on the operating system."
WDF comprises the following components: - Kernel-mode driver framework
- User-mode driver framework
- Driver verification tools
More info on SDV and SLAM
More details about SDV and SLAM are available from the SLAM project website, and from these documents:
Related stories:
(Click here for further information)
|
|
|
|
|
|
|
news feed