SDV Experiences at Microsoft
Updated: October 19, 2010
This article describes some of Microsoft's experience using SDV to advance driver quality, and offers insight into how driver developers can adopt the use of SDV in regular development and testing processes.
On This Page
Static Driver Verifier (SDV) is a rule-based, compile-time static analysis tool for verification of Windows drivers written in C code. SDV verifies a driver against a set of precise rules for the use of Windows device driver interfaces, and then reports any violations of these rules.
For information about how SDV works, see Static Driver Verifier in the Windows Driver Kit (WDK) documentation. All references discussed in this article are listed in the "Resources" section at the end of this article.
SDV and Microsoft Research
The Microsoft Research (MSR) Software Productivity Tools team invested several years' work to create an engine that performs an automatic check for whether a C-based program correctly uses the interfaces to an external library. This project, called SLAM at MSR, resulted in a powerful analysis engine that has been incorporated into SDV.
To quote the Microsoft Research team, from "Providing a Template for Tech Transfer" on the MSR Web site:
SDV is now used within Microsoft and is included in releases of the Windows Driver Kit (WDK). SDV is one of the tools that enables Microsoft and its partners to deliver higher-quality device drivers.
Using SDV to Investigate Bugs
Microsoft has been using SDV to test sample drivers included in the Windows Driver Kit (WDK) and against kernel-mode drivers included in the Microsoft Windows operating system.
Microsoft uses a wide range of quality checks and tools during the driver development cycle to find bugs and verify quality, including SDV, Driver Verifier, PREfast, event tracing tools, and WinDbg. These and many additional testing tools are available in the WDK for Windows driver developers.
You should run SDV as soon as the basic structure of a driver is in place, and continue to run it as you make changes to the driver. The Windows test teams have been running investigations against Windows drivers and WDK sample drivers, and have found bugs that couldn't be found through other extensive test and evaluation methods.
Some significant projects in the Windows Division include:
These SDV investigations have contributed to ensuring that the large set of drivers included with the Windows operating system represents the highest quality drivers ever included with an operating system.
Using SDV to Advance WDK Samples
The Windows Driver Kit provides sample drivers that developers use in their kernel-mode software. In many cases, developers clone these samples or include "snippets" from these samples to create drivers for their unique hardware. The Static Driver Verifier investigation was run against WDK driver sample code in Windows Vista Build 5043. This project provides an interesting case, illustrating what SDV can detect. These sample drivers had already gone through the rigorous development and testing process at Microsoft for verifying quality. In some cases, the sample drivers had been included in earlier versions of Windows 2000 and Windows XP.
Microsoft has been continually improving the quality of driver samples in each release of Windows and in successive releases of the WDK. The identification and fixing of the defects found in this SDV investigation have particularly strong impact, because these samples are used by so many developers in other drivers.
SDV found bugs in sample drivers that all other methods failed to find: these are well-tested drivers, but testing (even accompanied with Driver Verifier) could not provide enough coverage to find these obscure bugs. Moreover, sources of these sample drivers (or the majority of them) were available to the entire world to study and inspect. These bugs, however, had not been detected previously, but were found by the SDV tool.
Finding and fixing these bugs was an important part of the code quality efforts undertaken by Microsoft to improve quality of drivers for Windows Vista. The sample drivers were the most important target for SDV, because they set code styles for other drivers.
The defects found in older driver samples are also instructive, in that many of these errors are the result of earlier coding styles-common practices in kernel-mode development before Microsoft began providing tools such as Driver Verifier, along with extensive information about how to create stable, secure kernel-mode drivers.
The following list provides a glimpse of some of the critical bugs found by SDV in WDK sample drivers, which driver development teams subsequently fixed.
Using SDV to Learn Best Practices
Developers at Microsoft who are using Static Driver Verifier in the development and testing life cycle of kernel-mode drivers are finding that SDV is a good tutor.
SDV helps driver developers identify and use good practices. By presenting the rules in its results, SDV helps to enforce the good techniques that senior developers should know, and it alerts new driver developers to best practices that result in better-quality drivers.
An Attack on False Positives
Verification tools such as PREfast and SDV produce reports with obvious errors, but some results are "false positives," creating a certain amount of "noise" in some results. Running SDV investigations against Windows 7 code produces good results, with regard to true versus false positives.
The SDV team at Microsoft is continually improving SDV by investigating all false positive reports that appear in SDV investigations run against drivers for Windows or the WDK. The information is being used to improve SDV, by adding and refining rules. SDV reports a significantly reduced number of false defects. For a Window 7 WDM driver, the number of true defects detected in driver code is typically 95% of those identified.
In general, investigations show that a false positive indicates that the code is ambiguous in some way. When a developer encounters a false positive in SDV results, a best practice is to insert a comment at the location of the correct-but-ambiguous code, especially for the benefit of developers who will need to maintain the code in the future. In some cases, SDV reports errors that the developer knows cannot actually occur. However, the "false positive" in this case could indicate an assumption made by the developer that might or might not be justified:
To be useful, a tool must strike a balance between being too noisy and missing possible errors. Effective use of SDV takes that balance into account. Each potential defect should be evaluated on its own merits: some need to be acted upon, others ignored. Good programming judgment and careful use of comments or other appropriate records will make it easier to determine whether your SDV results are noise or reflect actual defects.
At Microsoft, the experience so far with SDV has shown that it is a valuable asset in the effort to build and ensure high-quality kernel-mode drivers. The results in advancing Windows driver quality, and Microsoft developers' experience, make Static Driver Verifier an extremely valuable, cost-effective addition to the Windows driver development process.
Bill Gates, Remarks at 17th Annual ACM Conference on Object-Oriented Programming, Systems, Languages and Application, Seattle, Washington, November 8, 2002
"Building a Better Bug Trap," The Economist, June 19, 2003
"Microsoft's Secret Bug Squasher," Wired News, November 10, 2005
MSDN Webcast: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods Inside Microsoft
"Providing a Template for Tech Transfer"
SLAM Project at Microsoft Research: Debugging System Software via Static Analysis
SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft
"Static Driver Verifier" in the WDK
"Static Driver Verifier - Finding Driver Bugs at Compile Time" on WHDC Web site