Static Driver Verifier Research Platform

Introduction	2

Target Audience	2

Requirements	2

Prerequisites	2

Alpha Release	2

Feedback	2

Model of Operation	3

Platform Model	3

Module	4

Rules	4

Plugins	4

The Custom Plugin	5

Platform Implementation %SDV%\samples\frameworks\custom	6

Sample driver %SDV%\samples\fail_drivers\custom\fail_driver1	8

Platform Model %SDV%\osmodel\custom	9

Platform Rules %SDV%\rules\custom	13

Platform Meta Data %SDV%\data\custom	14

SDVRP Customization	15

Folders to Customize	15

Customization	15

Refine Custom Plugin	15

Walk Through: fail_driver1	15

Limitations and Known Issues	20

Introduction

Static Driver Verifier (SDV) is a compile-time static verification tool, included in the Windows Driver Kit (WDK). SDV is delivered with support for three driver platforms: 1) WDM (The Windows Driver Model), 2) KMDF (Kernel Mode Driver Framework) and NDIS (Network Driver Interface Specification). For each of these platforms, SDV provides a number of platform specific components (for example platform specific rules and a platform model). Rules are expressed in the SLIC language and describe the proper way to use the APIs of the platform. A platform model is a collection of C procedures that represent the environment the driver operates in.

The SDV Research Platform (SDVRP) is an extension to SDV that allows you to adapt SDV to support additional platforms and write custom SLIC rules for this platform.

The platforms you would adapt SDV to verify would typically be driver platforms, but can technically be any piece of reactive code (a ‘module’) that is embedded inside an application or an OS. With some work, you can use SDV to verify that clients of an API or protocol adhere to the protocol/API specification. The key requirement is that your module can be composed with its environment in a manner that it fits with model presented in the following sections.

Target Audience

Academic access to experiment with the SLAM verification engine and introduce students to the process of writing rules for SDV.

Driver specialists that want to experiment with applying SDV to a new driver platform or experiment with additional rules for current driver platform.

Requirements

The SDVRP requires that the (freely available) Windows Driver Kit Version 7.1.0 (WDK) first be installed. See http://www.microsoft.com/whdc/driver/wdk/ for information about obtaining the WDK. (As of this writing under: How to Get the WDK -> Microsoft Download Center).

Prerequisites

To be able to use the SDVRP and to be able to understand the rest of this document a reasonable understanding of SDV is required. The Windows Driver Kit's SDV documentation provides the necessary information (see http://msdn.microsoft.com/en-us/library/ff552808.aspx). At the very least you should have an understanding of "Static Driver Verifier Concepts" (http://msdn.microsoft.com/en-us/library/ff552813.aspx) and understand the example "Verifying Fail_Driver1" (http://msdn2.microsoft.com/en-us/library/aa906583.aspx).

Alpha Release

This release of the SDVRP is an alpha release. As such, please expect and bear with problems, and be sure to provide feedback to us.

Feedback

Please provide feedback to sdvrpdis@microsoft.com .

Model of Operation

SDV verifies that a Module interacts correctly with a Platform. Platform is essentially a set of APIs, or a library. WDM Driver Model APIs is an example of such a library.

SDV consists of three major components:

Platform Model: The Platform Model is an abstraction of the Platform. Where the Platform might be millions of lines of code, the Platform Model is engineered to abstract only the bits relevant for verification.

Rules: The rules specify legal interactions on the edges between Platform Model and Module.

Verification Engine: The verification engine brings Platform Model, Module and Rules together. It verifies that the Module in context of the Platform Model adheres to the rules.

The following picture illustrates the interaction between a Module and the components of a Platform Model:

Platform Model Module DriverRead DriverWrite CustomAcquireLock CustomReleaseLock Platform API Models Platform Manager Model Platform Model Infrastructure

Platform Model

The Platform Model is an abstraction of the Platform.

The syntax is regular C syntax. The semantics is as the C syntax with a few changes, primarily to control verification flow and allow for introduction of non-determinism.

The Platform Model includes three components:

A Platform Manager Model responsible for exercising the module by calling the module’s entry points. We can think of this component as the entry point (main routine) of the system. For WDM drivers this is the Windows IO Manager.

A set of Platform API Models that the module can use in order to complete requests from the Platform Manager. The APIs typically contain functionality to access the underlying hardware. In Windows this is the Windows Device Driver Interfaces (DDIs), consisting of hardware abstraction layer, APIs for controlling execution (locks, queues, etc) and APIs for accessing resources such as memory.

