Developing Drivers with the Windows Driver Foundation (Pro Developer)

SDV explores code paths in a device driver by symbolically executing the driver source code. It places a driver in a hostile environment and systematically tests all code paths by seeking violations of usage rules-KMDF or WDM rules, depending on the type of driver. The symbolic execution makes few assumptions about the state of the Windows operating system or the initial state of the driver, so SDV can exercise code in situations that are difficult to assess through traditional testing. To verify a driver, SDV performs the following three-step process:

• Compiles, links, and builds the driver, by using the standard Build utility.

• Scans the driver source code, seeking driver entry points.

  For a KMDF driver, the entry points are the driver's callback functions; for a WDM driver, the entry points are the routines in the driver's dispatch table. SDV assembles the list of entry points into a file called Sdv-map.h that SDV then uses to guide the verification process.

  See "How to Scan Driver Source Code to Create an Sdv-map.h File" later in this chapter for details about Sdv-map.h.

• Prepares for the verification and then verifies that the driver follows the rules that you selected for the current verification.

  See "Under the Hood: How the SDV Verification Engine Works" and "How to Prepare Files and Select Rules for SDV" later in this chapter for details.

  Under the Hood: How the SDV Verification Engine Works

  When you run SDV on your driver, SDV combines the driver source code with its own operating system model to make a kind of "code sandwich":

  • The upper layer is a harness that provides call scenarios into KMDF callback functions or the dispatch routines in WDM drivers.

  • The middle layer is your driver's source code.

  • The lower layer consists of simplified DDI stubs that substitute for actual WDF and WDM DDI functions.

  SDV feeds this combined C code into the SLAM verification engine. SLAM instruments the combined C code with the rules that you selected when you started the verification. SLAM then performs exhaustive verification on the instrumented code.

  Note that SLAM instruments a copy of your driver in the code sandwich; it does not modify your original driver source code.

  For example, consider this hypothetical rule: MyFunctionA cannot be called after MyFunctionB. This rule would be written in the SLIC language as follows:

  state { enum {False, True} WasMyFunctionBCalled = False; } MyFunctionB.entry { WasMyFunctionBCalled = True; } MyFunctionA.entry { if ( WasMyFunctionBCalled ) abort "MyFunctionA is called after MyFunctionB"; }

  Note the pieces of C code between the pairs of curly braces in this rule. When SLAM instruments a driver, it inserts C code from the SDV rule into appropriate places in the driver source code. In this example, WasMyFunctionBCalled is initialized to False. Then SLAM inserts the following assignment at the beginning of MyFunctionB:

  WasMyFunctionBCalled = True;

  SLAM also inserts the following statement at the beginning of MyFunctionA:

  if ( WasMyFunctionBCalled ) SLIC_ABORT ("MyFunctionA is called after MyFunctionB");

  SLAM then performs the verification by iterating through these phases: abstraction, search, validation, and refinement.

  Abstraction

  First, the instrumented combined C code is reduced ("abstracted") to a Boolean abstraction code. The Boolean abstraction code is similar to the original C code in procedure calls and control flow, but differs in its data. It operates with only Boolean variables that represent predicates (that is, Boolean expressions) that were extracted from the original C code.

  Initially, the set of predicates is empty, which implies that the conditions in the conditional statements are nondeterministic: that is, SLAM assumes that each branch of any conditional statement is enabled at any state. Thus, SLAM crudely over-approximates the set of potential behaviors of the driver in a way that is sure to find a path to SLIC_ABORT.

  Search and Validation

  Having a Boolean abstraction-initially a trivial one with only nondeterministic conditions and no assignments at all and later a refined one with assignments to Boolean variables and some of the conditions expressed over Boolean variables-SLAM performs an exhaustive search of SLIC_ABORT on this abstraction. The search is done in the breadth-first manner, through a fixed-point computation of the binary decision diagram (BDD) that represents semantics of the Boolean abstraction.

  On a rough over-approximated abstraction such as the initial one, an error path to SLIC_ABORT might be found easily, unless the original program is trivially correct-for example, the driver doesn't call MyFunctionA at all.

  During the validation phase, SLAM symbolically simulates this error path on the original C code, taking into account the instrumentation it already added to the driver.

  First, consider the case when the driver incorrectly calls MyFunctionB before MyFunctionA (that is, the driver violates the rule). For example, the driver's source has the following code:

  MyFunctionB(…); MyFunctionA(…);

  The path from the entry into the C program to the call to SLIC_ABORT first goes through the initialization WasMyFunctionBCalled = False, then through the assignment WasMyFunctionBCalled =True, which was instrumented at the beginning of the body of MyFunctionB. Finally, the path goes through the "true" branch of the conditional if (WasMyFunctionBCalled), which was instrumented at the beginning of the body of MyFunctionA.

  Apparently, this path is quite possible, so SLAM validates the path and reports it as a defect in the driver. SLAM has accomplished the verification for this case.

  Now, consider the other case, when the driver does not call MyFunctionB before MyFunctionA. For example, suppose this driver is so simple that it only calls MyFunctionA and never calls MyFunctionB. In this case, the path from the entry into the C program to the call of SLIC_ABORT again goes through the initialization WasMyFunctionBCalled = False and then goes through the "true" branch of the conditional if (WasMyFunctionBCalled), which was instrumented at the beginning of MyFunctionA. This path does not contain the assignment WasMyFunctionBCalled =True that was instrumented at the beginning of the body of MyFunctionB because the driver does not call MyFunctionB. Apparently this path is impossible, which SLAM recognizes through the discovery of the following logical contradiction:

  WasMyFunctionBCalled == False && WasMyFunctionBCalled == True

  When SLAM discovers this contradiction, it also discovers a relevant predicate that is involved into this contradiction: WasMyFunctionBCalled. In this case, SLAM continues the verification because the path that is suggested as a defect path on a Boolean abstraction appears to be impossible-or at least infeasible-on the corresponding C code.

  Refinement

  The discovery of a logical contradiction in the initial simulation reveals that WasMyFunctionBCalled is a predicate in the contradiction. SLAM adds newly revealed predicates to the initially empty set of predicates.

  SLAM again reduces the original C code to a Boolean abstraction. This second Boolean abstraction is more refined and subtle than the initial abstraction because it operates on a larger set of predicates.

  With the WasMyFunctionBCalled variable in the set of predicates, the second Boolean abstraction also has all relevant statements that operate on this variable, namely, the {WasMyFunctionBCalled = False;} initialization . Now, the Boolean abstraction appears subtle enough for the search algorithm to fully explore it without discovering any path to SLIC_ABORT. Indeed, the search cannot take the "true" branch of the conditional if (WasMyFunctionBCalled) instrumented in MyFunctionA, because now it takes into account that WasMyFunctionBCalled has the value False. Then the search reports that the Boolean abstraction has no bugs, which implies that the driver's original code correctly follows the rule in this example.

   Info  See the literature on SLAM for a deeper explanation of the verification process-online at http://research.microsoft.com/slam.-Vlad Levin, Static Analysis Tools for Drivers, Microsoft

