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