Static driver verifier, a formal verification tool for Windows device drivers

Author

Levin, V.

Author_Institution

Microsoft Corp., Redmond, WA, USA

fYear

2004

fDate

23-25 June 2004

Firstpage

151

Abstract

Microsoft is improving the quality of system software, in particular, through the intensive application of formal methods. The ultimate goal is to reach a point at which robustness against failures and attacks can be guaranteed. To support this goal, the company has invested in advanced testing and verification tools. Examples include model-based testing supported by AsmL/SpeC#, TLC and Zing model checkers for concurrency verification, a type system augmented with pre-/post- conditions (Fugue), advanced static analysis tools (PreFix, ESP, etc.) and Static Driver Verifier, SDV. SDV is a formal verification tool aimed at checking device drivers developed using the Windows Driver Model (WDM) interface. The WDM interface consists of more than 800 functions - entry points into the kernel functionality. To correctly use the WDM interface is not easy: WDM rules are numerous and complicated.

Keywords

device drivers; program verification; Microsoft; Windows device drivers; formal methods; formal verification; static driver verifier; Application software; Concurrent computing; Electrostatic precipitators; Formal verification; Packaging; Robustness; Safety; System software; System testing; Wavelength division multiplexing;

fLanguage

English

Publisher

ieee

Conference_Titel

Formal Methods and Models for Co-Design, 2004. MEMOCODE '04. Proceedings. Second ACM and IEEE International Conference on

Conference_Location

San Diego, CA, USA

Print_ISBN

0-7803-8509-8

Type

conf

DOI

10.1109/MEMCOD.2004.1459840

Filename

1459840