Static Driver Verifier: a Compile-Time Bug-Finding Tool for WDM Device Drivers

Static Driver Verifier: Finding Bugs in Device Drivers at Compile-Time - 15

Static Driver Verifier: Finding Bugs in Device Drivers at Compile-Time

WinHEC 2004 Version - April 8, 2004

Abstract

This paper provides information about Static Driver Verifier (SDV) for Microsoft® Windows® Driver Model (WDM) device drivers. SDV is a tool that searches for driver bugs at compile time.

This information applies for the following operating systems:
Microsoft Windows 2000
Microsoft Windows XP
Microsoft Windows Server™ 2003
Next client version of Microsoft Windows, codenamed “Longhorn”

Static Driver Verifier has not yet been released for beta review. Information about availability of SDV for review and testing will be published in the Microsoft Hardware Newsletter. Up-to-date information about SDV is published on Windows Hardware and Driver Central, at http://www.microsoft.com/whdc/devtools/sdv.mspx.

Contents

Introduction 3

Rules 3

Environment Model 7

Analysis 8

Results 13

Resources 15

Disclaimer

This is a preliminary document and may be changed substantially prior to final commercial release of the software described herein.

The information contained in this document represents the current view of Microsoft Corporation on the issues discussed as of the date of publication. Because Microsoft must respond to changing market conditions, it should not be interpreted to be a commitment on the part of Microsoft, and Microsoft cannot guarantee the accuracy of any information presented after the date of publication.

This White Paper is for informational purposes only. MICROSOFT MAKES NO WARRANTIES, EXPRESS, IMPLIED OR STATUTORY, AS TO THE INFORMATION IN THIS DOCUMENT.

Complying with all applicable copyright laws is the responsibility of the user. Without limiting the rights under copyright, no part of this document may be reproduced, stored in or introduced into a retrieval system, or transmitted in any form or by any means (electronic, mechanical, photocopying, recording, or otherwise), or for any purpose, without the express written permission of Microsoft Corporation.

Microsoft may have patents, patent applications, trademarks, copyrights, or other intellectual property rights covering subject matter in this document. Except as expressly provided in any written license agreement from Microsoft, the furnishing of this document does not give you any license to these patents, trademarks, copyrights, or other intellectual property.

Unless otherwise noted, the example companies, organizations, products, domain names, e-mail addresses, logos, people, places and events depicted herein are fictitious, and no association with any real company, organization, product, domain name, email address, logo, person, place or event is intended or should be inferred.

© 2004 Microsoft Corporation. All rights reserved.

Microsoft, Windows, and Windows NT are either registered trademarks or trademarks of Microsoft Corporation in the United States and/or other countries.

The names of actual companies and products mentioned herein may be the trademarks of their respective owners.

Introduction

Writing a robust driver based on the Microsoft® Windows® Driver Model (WDM) requires a lot of expertise and a precise understanding of how the driver interacts with the I/O manager. Testing WDM drivers is also tricky. There are two main difficulties that typically limit the testability of WDM device drivers:

·  Observation: It is often difficult to see the moment when something goes wrong in the interaction between the driver and the operating system. Since the WDM application programming interface (API) is large, there are many situations where a driver can violate an implicit rule about API function usage, resulting in a crash or improper behavior at a later time. It would be useful to detect the error at the point where the root cause of the error happens, which is normally hard when drivers are being developed and tested.

·  Control: Drivers that work correctly under normal circumstances can have subtle errors that occur only under exceptional situations, such as when another driver, lower in the stack, fails an I/O request packet (IRP). Such situations are hard to exercise. As a result, traditional testing does not have high coverage in the error paths through the driver code.

Static Driver Verifier (SDV) reduces problems associated with observation and control during testing of WDM device drivers. Observation is improved by stating and checking several rules that check if the driver uses the WDM API properly. For example, SDV has a rule that specifies that under certain circumstances a driver’s dispatch routine should always return whatever value the lower driver in the stack returns. As another example, SDV enforces a rule that spin locks need to be acquired and released in strict alternation.

Control is improved by using the following techniques:

·  SDV provides a very hostile model of the driver’s environment, where several worst-case scenarios (such as operating system calls continually failing) can happen.

·  SDV provides very powerful static analysis (called model checking) that, in addition to providing a hostile environment, systematically explores all possible execution paths in the driver.

In other words, SDV is a unit-testing tool for device drivers. It places a driver in a hostile environment and systematically tests all code paths through the driver by looking for violations of WDM usage rules.

SDV is a compile-time tool. It explores paths by symbolically executing the source code. The symbolic execution makes very few assumptions about the state of the operating system or the initial state of the driver. Thus, it is able to exercise situations that are difficult to exercise by traditional testing. Testing some situations, however, may never be feasible.

Rules

SDV is packaged with a set of rules that define how device drivers should use the WDM API. For example, one rule checks that drivers, when running at raised IRQL, do not wait with a nonzero timeout. Another rule checks that drivers do not detach or delete on IRP_MN_SURPRISE_REMOVAL. All of the currently supported rules are specified in Table 1.

