Microsoft's Static Driver Verifier (SDV) pioneered the use of software model checking for ensuring that device drivers correctly use operating system (OS) APIs.However, the verification methodology has been difficult to extend in order to support either (a) new classes of drivers for which SDV does not already have a harness and stubs, or (b) memory-corruption properties.Any attempt to apply SDV out-of-the-box results in either false alarms due to the lack of environment modeling, or scalability issues when finding deeply nested bugs in the presence of a very large number of memory accesses.In this paper, we describe our experience designing and shipping a new class of checks known as angelic checks through SDV with the aid of angelic verification (AV) [1] technology, over a period of 4 years.AV pairs a precise inter-procedural assertion checker with automatic inference of likely specifications for the environment.AV helps compensate for the lack of environment modeling and regains scalability by making it possible to find deeply nested bugs, even for complex memorycorruption properties.These new rules have together found over a hundred confirmed defects during internal deployment at Microsoft, including several previously unknown high-impact potential security vulnerabilities.AV considerably increases the reach of SDV, both in terms of drivers as well as rules that it can support effectively.

Bugs in kernel-level device drivers cause 85% of the system crashes in the Windows XP operating system [44]. One of the sources of these errors is the complexity of the Windows driver API itself: programmers must master a complex set of rules about how to use the driver API in order to create drivers that are good clients of the kernel. We have built a static analysis engine that finds API usage errors in C programs. The Static Driver Verifier tool (SDV) uses this engine to find kernel API usage errors in a driver. SDV includes models of the OS and the environment of the device driver, and over sixty API usage rules. SDV is intended to be used by driver developers "out of the box." Thus, it has stringent requirements: (1) complete automation with no input from the user; (2) a low rate of false errors. We discuss the techniques used in SDV to meet these requirements, and empirical results from running SDV on over one hundred Windows device drivers.