A Platform Model Infrastructure containing shared header files, common functions and states for the Platform Manager Model and the Platform API Models.

Module

The module exposes a set of entry points that the platform may call with requests. When the module receives a request it may call its own code and APIs to complete the received request. In case of SDV – as deployed in the Windows Driver Kit – the modules are the drivers subject to verification.

Rules

The rules specify legal interactions on the edges between Platform Model and Module. On the picture above you can see four interactions: two calls from the Platform Manager Model to the Module and two calls from the Module to the API Models.)

The rule specification language of SDV is called SLIC. This document explains how the rules fit into the bigger picture: where you put them and how they fundamentally interact with the module and the platform model. The document SLIC.docx provides a more detailed description of SLIC, including syntax and semantics. Also, look at the various included driver platform rules (WDM, KMDF, NDIS) for inspiration.

Plugins

(Notice, in the following section and for the remainder of the document: All file references are relative to %SDV%. Also notice, in code sections: Three dots (...) indicate code left out)

The implementation of SDV and SDVRP organizes files pertaining to a specific platform in a ‘plugin’. To use SDVRP for a user's platform, the plugin for that platform need to be created.

A plugin ‘myplugin’ consists of:

%SDV%\data \myplugin: Meta-data pertaining to the plugin (SDV configuration files)

%SDV%\rules\myplugin: A set of rules

%SDV%\osmodel\myplugin: A platform model

SDV and SDVRP ships with existing plugins:

wdm

kmdf

ndis

Additionally the SDVRP has a minimal plugin (named ‘custom’) that serves as an example, or a template, of a new plugin.

With the SDVRP you can:

Create a new plugin from scratch;

Clone an existing plugin or

Refine any existing plugin as you see fit.

The Custom Plugin

The SDVRP includes a minimal, but complete, example of an artificial driver model called the ‘Custom Platform’. The components of the Custom Platform are:

Platform Implementation %SDV%\samples\frameworks\custom: We provide an implementation of the Custom Platform.

Sample Driver %SDV%\samples\fail_drivers\custom\fail_driver1: We provide a sample Custom Platform driver.

The SDVRP also provides the SDV-specific parts for the Custom Platform – the plugin:

Meta Data %SDV%\data\custom: configuration meta-data: the file msft.sdv containing the list of rules in the plugin (in this case, a single rule name), and the file sdv-default.xml with SDV parameters (timeout, spaceout, etc.).

Platform Rules %SDV%\rules\custom: The Custom Platform comes with a single SLIC rule.

Platform Model %SDV%\osmodel\custom: The Custom Platform provides Platform Manager Model, Platform API Models and Model Infrastructure.

Notice: The Platform Implementation and the Sample Driver are provided in order to show an example of a library (the Platform) and the code that uses the library (the Sample Driver). Together, they represent a subject for verification by SDV. In other words, they are provided so that we have a ‘nail’. The Custom Plugin combined with the SDV verification engine provides the ‘hammer’ for this ‘nail’.

Platform Implementation %SDV%\samples\frameworks\custom

The platform implementation consists of the custom.h and custom.c files, and the build files (sources and makefile). After the build, the output of this folder is the header file custom.h and a compiled and linked library custom.lib.

custom.h

The cornerstone of the Custom Platform is the header file custom.h. It declares all functions and types available to custom drivers. This header file represents the APIs that the driver uses to complete requests.