The rules can be logically categorized by the following architecturally related events and functions that they are testing:

·  IRP: rules related to functions that use input/output request packets

·  IRQL: rules related to functions that use interrupt request levels

·  PnP: rules related to Plug and Play functions

·  PM: rules related to power management functions

·  WMI: rules related to functions using Windows Management Instrumentation

·  Sync: synchronization rules related to spin locks, semaphores, timers, mutexes, and other methods of access control

·  Other: rules applying to functions that are not fully described by any of the categories above

Many of the SDV rules are designed to search for multiple potential flaws in a driver. For example, a driver can violate the AddDevice rule in one of three ways:

·  The driver can neglect calling IoCreateDevice.

·  The driver can neglect calling IoAttachDeviceToDeviceStack.

·  The driver can call IoAttachDeviceToDeviceStack before IoCreateDevice.

Table 1: Categorized WDM Rules

Category / Rule Name / Rule Description
IRP / CancelRoutineOnForwardedIrp / Checks that IoSetCompletionRoutine is not called on pending IRPs.
DoubleCompletion / Checks that drivers do not complete an IRP twice.
IrpProcessingComplete / Checks that dispatch routines completely process IRPs.
LowerDriverReturn / Checks that, if a lower driver is called, the dispatch routine returns the same status.
MarkIrpPending / Checks that return STATUS_PENDING and IoMarkIrpPending are correlated.
PendedCompletedRequest / Checks that drivers do not return STATUS_PENDING if IoCompleteRequest has been called.
PrematureSkip / Checks that IoSkipCurrentStackLocation is not called on IRPs being processed.
StartIoCancel / Checks for cancellation races.
StartIoRecursion / Checks for potential recursion in StartIo.
IRQL / Irql / Checks that functions are called only at appropriate IRQL levels.
IrqlReturn / Checks that dispatch routines return at the same IRQL at which they started.
PAGED_CODE / Checks that IRQL<=APC_LEVEL when PAGED_CODE is called.
PnP / AddDevice / Checks that AddDevice calls certain routines or returns failure.
PnpSameDeviceObject / Checks that IoAttachDeviceToDeviceStack is called with an appropriate device object.
Sync / CancelSpinLock / Checks that cancel spin locks are locked and unlocked in strict alternation.
CriticalRegions / Checks that KeEnterCriticalRegion and KeLeaveCriticalRegion are used in strict alternation.
ExclusiveResourceAccess / Checks that ExAcquireResourceExclusiveLite and ExReleaseResourceLite (or ExReleaseResourceForThreadLite) are used in strict alternation.
ExclusiveResourceAccessTry / Checks that ExTryToAcquireResourceExclusiveLite and ExReleaseResourceLite (or ExReleaseResourceForThreadLite) are used in strict alternation.
FastMutexes / Checks that ExAcquireFastMutex (or ExTryToAcquireFastMutex) and ExReleaseFastMutex are used in strict alternation.
InterruptSpinLock / Checks that KeAcquireInterruptSpinLock and KeReleaseInterruptSpinLock are used in strict alternation.
IoInitializeTimer / Checks that IoInitializeTimer is called only once.
KeWaitDeadlock / Checks that calls to KeWaitForSingleObject are waiting on KeSetEvent.
QueuedSpinLock / Checks that KeAcquireInStackQueuedSpinLock and KeReleaseInStackQueuedSpinLock are used in strict alternation.
QueuedSpinLockFromDpc / Checks that KeAcquireInStackQueuedSpinLockAtDpcLevel and KeReleaseInStackQueuedSpinLockFromDpcLevel are used in strict alternation.
SharedResourceAccess / Checks that ExAcquireResourceSharedLite and ExReleaseResourceLite (or ExReleaseResourceForThreadLite) are used in strict alternation.
SharedResourceAccessStarveExclusive / Checks that ExAcquireSharedStarveExclusive and ExReleaseResourceLite (or ExReleaseResourceForThreadLite) are used in strict alternation.
SharedResourceAccessWaitExclusive / Checks that ExAcquireSharedWaitForExclusive and ExReleaseResourceLite (or ExReleaseResourceForThreadLite) are used in strict alternation.
SpinLock / Checks that KeAcquireSpinLock (or KeAcquireSpinLockRaiseToDpc) and KeReleaseSpinlock are used in strict alternation.
SpinLockAtDpc / Checks that KeAcquireSpinLockAtDpcLevel and KeReleaseSpinLockFromDpcLevel are used in strict alternation.
SpinlockSafe / Checks for specific deadlock cases with spin locks.
Other / DanglingDeviceObjectReference / Checks that the driver calls ObDereferenceObject after calling IoGetAttachedDeviceReference.
DebugBreakUsage / Checks that drivers do not contain calls to DbgBreak functions in release code.
NullExFreePool / Checks that ExFreePool is not called with a NULL argument.
SafeStrings / Checks that drivers use the appropriate safe string routine replacements for drivers defined.
WorkItems / Checks that Io*WorkItem functions are used correctly.
ZwFileCreate / Checks that ZwCreateFile is used correctly and is followed by ZwClose once it is no longer in use.
ZwFileOpen / Checks that ZwOpenFile is used correctly and is followed by ZwClose once it is no longer in use.
ZwRegistryCreate / Checks that ZwCreateKey is used correctly and is followed by ZwClose or ZwDeleteKey once it is no longer in use.
ZwRegistryOpen / Checks that ZwOpenKey is used correctly and is followed by ZwClose or ZwDeleteKey once it is no longer in use.