SDV supplies its own operating system model for the verification. The verification engine exhaustively analyzes the driver code paths and attempts to prove that the driver violated the rules by interacting improperly with the operating system model that SDV supplied.

When SDV proves that the driver violated a rule, it declares a defect and assigns a Fail result to the verification. If SDV cannot prove a violation, it assigns a Pass result to the verification.

The SDV verification engine verifies one rule at a time until it has verified all selected rules. While performing the verification, SDV writes status messages to the command line, along with messages that report errors, as described in "How to View SDV Reports" later in this chapter.

About SDV Rules

SDV rules are written in a language called Specification Language for Interface Checking (of C), or SLIC. When SDV prepares a driver for verification, it uses SLIC language constructs to instrument a driver with additional C statements that describe proper interaction between the driver and the operating system model. Only SDV performs this instrumentation; you cannot do it manually. The results are applied to a copy of the driver's source code; your actual driver is not modified.

An SDV rule can include several elements:

• State variables These elements capture states that are relevant to the verification process on the driver code.

• Entry and exit actions These elements are, respectively, entries into and exits from C procedures of the driver or the SDV operating system model. An action indicates the points in code-in the driver or the operating system model-where the related instrumentation is to be inserted.

• Instrumentation This element consists of conditional statements, assignments to state variables, and abort constructs, which indicate an illegal state that should never be reached in a correct, well-behaving driver.

