The goal of the thesis is to create a model of the Windows NT kernel environment that can potentially be used to check WDM (Windows Driver Model) [1] driver correctness. The candidate should select an appropriate subset of WDM API and create a database of "patterns" describing correct behavior of WDM drivers with respect to the selected API subset. The patterns should follow the form used in the Specification Patterns project [2] - i.e. each pattern should contain both informal description of the pattern and a formula in a temporal logic (e.g. the Computation Tree Logic - CTL [3]) representing the pattern. When deciding about the WDM API subset that will be used as a base for the patterns, the candidate should take into account the Windows driver environment modeled as part of the Static Driver Verifier [4]. The candidate should be experienced in Windows driver programming.
Mgr. Pavel Jezek
The thesis introduces a new object-oriented specification language called DeSpec, primarily targeting model checking of the Windows NT kernel driver environment. It integrates the majority of Zing modeling language features and adds means for defining parameterized abstractions of the environment functions and structures at varying levels of detail. The Windows kernel imposes various rules on how and when the provided functions can or must be called. DeSpec enables to capture them in a form of quantified temporal logic patterns – the easy-to-read templates of LTL formulae introduced by the Bandera toolset.
Driven by DeSpec kernel specifications, a model extractor is supposed to generate a Zing model from driver source codes and the kernel header files. The thesis shows, that the run-time LTL analysis is feasible for the verification of LTL formulae in such a model using the Zing model checker. Finally, the DeSpec features are demonstrated on the specifications of a subset of the kernel functionality and rules including those verified by the recently released Microsoft Static Driver Verifier tool.
PDF version: Thesis.pdf
Defense talk: DefenseTalk.pdf
Kernel Specifications in DeSpec: Kernel.zip
DeSpec grammar (BNF): Grammar.txt
Visual Studio 2005 Beta 2 Integration Module: Whidbey.zip