WDM Rules Belonging to More Than One Category

Category / Rule Name / Rule Description
IRP,IRQL / ForwardedAtBadIrql / Checks for IRPs that are forwarded at the wrong IRQL.
IRP, PnP / PnpIrpCompletion / Checks that Plug and Play IRPs are passed on to the lower driver.
PnPSurpriseRemove / Ensures that drivers are not detached or deleted on IRP_MN_SURPRISE_REMOVAL.
TargetRelationNeedsRef / Checks that the dispatch routine calls ObReferenceObject on pointers returned on a TargetRelation Plug and Play IRP.
IRP, Sync / MarkingInterlockedQueuedIRPs / Checks that drivers mark the IRP as pending while queuing it in an interlocked fashion.
MarkingQueuedIRPs / Checks that drivers mark the IRP as pending while queuing it.
IRP, PM / RequestedPowerIrp / Checks that drivers always specify NULL as the last argument of PoRequestPowerIrp.
IRP, WMI / WmiComplete / Checks that dispatch routines do not return without completing a Windows Management Instrumentation IRP.
WmiForward / Checks that dispatch routines do not return without forwarding Windows Management Instrumentation IRPs with disposition IrpForward.
IRP, Other / NullDevobjForwarded / Checks that drivers do not call IoCallDriver on a NULL device object pointer.

Environment Model

Static Driver Verifier is a unit testing tool, which analyzes each WDM device driver individually. When analyzing a driver, SDV provides a model for the environment of the driver, which includes the operating system and other drivers in the driver stack. The environment model both drives the device driver through its dispatch routines and provides the semantics for the functions that the driver calls.

The SDV environment model is quite hostile. For example, in the Microsoft® Windows® operating system, a driver may work in practice when it does not check for NT_SUCCESS on a return value of a function call such as IoAllocateDriverObjectExtension. The SDV model of IoAllocateDriverObjectExtension, however, encodes the possibility that the function will return a failure status, and the analysis considers the failure possibility at every call and determines if the driver handles this possibility correctly.

SDV uses symbolic simulation. This means that SDV might not have the value of a given variable. In some cases, SDV will have only a few facts about a variable. For example, in the call to IoCallDriver in the following example, SDV might know only that ptr is not equal to NULL:

if (ptr != NULL) {
IoCallDriver(po,pirp);
}

As you can imagine, it is difficult for SDV to model all possible interactions between the device driver and its surrounding environment. SDV instead models two general scenarios, each of which is defined in a harness.

The simple harness simulates the effect of one of the following possible events:

·  Calling any of the driver’s dispatch routines on some IRP.

·  Calling the driver’s StartIo routine.

·  Running a deferred procedure call (DPC).

·  Running an interrupt service routine (ISR).

The routines are given a completely unknown IRP and an unknown initial state. In other words, SDV is effectively asking:

·  Does the rule hold for the dispatch routine if it is called from an unknown state on a device object and an IRP that we know nothing about?

·  Does the rule hold for any ISRs if they are called from an unknown state?

·  Does the rule hold for any DPCs if they are called from an unknown state?

·  Does the rule hold for any the driver's StartIo routine?

If a driver passes a rule using this harness, the result is quite strong; it holds for any dispatch routine, regardless of the state of the system before or after the execution.

For some rules, the correctness of a driver will depend on an event occurring in DriverEntry, AddDevice, or even the Plug and Play dispatch routine on an IRP_MN_START_DEVICE IRP. In these cases, SDV uses a Plug and Play harness, which calls the following functions, in order:

·  The driver’s DriverEntry routine

·  The driver’s AddDevice routine

·  The Plug and Play dispatch routine with an IRP_MN_START_DEVICE IRP

·  Any dispatch routine with an unknown IRP, DPC, ISR, or the driver’s StartIo function

·  The Plug and Play dispatch routine with an IRP_MN_REMOVE_DEVICE IRP

·  The driver's Unload routine

Analysis

As shown in Figure 1, Static Driver Verifier takes the driver code as input and analyzes it by looking for violations of a set of WDM usage rules. For each rule, the tool can determine whether the driver passes the rule or violates it[1]. Violations are presented as source-level error paths through the driver code.