/*++ … Abstract: Header file for the SDV Custom Framework Drivers compiling with this custom.h header file can be compiled and linked to .sys files, however those .sys files are not functional and should never be loaded into the kernel. The custom driver model consist of: * Type CUSTOM_IRP representing a Custom IO Request Packet. * Type CUSTOM_LOCK representing a Custom Lock. * Type CUSTOM_STATUS used for returning status code from DDIs and entry points. * Driver entry point role type declarations: CUSTOM_READ and CUSTOM_WRITE. * DDIs of the Custom Framework: CustomAcquireLock, CustomReleaseLock and CustomMemMove. * Miscellaneous: The UNREFERENCED_PARAMETER macro Environment: Static Analysis using SDV only. Not to be used in real drivers. --*/ /* Type CUSTOM_IRP representing a Custom IO Request Packet: */ typedef struct { char buffer[512]; } CUSTOM_IRP; typedef CUSTOM_IRP *PCUSTOM_IRP; /* Type CUSTOM_LOCK representing a Custom Lock: */ typedef struct { int lock; } CUSTOM_LOCK; typedef CUSTOM_LOCK *PCUSTOM_LOCK; /* Type CUSTOM_STATUS used for returning status code from DDIs and entry points: */ typedef int CUSTOM_STATUS; #define CUSTOM_STATUS_SUCCESS 0 #define CUSTOM_STATUS_UNSUCCESSFUL 1 /* Driver entry point role type declarations: CUSTOM_READ and CUSTOM_WRITE: */ typedef CUSTOM_STATUS CUSTOM_READ( PCUSTOM_IRP Irp ); typedef CUSTOM_STATUS CUSTOM_WRITE( PCUSTOM_IRP Irp ); /* DDIs: CustomAcquireLock, CustomReleaseLock and CustomMemMove: */ void CustomAcquireLock( PCUSTOM_LOCK Lock ); void CustomReleaseLock( PCUSTOM_LOCK Lock ); CUSTOM_STATUS CustomMemMove( char *dst, char *src, int bytes ); …

A note regarding Role Type Declarations: A role type is a function typedef that defines driver's entry points for the Framework in the platform header file.

To inform SDV about the module's entry points, modules must declare driver entry points using role type declarations (see our example further down: %SDV%\samples\fail_drivers\custom\fail_driver1\fail_driver1.h). Also, the role type declarations should be present in the SDV-specific file dispatch_routines.h (see our example further down: %SDV%\osmodel\custom\dispatch_routines.h).

custom.c

The custom.c file contains the "implementation" of the APIs declared in custom.h. Those implementations do not provide a real functionality, but are only present to satisfy the linker so that we can produce custom.lib. For example, the CustomMemMove function, as implemented in custom.c, always returns CUSTOM_STATUS_SUCCESS. In a real plugin, this should be replaced with the actual implementation of the APIs. Also, to make the build work, we are piggybacking our Custom Platform on top of the WDM platform and also provide the WDM required function DriverEntry. One important detail: Neither custom.h, nor custom drivers will include wdm.h. Hence, the Custom Platform is a perfectly opaque encapsulation of wdm.h.

Sample driver %SDV%\samples\fail_drivers\custom\fail_driver1

We provide a sample driver that uses the Custom Platform. Notice: the driver won't do anything useful and should never be loaded into a real operating system.

The sample driver consists of the fail_driver1.h, fail_driver1.c and build files (sources and makefile). After the build, the output of this folder is the compiled and linked driver fail_driver1.sys.

fail_driver1.h

The fail_driver1.h file includes the Custom Framework header custom.h and declares the driver's entry points:

... #include <custom.h> CUSTOM_READ DriverRead; CUSTOM_WRITE DriverWrite;

The driver's entry points are declared using the provided role types. This is an important detail. As we will see later, SDV uses this information to determine that (for example) DriverRead is a CUSTOM_READ entry point and hence should follow a certain set of rules.

fail_driver1.c

The implementation of the driver provides functionality to read and write a block of data to/from a global data structure.

... #include "fail_driver1.h" /* Global data for the driver: */ struct DriverData { CUSTOM_LOCK Lock; int reads; int writes; char buffer[512]; } DriverData; CUSTOM_STATUS DriverRead( PCUSTOM_IRP Irp ) { CUSTOM_STATUS status; CustomAcquireLock(&(DriverData.Lock)); /* Left out: Somehow magically read DriverData.buffer from disk. */ status=CustomMemMove(Irp->buffer, DriverData.buffer, 512); if (status==CUSTOM_STATUS_UNSUCCESSFUL) { return CUSTOM_STATUS_UNSUCCESSFUL; } DriverData.reads++; CustomReleaseLock(&(DriverData.Lock)); return CUSTOM_STATUS_SUCCESS; } ...

You can probably point out a few flaws in this implementation, but in this document we will only focus on the handling of locks. We have not really defined the rules for the proper use of locks yet, but take a minute to look at the implementation. Do you see anything that is a concern for you regarding the driver's use of locks?

Platform Model %SDV%\osmodel\custom

The custom platform model provides I/O Manager Model, DDI Models and Model Infrastructure and includes the following files: dispatch_routines.h, harness-defs.h, sdv_cl_frontend.h and osmodel.c.

