Introducing Static Driver Verifier
Compile-time verification for WDM kernel-mode drivers
Static Driver Verifier (SDV) is a static analysis tool designed to automatically inspect C code in a Windows driver at compile time, targeting violations of Windows Driver Model (WDM) usage rules. SDV can be characterized as a compile-time version of Driver Verifier, although these two tools are quite different.
This overview describes how SDV works, and provides insight into the requirements and limitations for using SDV to verify Windows drivers.
On This Page
 | About Static Driver Verifier |
| SDV Verification Process |
| SDV Guidelines for Drivers |
| How to Run Static Driver Verifier |
About Static Driver Verifier
Developing Windows drivers can be challenging because:
| • | Drivers are asynchronous and massively reentrant. |
| • | Drivers use many complex rules, based on hundreds of kernel-mode application programming interfaces (APIs). |
| • | Driver models are evolutionary and age over time. |
Testing device drivers is limited by these factors:
| • | You cannot observe an error in the interaction between the driver and the operating system. Drivers can violate implicit usage rules, resulting in a crash or improper behavior; however, it is difficult to detect the root cause of an error when developing and testing drivers. |
| • | Drivers that normally work correctly can have subtle errors that occur only in exceptional situations. Such situations are hard to exercise in traditional testing, which cannot adequately detect the possible error paths through the driver code. |
SDV enhances the ability to observe errors when testing drivers by defining rules for proper use of kernel-mode APIs and then monitoring the driver's compliance with those rules.
SDV explores code paths in a device driver by symbolically executing the source code. It places a driver in a hostile environment and systematically tests all code paths by looking for violations of WDM usage rules. The symbolic execution makes very few assumptions about the state of the operating system or the initial state of the driver, so it can exercise situations that are difficult to exercise by traditional testing.
The set of rules that are packaged with SDV define how device drivers should use the WDM API. The categories of rules tested include I/O request packet (IRP), interrupt request level (IRQL), Plug and Play (PnP), power management (PM), Windows Management Instrumentation (WMI), synchronization, and others.
SDV is designed to be run on a driver after driver code is complete, so that the driver can be compiled and built. SDV runs on the Microsoft Windows XP operating system and later versions of Windows and supports free and checked build environments for x86 and x64. SDV is provided in the Microsoft Windows Driver Kit (WDK) in the \tools\sdv subdirectory.
SDV Verification Process
SDV uses an advanced model-checking engine (SLAM) that performs rule verification, based on the following input:
| • | Driver source code |
| • | One or more SDV rules |
The verification engine processes this input and attempts to prove that the driver violated the rules by interacting improperly with the SDV operating system model.
SDV performs a three-step process:
1. | Build. SDV compiles, links, and builds the driver, using the standard build utility in the WDK. |
2. | Scan. SDV scans the driver source code and assembles a list of driver entry points it discovers into a file that then guides the verification process. The developer should validate this list. |
3. | Check. SDV prepares for and verifies the driver by using the rules that the developer selected for the verification. |
The SDV verification engine then verifies one rule at a time, until it verifies all selected rules. While SDV performs the verification it writes status messages to the command line, along with messages that report errors in each step (see below).
When SDV proves that the driver violated a rule, it declares a defect and assigns a Fail result to the verification. If it cannot prove a violation, it assigns a Pass result to the verification.
A rule can include several elements:
| • | The state variables that capture states relevant to the verification process on the driver code. |
| • | Driver actions that can change the state, typically a function call or function return. SDV monitors the driver code for occurrences of these actions. |
| • | Conditional expressions that evaluate the state at the point of the driver action. |
| • | Assignment statements that change the value of the state variables to represent the way in which the driver action changed the state of the driver's environment. |
SDV Guidelines for Drivers
For SDV to verify a driver, it must be able to interpret the driver's entry points and the code in other driver functions. SDV is able to verify only drivers with the following characteristics:
| • | Drivers and libraries written in C and contained in source files with a .c file name extension. |
| • | WDM-compliant device drivers (function drivers, filter drivers, and bus drivers), and file system filter drivers. |
For large drivers, SDV might not produce useful results. Although we do not have an accurate measure to judge when a driver is too large for SDV, experience shows that when the driver code size exceeds 50 KB lines, SDV becomes less useful.
Standard Driver Routines. SDV expects that the driver's standard routines use the function prototypes documented in the WDK. When SDV encounters driver entry points that it cannot interpret because of improper function prototypes, it might declare a syntax error.
DriverEntry Routines. SDV must be able to find and correctly interpret the entry points for the driver's standard routines in the DriverEntry routine. SDV expects the syntax of the driver object's dispatch table to be similar to the standard format described in the WDK documentation.
SDV Status Messages in the Command-line Windows
How to Run Static Driver Verifier
Before running SDV, the developer performs the following tasks, in any order.
| • | Select a driver |
| • | Select rules |
| • | Process the driver's libraries |
| • | Examine the Options file |
Following are the basic steps for using SDV. For best practices and details that experienced users need to know, see the WDK documentation.
To run SDV
1. | Open a WDK build environment window | ||||||
2. | Navigate to the driver's sources directory | ||||||
3. | Start a verification | ||||||
4. | View the results
| ||||||
5. | Resolve errors and run SDV again. Fix the errors that SDV detected in the driver. Then clean the directory and run SDV again. |
SDV Defect Viewer
