Static Driver Verifier (SDV) is a thorough compile-time static verification tool designed for drivers. SDV finds serious errors that are unlikely to be encountered even in thorough testing. SDV systematically analyzes the source code of Windows drivers that are written in the C language. Using a set of interface rules and a model of the operating system, it determines whether the driver interacts properly with the Windows operating system. SDV can verify device drivers (function drivers, filter drivers, and bus drivers) that use the Windows Driver Model (WDM), Kernel-Mode Driver Framework (KMDF), or NDIS miniport drivers. SDV is designed to be used throughout the development cycle. 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. SDV runs on Microsoft Windows XP and later versions of Windows and supports all x86-based and x64-based build environments. SDV is included in the Windows Driver Kit (WDK). What’s New for Static Driver Verifier in Windows 7 | • | SDV support for NDIS miniport drivers. SDV now has support for the following NDIS miniport versions: NDIS 6.0, 6.1, 6.2 and 6.20. | | • | An expanded set of rules for WDM and KMDF. For Windows 7, SDV can detect more issues related to reliability, security, IRQL levels, synchronization, and correct object lifetime management. | | • | Role type declarations. To use SDV, you must add role type declarations to your source header files. Role types are function typedefs for driver entry points. Role type declarations enable SDV to identify the entry points in your driver and perform more accurate analysis. Role types also act as documentation by describing the intended role of a driver entry point routine (or callback function) and the routine’s return value and parameter types. Using role types enables Static Driver Verifier to discover complex inter-procedural bugs that may cause a system to hang or stop responding. | | • | Driver property rules. SDV for Windows 7 internally uses a set of driver property rules to identify specific characteristics of a driver and apply a set of more specific, simpler rules during analysis. These rules improve the accuracy of the analysis and reduce the likelihood of a timeout or failure. SDV uses these property rules automatically; you do not have to do anything other than run SDV to take advantage of these rules. | | • | Per-entry verification. Per-entry verification allows SDV to do a more detailed investigation of drivers, by segmenting the driver. This technique identifies groups of driver callbacks that have well defined execution ordering, and submits each group of related callbacks to the static analysis engine as a unit. Using this technique results in fewer timeouts and failures. |
| • | Improved performance, scalability, and accuracy. SDV for Windows 7 provides the following improvements: | • | For WDM drivers: | • | Reduces average analysis runtime to less than 40 minutes on a 4-processor computer. | | • | Reduces the number of non-results (timeouts, and so on) by half compared to SDV in the Windows Vista WDK. | | • | Improves defect detection. The number of true defects detected in driver code is 95% of those identified. This is an improvement from 73% in the Windows Vista version. |
| | • | For KMDF drivers: | • | Reduces average runtime to less than 20 minutes on a 4-processor computer. | | • | Reduces the number of non-results (timeouts, and so on) to almost zero. |
| | • | For WDK, KMDF, and NDIS drivers using per-entry verification (PEV): | • | Reduces the number of non-results (timeouts, and so on) by 10 times when PEV is enabled. Users can choose to enable or disable this feature to analyze specific parts of a driver by using the /refine option. |
|
|
High Quality Drivers and WDK Samples | • | Microsoft WDM, KMDF, and NDIS miniport drivers that ship with the operating system have been analyzed with SDV and the defects have been fixed. | | • | WDM, KMDF, and NDIS sample drivers in the WDK have been analyzed with SDV and the defects have been fixed. These WDK samples serve as high quality models for your new drivers. |
General SDV Static Analysis Tools - WinHEC Static Tools for Driver Development - WHDC Labs SDV Background  | "Microsoft bug-checking tools promise fewer crashes" - CNET News.com, May 26, 2006 | | “Building a Better Bug Trap” - The Economist, June 19, 2003 [reprint] | | “Microsoft's Secret Bug Squasher,” Wired News, November 10, 2005 |  | "Providing a Template for Tech Transfer" | | Bill Gates, Remarks at 17th Annual ACM Conference on Object-Oriented Programming, Systems, Languages and Application | | SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft (PDF file) | | SLAM Project at Microsoft Research: Debugging System Software via Static Analysis |
| |
