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.