dispatch_routines.h

This file declares the platform's entry points:

... #ifdef fun_CUSTOM_READ extern CUSTOM_READ fun_CUSTOM_READ; #endif #ifdef fun_CUSTOM_WRITE extern CUSTOM_WRITE fun_CUSTOM_WRITE; #endif

This is compiled as a C header file, but is additionally and separately parsed by the verification engine. The verification engine looks for the pattern

^extern role_type abstract_name;$

The role_type must match a role type declaration in the platform header file custom.h, and the abstract_name must match the function identifier called by the osmodel.c file (see below).

harness-defs.h

This file declares the set of possible variations of the platform model. Each rule will be designed with one such variation in mind. The Custom Platform model provides two platform model variations: SDV_HARNESS_A and SDV_HARNESS_B:

... #define SDV_HARNESS_A 1 #define SDV_HARNESS_B 2

sdv_cl_frontend.h

This file is present, but empty. It is only present for historic reasons. We will remove this file in a later release.

osmodel.c

This file contains the core of the Platform Model. It has five sections:

... /* osmodel-headers.c begin */ ... /* osmodel-control.c begin */ ... /* osmodel-state.c begin */ ... /* osmodel-iomanager.c begin */ ... /* osmodel-ddis.c begin */ ...

Platform Model Headers

This section sets up environment for interpreting the Custom Platform:

Include platform-specific header files: custom.h

Include driver-specific entry point declarations: sdv-map.h

Include platform-specific SDV role types declarations: dispatch_routines.h

Platform Model Control

The Platform Model Control section provides SDV-specific common functions used to control non-determinism and program execution:

malloc: Provides initialization of pointer values with fresh and unique addresses.

SdvMakeChoice: Non-deterministic initialization of non-pointer values.

SdvExit: Acts like exit() within the context of model checking.

SdvAssume/SdvAssumeSoft: Acts like an ASSERT, but halts analysis if the assert fails.

sdv_DoNothing: As the name says: Does nothing.

For details look at the osmodel.c file, also see the following sections for a discussion of the magic of SdvMakeChoice. These functions are not platform-specific.

Platform Model State

The Platform Model State defines variables used in the platform manager implementation. For our custom platform model, we need two variables to model the request to the driver from the IO Manager:

sdv_custom_irp

sdv_pcustom_irp

In particular, the variable sdv_pcustom_irp is used as a parameter in the calls to the driver's entry points CUSTOM_READ and CUSTOM_WRITE, see section osmodel-iomanager.c in osmodel.c.

Platform Manager Model

The Platform Manager Model is basically a test harness that exercises entry points defined in the driver. It includes the function main, calling the function sdv_main that sets up the environment and calls into the driver:

