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
.gif)
Introduction
SDV and Microsoft Research
Using SDV to Investigate Bugs
Using SDV to Advance WDK Samples
Using SDV to Learn Best Practices
An Attack on False Positives
Resources
Introduction
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:
Choice of Problem. "We chose a critical, but not insurmountable, problem domain to work on (device drivers). ...We had access to the Windows source code and the source code of the device drivers. We also had extensive access to the foremost experts on device drivers and Windows."
Standing on Shoulders. "SLAM builds on decades of research in formal methods and programming languages. We are fortunate to have had many people contribute to SLAM and SDV, both in Microsoft Research, the Windows Division, as well as from outside Microsoft."
Research Environment. "Microsoft's industrial research environment and general hands-on/can-do culture allowed us great freedom in which to attempt a risky solution to a big problem, and provided support when we needed it the most."
Software Engineering. "We developed SLAM in an 'open' architectural style using very simple conceptual interfaces for each of its core components. This allowed us to experiment quickly with various tools and settle on a set of algorithms that we felt best solved the problem. This architecture also allows us to reconfigure the various components easily in response to new problems."
The Right Tools for the Job. "We developed SLAM using the French research institute INRIA's Objective Caml functional programming language. The expressiveness of this language and robustness of its implementations provided a great productivity boost."
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.
Bill Gates at OOPSLA 2002: We've created a number of things to do rich static analysis. We actually went out and bought for a little over $30 million a company that was in the business of building those kinds of tools, and we said now we want you to focus on applying these tools to large-scale software systems, the kind of system we have in the source code of Windows or Office, and see how far we can get on this. We also went back and say, OK, what is the state-of-the-art in terms of being able to prove programs, prove that a program behaves in a certain way? This is the kind of problem that has been out there for many decades. When I dropped out of Harvard, this was an interesting problem that was being worked on, and actually at the time I thought, well, if I go and start a company it will be too bad, I'll miss some of the big breakthroughs in proving software programs because I'll be off writing payroll checks. And it turns out I didn't miss all that much in terms of rapid progress -- (laughter) -- which now has become, I'd say, in a sense, a very urgent problem. And although a full general solution to that is in some ways unachievable, for many very interesting properties this ideas of proof has come a long ways in helping us quite substantially just in the last year. We call the system that does this kind of proof, it's a model-checking system. You describe the constraints, including things as simple as nobody should acquire the lock if they've already acquired it, nobody should release it if they haven't acquired it, certain things about the multi-threading aspect of the code that you want to make sure work very well. And you describe those things literally, in this case in the C code itself, and then the analyzer goes through and reduces the program, takes away anything that doesn't affect the path analysis that it's trying to go through to determine is there some path through the program that violates the constraints. The initial domain we applied this in was in device drivers. 17th Annual ACM Conference on Object-Oriented Programming, Systems, Languages and Application |
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:
Windows Vista Inbox Investigation. This project included running SDV on kernel-mode drivers in the Windows Vista sources and investigating the results. The results helped find bugs in drivers to be included in Windows Vista
WDK Investigation. This investigation was run on the WDM and C-only drivers in the WDK. All defects found were classified-resulting in bugs fixed in the WDK or in SDV, leading to improved quality of both the sample drivers and SDV itself. This project is discussed in more depth in the following sections.
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.
"Microsoft's Secret Bug Squasher" Because device drivers run deep within the operating system, they are hard to write and hard to debug. And when they fail, they can take down the whole computer. "If they go bad, the whole OS can go bad," says Tom Ball, a scientist at Microsoft Research. But in a little-noticed project percolating in Redmond, the world's biggest single producer of software bugs is pushing the envelope on an anti-bug technology that promises to make the Windows operating system a whole lot more reliable, and may eventually raise the bar for dependable software throughout the industry. Microsoft has developed a tool called the Static Driver Verifier, or SDV, that uses "model checking" to analyze the source code for Windows device drivers and see if the code that the programmer wrote matches a mathematical model of what a Windows device driver should actually do. ... It's a deceptively simple-sounding breakthrough that encapsulates some remarkable software engineering theory. When Bill Gates announced that the technology was under development at the 2002 [WinHEC] Conference, he [said], "Now in some very key areas--for example, driver verification--we're building tools that can do actual proof about the software and how it works in order to guarantee the reliability," said Gates. ... "It finds bugs via static analysis (compile-time analysis) of the code rather than run-time analysis," says Ball, who led the Slam project with Sriram Rajamani. A typical driver can be checked in a few minutes, but some complex drivers can take as long as 20 minutes to analyze. Wired News, November 10, 2005 |
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.
sys
It is a bug to pend Irp without checking Irp->Cancel.
mouclass
The driver is passing NULL to ExFreePool, which can cause a bugcheck.
moufiltr
The dispatch routine is returning STATUS_PENDING, but it has also called IoCompleteRequest on the incoming IRP.
daytona
There is a potential for unbounded recursion. The driver has called IoStartNextPacket inside startIo but it has not set the DeferredStartIo attribute of the device object to true.
It is a bug to pend Irp without checking Irp->Cancel.
fakemodem
The KeReleaseSpinLock should only be called at IRQL = DISPATCH_LEVEL.
The driver is passing NULL to ExFreePool, which can cause a bugcheck.
bulltlp3
KeDelayExecutionThread should only be called at <=APC_LEVEL
pscr
IoCompleteRequest has been called while holding a spin lock
One of the dispatch routines does not return at the same IRQL level at which it was called.
fdc
The driver is passing NULL to IoCallDriver.
The driver is passing NULL to ExFreePool, which can cause a bugcheck.
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.
"Building a Better Bug Trap" A study published in 2002 by America's National Institute of Standards and Technology (NIST) estimated that software bugs are so common that their cost to the American economy alone is $60 billion a year or about 0.6% of gross domestic product. ... Programmers spend far longer fixing bugs in existing code than they do writing new code. According to NIST, 80% of the software-development costs of a typical project are spent on identifying and fixing defects. ... Hence the growing interest in software tools that can analyse code as it is being written, and automate the testing and quality-assurance procedures. The goal, says Amitabh Srivastava, a distinguished engineer at Microsoft Research, is to achieve predictable quality in software-making, just as in carmaking. "The more you automate the process, the more reliable it is," he says. In short, use software to make software better. ... Opinion is divided as to whether programmers will welcome or reject such tools. Mr Srivastava is optimistic, noting that the important thing is that metrics are used appropriately--to guide training rather than punishment. "If you find out what the fault was, and use training to make sure that it doesn't happen again, then it's a positive thing," he says. The Economist, June 19, 2003 |
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:
If the assumption is justified, adding a comment in code is good practice; it tells subsequent developers that someone thought about the issue.
If the assumption proves to be false, a checked build is likely to diagnose the problem in a way that is clear and easy to find. If the assumption is not justified, the code should be changed.
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.
Resources
Bill Gates, Remarks at 17th Annual ACM Conference on Object-Oriented Programming, Systems, Languages and Application, Seattle, Washington, November 8, 2002
http://www.microsoft.com/en-us/news/press/2002/Nov02/11-08OOPSLAPR.aspx
"Building a Better Bug Trap," The Economist, June 19, 2003
http://www.klocwork.com/company/downloads/economist.html [reprint]
http://www.economist.com/science/tq/displayStory.cfm?story_id=1841081 [subscription]
"Microsoft's Secret Bug Squasher," Wired News, November 10, 2005
http://www.wired.com/news/technology/bugs/0,2924,69375,00.html
MSDN Webcast: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods Inside Microsoft
http://msevents.microsoft.com/cui/WebCastEventDetails.aspx?EventID=1032273456&EventCategory=5&culture=en-US&CountryCode=US
"Providing a Template for Tech Transfer"
http://research.microsoft.com/displayArticle.aspx?id=1338
SLAM Project at Microsoft Research: Debugging System Software via Static Analysis
http://research.microsoft.com/slam/
SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft
ftp://ftp.research.microsoft.com/pub/tr/tr-2004-08.pdf
"Static Driver Verifier" in the WDK
See the Driver Development Tools section of the WDK
"Static Driver Verifier - Finding Driver Bugs at Compile Time" on WHDC Web site
http://msdn.microsoft.com/en-us/windows/hardware/gg487498.aspx
.gif){kind=icon}
