4 ms·

I've read very little detail about the Static Driver Verifier other than that it's supposed to use an SMT solver. I don't know if MS is using the same tool for

I've read very little detail about the Static Driver Verifier other than that it's supposed to use an SMT solver. I don't know if MS is using the same tool for other products in their portfolio or not. I've used it a little bit (it's a pain to set up) but have little information about exactly what it does, since it doesn't rely on any special annotations or specification language. Can you shed any light on more technical details about it? With F*, Dafny and the Lean theorem prover, it seems like Microsoft (at least the research division) is moving in the direction of formal verification but I hear very little about it's use on their commercial products. Trade secret, perhaps?

Animats 6y ago
The Static Driver Verifier is something you can download if you're a Microsoft developer. There's not much of a secret about it. There are papers. It tries to verify that a driver can't crash the rest of the kernel. No bad pointers, no infinite loops, no setting up DMA into some memory it shouldn't, no driver API calls with wrong params, stuff like that. Doesn't mean the driver will talk to the device properly. It just proves that the driver stays in its lane and doesn't mess up the rest of the system. Huge win for Microsoft. Half of Windows crashes used to come from drivers. (Yeah, yeah, undecidability makes proving halting impossible. No. It's easy to prove that most code finishes. If you're writing a kernel driver and there is any ambiguity about whether the code will finish, you're doing something very wrong. If it's hard to prove termination, you add a loop counter so that after N tries, it gives up.)
- nwmcsween 6y ago
  It would be nice if it verified stack usage or microsoft mitigated known garbage kernel modules, I spent a good part of a day setting up debug symbols and tearing out drivers without debug info till finding out a Sophos kernel driver was blue screening about 50 or so workstations with 50 or so angry people.. what fun.
mabrocks 6y ago
There's been a long, long tradition of software verification at Microsoft; look for SLAM (the original research backing the Static Driver Verifier), Yogi (SDV backend V2), Slayer (generic memory safety) and Terminator (termination of system code). All of the research is out in the open, often with reference implementations. The problem with all of these things (as with FramaC) is that they only work if you restrict the fragment of programs that you're looking at. Kernel modules work out surprisingly well, because they are not allowed to do a whole lot by convention.

Animats 6y ago

The Static Driver Verifier is something you can download if you're a Microsoft developer. There's not much of a secret about it. There are papers. It tries to verify that a driver can't crash the rest of the kernel. No bad pointers, no infinite loops, no setting up DMA into some memory it shouldn't, no driver API calls with wrong params, stuff like that. Doesn't mean the driver will talk to the device properly. It just proves that the driver stays in its lane and doesn't mess up the rest of the system. Huge win for Microsoft. Half of Windows crashes used to come from drivers. (Yeah, yeah, undecidability makes proving halting impossible. No. It's easy to prove that most code finishes. If you're writing a kernel driver and there is any ambiguity about whether the code will finish, you're doing something very wrong. If it's hard to prove termination, you add a loop counter so that after N tries, it gives up.)

nwmcsween 6y ago
It would be nice if it verified stack usage or microsoft mitigated known garbage kernel modules, I spent a good part of a day setting up debug symbols and tearing out drivers without debug info till finding out a Sophos kernel driver was blue screening about 50 or so workstations with 50 or so angry people.. what fun.

mabrocks 6y ago

There's been a long, long tradition of software verification at Microsoft; look for SLAM (the original research backing the Static Driver Verifier), Yogi (SDV backend V2), Slayer (generic memory safety) and Terminator (termination of system code). All of the research is out in the open, often with reference implementations. The problem with all of these things (as with FramaC) is that they only work if you restrict the fragment of programs that you're looking at. Kernel modules work out surprisingly well, because they are not allowed to do a whole lot by convention.