BOX 3.2

Lessons Learned from the Technology-Transfer Effort Associated with Microsoft’s Static Driver Verifier

The Static Driver Verifier (SDV) systematically analyzes Windows device drivers against a set of rules that define what it means for a device driver to properly interact with the Windows operation system kernel. The SDV is based on a code-analysis engine known as SLAM, which incorporates type checking, model checking, program analysis, and automated deduction. SLAM was the result of research to create methodologies and tools to check the correctness of partial specification of program behavior—specifically the use of the device driver interface to the Windows kernel. The SDV provides an automated environment for running SLAM that incorporates rules for the Windows Driver Model; a well-articulated environment model of the Windows kernel and other drivers; scripts to configure the SDV with driver-specific information; and a graphical user interface to present results.

Intellectually, the primary lesson learned in the transition from the SLAM research to the working SDV tool is to focus on problems rather than technology. The problem must be recognized as critical by product developers and end users, and not just technically interesting to researchers. It must also be bounded sufficiently to provide a tangible solution with measurable success criteria. All parties involved, including product developers, end users, and researchers, must see clearly the link between the problem at hand and the solution—which is what the implementation of the SDV framework made clear in the case of the SLAM research.

From an organizational point of view, the primary lesson is that leaving the scaling up of a prototype research as an exercise for the development group is likely to result in lack of acceptance and adoption, since the development group will not necessarily make the “obvious” leap from technology solution to useful and viable product. Successful technology transfer is, at least in part, a research team responsibility, and involves considerable effort on the part of researchers to understand how product teams operate, how they allocate resources, how they make decisions, and what it takes to turn a prototype into a product.

SOURCE: Adapted from Thomas Ball, Byron Cook, Vladimir Levin, and Sriram K. Rajamani, SLAM and Static Driver Verifier: Technology Transfer of Formal Methods Inside Microsoft, Microsoft Research Technical Report, MSR-TR-2004-08, January 2004.

under such circumstances. In addition, because post-catastrophe deployments often change the boundaries of what is politically feasible, research should also consider what sensible things might be done if and when such opportunities arise.
New Computing Paradigms and Applications Domains

Cybersecurity problems in an environment of large-scale distributed computing, embedded computing, batch processing and mainframe com-

The National Academies | 500 Fifth St. N.W. | Washington, D.C. 20001
Copyright © National Academy of Sciences. All rights reserved.
Terms of Use and Privacy Statement