/** sdv_stubs_custom_...: Provide function stubs called at various stages by the IO manager model. The functions do not provide functionality, rather they can be used in SDV rules as hooks for instrumentation: */ void sdv_stub_custom_main_begin() { } void sdv_stub_custom_main_end() { } void sdv_stub_custom_read_begin() { } void sdv_stub_custom_read_end() { } void sdv_stub_custom_write_begin() { } void sdv_stub_custom_write_end() { } /** sdv_main: Provide IO Manager model with fixed name sdv_main: */ int sdv_main() { CUSTOM_STATUS status; int choice = SdvMakeChoice(); sdv_stub_custom_main_begin(); switch (choice) { case 0: #ifdef fun_CUSTOM_READ sdv_stub_custom_read_begin(); status=fun_CUSTOM_READ(sdv_pcustom_irp); sdv_stub_custom_read_end(); #else status=sdv_DoNothing(); #endif break; case 1: #ifdef fun_CUSTOM_WRITE sdv_stub_custom_write_begin(); status=fun_CUSTOM_WRITE(sdv_pcustom_irp); sdv_stub_custom_read_end(); #else status=sdv_DoNothing(); #endif break; default: status=sdv_DoNothing(); break; } sdv_stub_custom_main_end(); } /** main: Provide entry point for the analysis: */ void __cdecl main() { sdv_main(); }

A note regarding non-determinism: The sdv_main function is similar to a test case in the sense that it is responsible for setting up environment and calling into the component being tested. However, where you would have maybe thousands of test cases, there is only one sdv_main function. sdv_main exercises multiple testing scenarios by using non-determinism (SdvMakeChoice()). Any time you see initialization of variables using the SdvMakeChoice function, the verification engine will non-deterministically choose a value.

The empty stub functions only serve as 'labels' during verification. Later, when we look at the sample rule, we will see how these stubs are used.

Platform API Models

The API (or DDI, in the driver model terminology) models must abstract the functionality of the real custom library by focusing only on the aspects relevant for the verification. In other words, the API models are dependent on the particular set of the rules. When new rules are added to a plugin, the API models have to be reviewed and updated with more details, if needed.

Here is the model for a single API CustomMemMove:

... CUSTOM_STATUS CustomMemMove( char *dst, char *src, int bytes ) { int choice = SdvMakeChoice(); UNREFERENCED_PARAMETER(dst); UNREFERENCED_PARAMETER(src); UNREFERENCED_PARAMETER(bytes); switch (choice) { case 0: return CUSTOM_STATUS_SUCCESS; default: return CUSTOM_STATUS_UNSUCCESSFUL; }; } ...

A note regarding non-determinism: notice the use of SdvMakeChoice. This time the nondeterministic choice is used to ensure that the driver is tested for all possible return values that CustomMemMove may return.

Note: Recall that the CustomMemMove "implementation" provided in custom.c always returns CUSTOM_STATUS_SUCCESS. However, in osmodel.c, we model a realistic implementation of the function.

Platform Rules %SDV%\rules\custom

The Custom Platform comes with a single rule CustomLock. The rule consists of a CustomLock.slic file (the rule) and a CustomLock.h file (the header file).

CustomLock.slic

This rule specifies proper locking behavior for Custom drivers. It specifies that calls to CustomAcquireLock and CustomReleaseLock must be used in strict alternation. Moreover, at the return from an entry point, the driver should not be holding the lock:

... state{ enum {unlocked, locked} s = unlocked; } watch CustomAcquireLock.exit.$1; CustomAcquireLock.exit[guard $1] { if(s==locked) { abort "The driver is calling $fname after already acquiring the lock."; } else { s=locked; } } CustomReleaseLock.exit[guard $1] { if(s==unlocked) { abort "The driver is calling $fname without first acquiring the lock."; } else { s=unlocked; } } sdv_stub_custom_main_end.entry { if(s==locked) { abort "The driver has returned from an entry point without releasing the lock."; } }

Notice that the functions used as the events names (CustomAcquireLock, CustomReleaseLock, sdv_stub_custom_main_end) are all implemented in the Platform Model, either as the DDI models or as stub functions.

Given the rule CustomLock, look at the fail_driver1.c. Can you see the bug in the driver that this rule will find?

CustomLock.h

The rule header file contains a reference to the harness that SDV should invoke in order to check the rule. Recall that the harnesses are declared in the harness-defs.h file. The CustomLock.h file is as follows:

#define SDV_HARNESS SDV_HARNESS_A

Platform Meta Data %SDV%\data\custom

The meta-data to configure SDV for the Custom Platform is:

msft.sdv: List of rules. For the Custom plugin, it contains the single line "CustomLock.slic"

sdv-default.xml: Settings for SDV parameters. See the SDV user manual for details.

SDVRP Customization

Folders to Customize

The following are the folders that SDV will consume at runtime:

%SDV%\data\%SDV_MODEL%: Platform Meta Data for the %SDV_MODEL% platform.

%SDV%\rules\%SDV_MODEL%\: Platform Rules for the %SDV_MODEL% platform.

%SDV%\osmodel\%SDV_MODEL%: Platform Model for the %SDV_MODEL% platform.

The %SDV% variable is set during installation of the SDVRP and you should not change this variable. The %SDV_MODEL% variable must be set by you with a “set SDV_MODEL=…” command.

Notice: SDV does not reference any of the files or folders in the %SDV%\samples\%SDV_MODEL% folder (unless you invoke SDV in this folder).

Customization

With the SDVRP you can:

Create a new plugin from scratch. You do this by setting the SDV_MODEL variable (for example to “myplugin”) and then ensure that relevant files are in place (for example %SDV%\{data, rules, osmodel}\myplugin.

Clone an existing plugin. For example, you copy the %SDV%\{data,rules, osmodel}\custom folders to new folders (for example %SDV%\{data, rules,osmodel}\myplugin) and then set SDV_MODEL to myplugin.

Refine any existing plugin as you see fit.

Refine Custom Plugin

If you want to refine the Custom Plugin you proceed as explained above. Furthermore you may also want to update the Custom Platform implementation and sample driver. Check that you can build (build –cz) the refined platform implementation and driver prior to invoking SDV.

Walk Through: fail_driver1

A script is provided that demonstrate how all components tie together: custom_build.cmd.

Steps:

Open a “Windows Win7 x86 Free Build Environment" window (from All Programs -> Windows Driver Kits -> 7600.16385.1 -> Build Environments -> Windows 7 -> x86 Free Build Environment)

rd /s /q %BASEDIR%\sdv_samples 2>NUL

robocopy /e "%SDV%\samples" %BASEDIR%\sdv_samples

cd %BASEDIR%\sdv_samples

.\custom_build.cmd

The .\minmal_build.cmd demonstrates:

How to build the Custom Platform library

How to build a driver that use the Custom Platform library

How to run SDV on said driver

How to spawn the SDV Defect Viewer

The content of the script is as follows:

@echo off REM REM custom_build.cmd REM REM This script demonstrates: REM * How to build the custom framework library REM * How to build a driver that use the custom framework REM * How to run SDV on said driver REM * How to spawn the SDV Defect Viewer REM REM Usage: REM * rd /s /q %BASEDIR%\sdv_samples 2>NUL REM * xcopy /e /i "%SDV%\samples" %BASEDIR%\sdv_samples REM * cd %BASEDIR%\sdv_samples REM * .\custom_build.cmd REM REM Cleanup call .\custom_clean.cmd REM Build the framework 'frameworks\custom': SETLOCAL cd frameworks\custom build -cz ENDLOCAL REM Build the sample driver 'fail_drivers\custom\fail_driver1'. REM Run SDV on the driver revealing the one injected defect. REM Spawn SDV Defect Viewer. REM REM As this driver use the 'custom' framework header file which is not REM in standard include location, update INCLUDE variable appropriately. REM REM As this driver is a 'custom' driver, set the SDV_MODEL variable to REM indicate what framework SDV should analyse drivers against. REM SETLOCAL cd fail_drivers\custom\fail_driver1 set INCLUDE=%INCLUDE%;%BASEDIR%\sdv_samples\frameworks\custom set SDV_MODEL=custom build -cz staticdv /rule:* staticdv /view ENDLOCAL

The output from the script is:

--------------------------------------------------------------------- Microsoft (R) Windows (R) Static Driver Verifier Version 2.0.0.0 Copyright (C) Microsoft Corporation. All rights reserved. --------------------------------------------------------------------- BUILD: Compile and Link for x86 BUILD: Start time: Fri Jun 11 14:09:43 2010 BUILD: Examining j:\sd\slam\7\wdk\sdv_samples\frameworks\custom directory for files to compile. j:\sd\slam\7\wdk\sdv_samples\frameworks\custom BUILD: Compiling j:\sd\slam\7\wdk\sdv_samples\frameworks\custom directory Compiling - custom.c Building Library - objfre_win7_x86\i386\custom.lib BUILD: Finish time: Fri Jun 11 14:09:43 2010 BUILD: Done 3 files compiled 1 library built BUILD: Compile and Link for x86 BUILD: Start time: Fri Jun 11 14:09:43 2010 BUILD: Examining j:\sd\slam\7\wdk\sdv_samples\fail_drivers\custom\fail_driver1 directory for files to compile. j:\sd\slam\7\wdk\sdv_samples\fail_drivers\custom\fail_driver1 BUILD: Compiling and Linking j:\sd\slam\7\wdk\sdv_samples\fail_drivers\custom\fail_driver1 directory Compiling - fail_driver1.c Linking Executable - objfre_win7_x86\i386\fail_driver1.sys BUILD: Finish time: Fri Jun 11 14:09:43 2010 BUILD: Done 3 files compiled 1 executable built --------------------------------------------------------------------- Microsoft (R) Windows (R) Static Driver Verifier Version 2.0.0.0 Copyright (C) Microsoft Corporation. All rights reserved. --------------------------------------------------------------------- BUILD: Compile and Link for x86 BUILD: Start time: Fri Jun 11 14:09:44 2010 BUILD: Examining j:\sd\slam\7\wdk\sdv_samples\fail_drivers\custom\fail_driver1 directory for files to compile. j:\sd\slam\7\wdk\sdv_samples\fail_drivers\custom\fail_driver1 BUILD: Compiling and Linking j:\sd\slam\7\wdk\sdv_samples\fail_drivers\custom\fail_driver1 directory Compiling - fail_driver1.c Linking Executable - objfre_win7_x86\i386\fail_driver1.sys BUILD: Finish time: Fri Jun 11 14:09:44 2010 BUILD: Done 3 files compiled 1 executable built Build 'fail_driver1' ...Done Scan 'fail_driver1' ...Done Compile 'fail_driver1' for [sdv_harness_a] ...Done Link 'fail_driver1' ...Done Check 'fail_driver1' for 'customlock' ...Running Check 'fail_driver1' for 'customlock' ...Done SDV performed 1 check(s) with: 2 Defect(s) Run this command to view the results: StaticDV /view Start Time :6/11/2010 2:09:45 PM and End Time :6/11/2010 2:09:48 PM --------------------------------------------------------------------- Microsoft (R) Windows (R) Static Driver Verifier Version 2.0.0.0 Copyright (C) Microsoft Corporation. All rights reserved. ---------------------------------------------------------------------

Additionally the SDV Defect Viewer is started. It reports two (similar) defects detected for the CustomLock rule, one in the DriverRead function, another in the DriverWrite function. The defect viewer shows you the exact trace in fail_driver1 that violates the CustomLock rule; for example, for the defect in the DriverRead function:

Limitations and Known Issues

This SDVRP has the following Limitations:

No support for libraries: The mainstream SDV supports that a driver is linked together with a number of supporting libraries. This is handled with the staticdv /lib command. The SDVRP does not support libraries. (Most likely it will work; we simply have not tested nor thought this scenario through.) Warning: Never run staticdv /lib on your platform library.

No support for annotations of role types: The mainstream SDV supports that role types are specialized using annotations. For example, the WDM platforms DRIVER_DISPATCH functions use this heavily. This is not supported for custom platforms. (It should work fine for custom platforms also; we simply have not documented this.)

Only one header file per platform supported: The mainstream SDV supports that a platform may use multiple header files. The SDVRP only supports one header file.

Only function declarations allowed in header files: The mainstream SDV use a complex schema to support that platforms provide functions in header file in a mixed form of 1) function declarations, 2) inline function definitions and 3) function style macros. The SDVRP only supports function declarations in the platform header file.

