Hacker News Reader

Comment by colejohnson66 | Hacker News Reader

As someone who's never worked with the Windows kernel, I'm curious about the tools you mention. How do I get them?

Microsoft has been shipping static analysis tools with the Windows DDK for a long time (originally PREfast[1], now Static Driver Verifier[2]). I believe the static analysis is even integrated with Visual Studio now.

[1]: http://research.microsoft.com/en-us/news/features/prefast.as... [2]: https://msdn.microsoft.com/en-us/library/windows/hardware/ff...

Driver Verifier is the main one I've used. It's pretty awesome.

https://msdn.microsoft.com/en-us/library/windows/hardware/ff...

I think the most significant are the SAL version 2 annotations. This is a nice introduction : https://www.cs.cmu.edu/~fp/courses/15122-f10/lectures/25-sal....

Basically, there's an additional step after compilation, called code analysis, which runs this static verification. I think it's implemented on top of the Z3 theorem prover.

Here's a list of the driver code analysis warnings. I wonder how many of these could be codified as compile-time checks in the winapi-kmd-rs library. For example, the KIRQL type is a u8 in winapi-kmd-rs, but the code analysis warnings the valid IRQL range is 0–31.

https://msdn.microsoft.com/en-us/library/windows/hardware/ff...

They are part of the DDK

https://msdn.microsoft.com/en-us/library/windows/hardware/ff...

https://msdn.microsoft.com/en-us/library/windows/hardware/hh...

https://msdn.microsoft.com/en-us/library/windows/hardware/ff...

Reply on news.ycombinator.com