Model checking is often called “push-button” technology, 16 giving the impression that the user simply gives the system to the model checker and receives useful output about errors in the system, with state-space explosion being the only obstacle. In practice, in addition to state-space explosion, several other obstacles can inhibit model checking being a “ push-button” technology: First, users must specify the properties they want to check, without which there is nothing for a model checker to do. In complex systems (such as the Windows driver interface), specifying such properties is difficult, and these properties must be debugged. Second, due to the state-explosion problem, the code analyzed by the model checker is not the full system in all its gory complexity but rather the composition of some detailed component (like a device driver) with a so-called “environment model” that is a highly abstract, human-written description of the other components of the system—in our case, kernel procedures of the Windows operating system. Third, to be a practical tool in the toolbox of a driver developer, the model checker must be encapsulated in a script incorporating it in the driver development environment, then feed it with the driver’s source code and report results to the user. Thus, creating a push-button experience for users requires much more than just building a good model-checking engine.

Here, we explore the various components of the SDV tool besides SLAM: driver API rules, environment models, scripts, and user interface, describing how they’ve evolved over the years, starting with the formation of the SDV team in Windows in 2002 and several internal and external releases of SDV.

API rules. Different classes of devices have different requirements, leading to class-specific driver APIs. Thus, networking drivers use the NDIS API, storage drivers use the StorPort and MPIO APIs, and display drivers the WDDM API. A new API called WDF was designed to provide higher-level abstractions for common device drivers. As described earlier, SLIC rules capture API-level interactions, though they are not specific to a particular device driver but to a whole class of drivers that use a common API. Such a specification

We wanted to build
a verifier covering
all possible
behaviors of the
program while
checking the rule,
as opposed to a
testing tool that
checks the rule on a
subset of behaviors
covered by the test.

means the manual effort of writing rules can be amortized by checking the rules on thousands of device drivers using the API. The SDV team has made significant investment in writing API rules and teaching others in Microsoft’s Windows organization to write API rules.

Environment models. SLAM is designed as a generic engine for checking properties of a closed C program. However, a device driver is not a closed program with a main procedure but rather a library with many entry points (registered with and called by the operating system). This problem is standard to both program analysis and model checking.

Before applying SLAM to a driver’s code, we first “close” the driver program with a suitable environment consisting of a top layer called the harness, a main procedure that calls the driver’s entry points, and a bottom layer of stubs for the Windows API functions that can be called by the device driver. Thus, the harness calls into the driver, and the driver calls the stubs.

Most API rules are local to a driver’s entry points, meaning a rule can be checked independently on each entry point. However, some complex rules deal with sequences of entry points. For the rules of the first type, the body of the harness is a nondeterministic switch in which each branch calls a single and different entry point of the driver. For more complex rules, the harness contains a sequence of such nondeterministic switches.

A stub is a simplified implementation of an API function intended to approximate the input-output relation of the API function. Ideally, this relation should be an overapproximation of the API function. In many cases, a driver API function returns a scalar indicating success or failure. In these cases, the API stub usually ends with a nondeterministic switch over possible return values. In many cases, a driver API function allocates a memory object and returns its address, sometimes through an output pointer parameter. In these cases, the harness allocates a small set of such memory objects, and the stub picks up one of them and returns its address.

Scaling rules and models. Initially, we (the SDV team) wrote the API rules in SLIC based on input from driver API