experts. We tested them on drivers with injected bugs, then ran SDV with the rules on real Windows drivers. We discussed the bugs found by the rules with driver owners and API experts to refine the rules. At that time, a senior manager said, “It takes a Ph.D. to develop API rules.” Since then, we’ve invested significant effort in creating a discipline for writing SLIC rules and spreading it among device-driver API developers and testers.

In 2007, the SDV team refined the API rules and formulated a set of guidelines for rule development and driver environment model construction. This helped us transfer rule development to two software engineers with backgrounds far removed from formal verification, enabling them to succeed and later spread this form of rule development to others. Since 2007, driver API teams have been using summer interns to develop new API rules for WDF, NDIS, StorPort, and MPIO APIs and for an API used to write file system mini-filters (such as antivi-ruses) and Windows services. Remarkably, all interns have written API rules that found true bugs in real drivers.

SDV today includes more than 470 API rules. The latest version SDV 2.0 (released with Windows 7 in 2009) includes more than 210 API rules for the WDM, WDF, and NDIS APIs, of which only 60 were written by formal verification experts. The remaining 150 were written or modified from earlier drafts by software engineers or interns with no experience in formal verification.

Worth noting is that the SLIC rules for WDF were developed during the design phase of WDF, whereas the WDM rules were developed long after WDM came into existence. The formalization of the WDF rules influenced WDF design; if a rule could not be expressed naturally in SLIC, the WDF designers tried to refactor the API to make it easier to verify. This experience showed that verification tools (such as SLAM) can be forward-looking design aids, in addition to being checkers for legacy APIs (such as WDM).

Scripts. SDV includes a set of scripts that perform various functions: combining rules and environment models; detecting source files of a driver and its build parameters; running the SLIC compiler on rules and the C compiler

A unique SLAM
contribution is
the complete
automation
of CEGAR for
software written
in expressive
programming
languages
(such as C).

on a driver’s and environment model’s source code to generate an intermediate representation (IR); invoking SLAM on the generated IR; and reporting the summary of the results and error traces for bugs found by SLAM in a GUI.

The SDV team worked hard to ensure these scripts would provide a very high degree of automation for the user. The user need not specify anything other than the build scripts used to build the driver.

SDV Experience

The first version of SDV ( 1. 3, not released externally outside Microsoft) found, on average, one real bug per driver in 30 sample drivers shipped with the Driver Development Kit (DDK) for Windows Server 2003. These sample drivers were already well tested. Eliminating defects in the WDK samples is important since code from sample drivers is often copied by third-party driver developers.

Versions 1. 4 and 1. 5 of SDV were applied to Windows Vista drivers. In the sample WDM drivers shipped with the Vista WDK (WDK, the renamed DDK), SDV found, on average, approximately one real bug per two drivers. These samples were mostly modifications of sample drivers from the Windows Server 2003 DDK, with fixes applied for the defects found by SDV 1. 3. The newly found defects were due to improvements in the set of SDV rules and to defects introduced due to modifications in the drivers.

For Windows Server 2008, SDV version 1. 6 contained new rules for WDF drivers, with which SDV found one real bug per three WDF sample drivers. The low bug count is explained by simplicity of the WDF driver model described earlier and co-development of sample drivers, together with the WDF rules.

For the Windows 7 WDK, SDV 2.0 found, on average, one new real bug per WDF sample driver and few bugs on all the WDM sample drivers. This data is explained by more focused efforts to refine WDF rules and few modifications in the WDM sample drivers. SDV 2.0 shipped with 74 WDM rules, 94 WDF rules, and 36 NDIS rules. On WDM drivers, 90% of the defects reported by SDV are true bugs, and the rest are false errors. Further, SDV reports nonresults (such as timeouts