DevCon:Static Driver Verifier

Ok, its the last day, and I only have one session left, titled "Static Driver Verifier" (SDV).

All I can say is WOW. They have been doing some neat work in Microsoft Research on a neat new tool that can find bugs in device drivers at compile time. It can even find bugs that Driver Verifier and Prefast will miss. (I will talk about prefast in another post)

SDV will look through all possible paths in a driver that are excercied by the OS model. The only drawback is the requirements. To run the tool, they are wanting about half a gig to a gig of ram! And what sucks more... we can't HAVE it yet. GRRRRRRRR.

SDV is a really interesting tool. The analogy I liked was that "SDV is like having Adrian Oney together with a logician checking your code at compile time". SDV basically knows how the interfaces should be used. It provides a set of interface usage rules that the driver should obey. When it doesn't, you find out about it.

Because SDV knows the OS internals, it can attempt to find a correctness proof. This correctness proof is found using abstraction search and symbolic model checking. If a bug is found, it shows you the path through your driver to the bug. This will significantly increase the quality of drivers that use it. Its a heavy hammer so to speak, and is a welcomed additional tool that will be part of a future DDK.