Only Windows 7.1.0 Driver Kit's " Windows 7 x86 Free Build Environment" build environment is supported. (The mainstream version of SDV supports a number of DDKs/WDKs, a number of build environments, and also the Microsoft internal Razzle build environment.)

No macro expansion of rules: Rules are not macro-expanded in the SDVRP version of SDV. (In mainstream SDV rules are macro expanded and then compiled.)

staticdv /showrules not supported for custom platforms.

No detailed documentation of the SLIC language. As a workaround look at the provided WDM or KMDF rules.

This SDVRP has the following Known Issues:

sdv_cl_frontend.h: Currently the platforms must have an empty file named sdv_cl_frontend.h. See %SDV%\osmodel\custom\sdv_cl_frontend.h for an example.

sdv_main: Currently the platform model must have a main function that simply calls a function that must be named sdv_main. See %SDV%\osmodel\custom\osmodel.c for an example.

INCLUDES: staticdv does not pickup INCLUDES settings from the sources files. Because of this you need to set the INCLUDE variable to point to your platform. See the %SDV%\samples\custom_build.cmd for an example.

SDV_MODEL: Currently you must set SDV_MODEL variable to the name of the platform you wish to use. For example: set SDV_MODEL=custom. See also the %SDV%\samples\custom_build.cmd for an example.

At a future release we may additionally incorporate the following changes:

We will change references from %SDV% to %SDV%\plugins (Search for all occurrences of %SDV% )

We will change folder structure to:

myplugin\data: Meta data pertaining to the plugin (configuration files, etc)

myplugin\rules: A set of rules

myplugin\platform: A platform model

(Search for all occurrences of %SDV% )

We will call the ‘Custom Plugin’ for the ‘Minimal’ plugin. (Search for all occurrences of ‘Custom’ and replace.)

We will call osmodel.c for platform.c

We will talk about APIs rather than DDIs. (Understand when DDI/API is plural?)

We will call osmodel-iomanager for osmodel-manager

We will call osmodel-ddis for osmodel-apis

We will rename SDV_MODEL to SDV_PLUGIN