• Guards These elements are implicit conditions imposed on a pointer argument of an action procedure. The argument is referenced by its position: $1 for first argument, $2 for second, and so on, and $return for the return value. The argument must point to the same object as the object pointed to by the "guardian" pointer variable at a particular "watch-up" point in the driver or in the SDV operating system model.

A guardian can be specified in one of two ways:

For example, the RequestCompleted.slic SDV KMDF rule checks that each request presented to the driver's default I/O queue is completed by the driver-with some exceptions-as specified by the framework. The RequestCompleted.slic rule uses the following construct:

state{ enum {INIT, OK} t = INIT; enum {INIT1, REQPRESENTED} s = INIT1; } with guard (sdv_main, hrequest)

In this example, t and s are state variables that have two possible values and are initialized by the values INIT and INIT1, respectively.

This construct tells SDV that the sdv_main procedure is the single watch-up point for the pointer variable hrequest:

} with guard (sdv_main, hrequest)

where:

• sdv_main is a procedure created by SDV as a wraparound for the driver.

• hrequest is an SDV pointer variable that has as its value a pointer to the WDFREQUEST object.

In the RequestCompleted.slic rule, the following entry actions are present, among others:

fun_WDF_IO_QUEUE_IO_READ.entry[guard $2] {…} sdv_WdfRequestComplete.entry[guard $1] {…}

These actions mean that any call to the driver's EvtIoRead callback or to WdfRequestComplete will be instrumented to check the value of its second or, respectively, first parameter against the value of hrequest that is being watched.

As another example, consider the SDV WDM rule SpinLoc.slic, which checks that every spinlock is acquired and released in alternation. The rule uses the following construct:

watch sdv_KeAcquireSpinLock.exit.$1;

This rule tells SDV that the set of watch-up points includes all calls from the driver to KeAcquireSpinLock. If SDV finds two calls to KeAcquireSpinLock in the driver's source code, SDV dumps the references to these two calls into a file called Slamwatchpoints.txt and runs two separate verification sessions, one for each call.

How SDV Applies Rules to Driver Code

When you run SDV, you select which rules to verify. During verification, SDV examines every execution path in the driver code and tries to prove that the driver violates the selected rules. If SDV fails to prove a violation, it reports a Pass result-that the driver complies with the rules. If the driver has libraries, SDV analyzes every execution path in its entirety, including the path parts that belong to libraries, if the libraries have been processed with SDV before running the verification.

To verify the selected rules, SDV creates a hostile model of the driver's environment in which several worst-case scenarios can happen, such as operating system calls continually failing. SDV systematically tests all possible execution paths in the driver, looking for violations of usage rules that define proper interaction between a driver and the framework, and proper interaction between a driver and the operating system kernel. For example, request-cancellation rules for KMDF drivers specify usage rules for DDI functions that are involved in canceling a request that was presented to the driver's default I/O queue.

Certain SDV rules are preconditions for other rules. That is, if precondition rule A presents a Pass or Fail result, that result determines whether rule B applies for the driver. For example, if the result of the precondition rule FDODriver is Pass, then the FDOPowerPolicyOwnerAPI rule applies for the driver; if the FDODriver result is Fail, then the FDOPowerPolicyOwnerAPI rule does not apply for this driver. Therefore, in the latter case, you should disregard any verification results for this driver that are related to that rule.

Because SDV tests for serious errors in obscure paths that are unlikely to be encountered even in thorough testing, running SDV with all rules can take a long time and use substantial amounts of physical memory, depending on the size of the driver.

To take advantage of SDV rules for KMDF drivers, you should declare callback functions with the corresponding function role types listed in Dispatch_routines.h-and in this chapter-and defined in WDF header files. The function role types are available to your driver when you include Wdf.h.

See "How to Annotate KMDF Driver Source Code for SDV" later in this chapter for more information about how to take advantage of SDV rules in drivers. See also "KMDF Rules for SDV" later in this chapter for details about the specific rules for KMDF drivers.

 Info  See "Thorough Static Analysis of Device Drivers" from the EuroSys 2006 conference for more details-online at http://go.microsoft.com/fwlink/?LinkId=80612.