SLAM

Established: November 5, 2001

SLAM is a project for checking that software satisfies critical behavioral properties of the interfaces it uses and to aid software engineers in designing interfaces and software that ensure reliable and correct functioning. Static Driver Verifier is a tool in the Windows Driver Development Kit that uses the SLAM verification engine.

“Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas, for example, driver verification we’re building tools that can do actual proof about the software and how it works in order to guarantee the reliability.” Bill Gates, April 18, 2002. Keynote address at WinHec 2002

What's New

What’s New?

Yogi is now available to plug into the Static Driver Verifier Research Platform. To install SDVRP and Yogi, see this README.

The Summer (2011) of SLAM saw two awards and a retrospective article in CACM:

Paper:

The Static Driver Verifier Research Platform (SDVRP) is a release of SDV/SLAM for academic research. It allows the creation and checking of API-specific rules and programs (for general APIs and programs, not just driver APIs and drivers) and contains a repository of Boolean programs and test results.

Pointers in SLAM2. Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2, Thomas Ball, Ella Bounimova, Vladimir Levin, Leonardo de Moura, March 2010, MSR-TR-2010-24

Congratulations to the Driver Quality Team on winning a 2009 Engineering Excellence Award for “Improving Driver Quality thru Static Verification”. Jon Hagen, Vlad Levin, Adam Shapiro, Donn Terry, Abdullah Ustuner. PREfast for Drivers scans the driver code for issues with concurrency, proper IRQL handling, and a host of other driver challenges. The Static Driver Verifier simulates a hostile environment and systematically tests all code paths, looking for driver model violations. These complementary tools provide both quick and deep driver testing. Both tools have been adopted broadly within Windows and with third-party developers through MSDN and the Windows Driver Kit.

Static Driver Verifier Research Platform README

Overview of Static Driver Verifier Research Platform

Static Driver Verifier (SDV) is a compile-time static verification tool, included in the Windows Driver Kit (WDK). The SDV Research Platform (SDVRP) is an extension to SDV that allows you to adapt SDV to:

  • Support additional frameworks (or APIs) and write custom SLIC rules for this framework.
  • Experiment with the model checking step.

This file provides the following sections:

  • Getting Started
  • Documentation
  • Installation Instructions

Notice: Links in this file are relative and will only work after installation of SDVRP, when this file is opened from the Start -> All Programs -> Microsoft Static Driver Verifier folder.

Getting Started

Documentation

After installation the following documents are available in the Start -> All Programs -> Microsoft Static Driver Verifier folder:

  • README.htm: This file.
  • SDVRP.docx: SDVRP Documentation. This is the primary document supporting SDVRP development; however it does not cover the details of the SLIC language, or the basic operation of SDV. These topics are covered by SLIC.docx and staticdv.chm (see beneath).
  • SLIC.docx: SLIC Documentation. Syntax and semantics of SLIC, the rule specification language of SDV.
  • bebop.docx: Bebop Documentation. Syntax and semantics of Boolean Programs, the internal language used for the model checking step in SDV. Instructions on how to run on the Bebeop Boolean Program Test Suite.
  • staticdv.chm: SDV Documentation. This is the documentation provided with the regular version of Static Driver Verifier. It does not cover the SDVRP extensions. This document is also included in the Windows Driver Kit Documentation.
  • License.rtf: License Agreement. This license is also presented during download and installation.

Installation Instructions

  • Install the WDK.
    • What: The SDVRP requires that the (freely available) Windows Driver Kit Version 7.1.0 (WDK) first be installed. The WDK contains compiler, build environment, and supporting tools that is required to use SDV.
    • 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).
    • Recommend default selection of Features and Location.
    • Notice: The WDK will be installed to “%SystemDrive%\WinDDK\7600.16385.1”.
  • Install the SDVRP.
    • What: The SDVRP contains a customized version of SDV that can be used for rule development.
    • Recommend default selection of Features and Installation Path. Installation Path must be a path with no spaces in path name.
    • Notice: The SDVRP will be installed to “%SystemDrive%\WinDDK\SDV”.
  • Confirm the WDK use the SDVRP version of SDV:
    • What: The WDK already has SDV available (in the “tools\sdv” folder), but this WDK version of SDV is not useable for SDVRP work. The WDK build environment should automatically detect that SDVRP is installed and use the SDVRP version of SDV.
    • 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)
    • Validate that this line is printed when you start the build environment: “WARNING: Using external version of Static Driver Verifier.”
    • In case of trouble you should look at the script %SystemDrive%\WinDDK\7600.16385.1\bin\setenv.bat, search for SDV.
  • The SDVRP is now ready for use.

Resources

Publications

Book Chapter

History

The SLAM Process

SLAM Specifications

Boolean Programs

Abstraction Refinement

Concurrency

Miscellaneous

News

News

Related Projects

Related Projects

Collaborators

Co-founders

MSR colleagues

Windows colleagues

  • Nar Ganapathy
  • Jakob Lichtenberg
  • Rahul Kumar
  • Vladimir Levin
  • Con McGarvey
  • Abdullah Ustuner
  • Donn Terry

Alumni

  • Bohus Ondrusek

Visitors

Interns

2008

2007

2006

2003

2002

2001

2000

2004

​