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

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.