This is a neat project but with a caveat: Microsoft has solid, verification tools for C drivers but Rust doesn't have the equivalent. The tools are especially important for finding behavioral problems at the interface between the driver itself and Windows.
So, my suggestion for production by Rust developers is to simultaneously develop the driver in Rust and a C subset. Keep the two logically equivalent. Rust's checker will catch problems in C program possibly. More importantly, Microsoft's analysis tools will probably catch problems in both if it's a logical error. Should result in some pretty robust drivers.
So is there some documentation on the "behavioral problems" their checker finds? If we know what to look out for, we can simply write some clippy lints to replicate the checks.
I had the original papers on SLAM and driver verification. Didn't have this one. It's a great write-up with lots of useful data on a few, related topics. Thanks for the link.
I just had time to look at clippy itself. Funny name given I imagined redoing Microsoft's Clippy in Rust still wouldn't fix it. :)
I'm keeping the page in case I field Rust stuff as it's a nice list of things to look for. Not just for this tool but other developers applying CompSci solutions to Rust. They'll need a list of issues to encode in those.
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.
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.
Based on the cousin-comments in this thread, I don't think it would. Part of the benefits come from static analysis, but that static analysis uses annotations (such as for pre and post conditions) that the Rust to C compilation would not have.
LLVM had a c backened, it is no longer maintained. There was a project [1] to resurrect it but there hasn't been a commit in 11 months so I don't know the state of it.
I've seen it come up a lot for various reasons related to rust so maybe someone will do the work. I think most of the reasons you'd want a C backened could be solved better just by extending the compiler, but not this case (closed source c-only utility).
SDV uses model checking and symbolic execution. its exploration is partial. the guarantees you get from the rust type checker are much stronger.
the real trick would be, could you represent the contract between the kernel and drivers as rust types. if you could, then you don't need SDV, you just need the rust type checker.
SDV proves properties that are in general undecidable, and as such it is not possible to substitute the Rust type checker for it. The critical difference is that software verification algorithms are allowed to be partial (i.e. not terminate or return "unknown"), while type checking algorithms are required to be total.
Edit: Another way to look at it is that software verification tools find proofs for properties, while type checkers only verify proofs (given as the program structure and type annotations).
One option which allows you to keep Turing completeness is just asking the user to write more annotations, such as loop invariants and termination conditions. For example the Dafny [1] language+verifier does this: it automates the tedious parts of the proofs but requires the user to give the hard parts (loop invariants) as annotations.
That would be a real trick. Meanwhile, the reality is Microsoft's tools cover more stuff in this area. That blue screens are rare speaks to tge results. Make sonething equivalent for Rust then we'll talk along these lines.
This looks very cool, definitely something I'm tempted to play with (having never done any dev in this area before).
However, the feedback loop for debugging drivers on Windows seems quite manual (https://msdn.microsoft.com/en-us/library/windows/hardware/mt...). On Linux I'd have SSH at my disposal - are there any best practices for speeding up this copy/install process? Cygwin sshd could be an option, off the top of my head?
First step I'd say is to import your certificate into the the debugged computer, so it doesn't warn you every time you re-upload the driver [1]. Second, use powershell remoting [2]. Pretty much all of the other steps can be established and automated with a powershell remote connection. I'm in fact surprised that microsoft hasn't updated that page to use powershell, because driver debugging is a task where it could be invaluable in helping.
Judging from the screenshot it even works on Windows XP. This is really impressive, since Windows kernel drivers typically have to be written in plain old C.
It's just the kind of area Rust does really well in. From a certain point of view, Rust can produce executables that are pretty much "written in plain old C" in that they can provide linkage that works like C linkage, don't necessarily need heap/GC, don't necessarily need big std library presuming userspace context.
I'd wager you could do something similar with D (soon if not now), since its no-std support is catching up w/Rust's.
I have a "framework" (really just a build tool and some examples) for bare-bones Win32 support for D[1]. I haven't tried writing kernel drivers with it though.
I used it to create a few Fallout 4 mods[2]. Avoiding the stdlib was not necessary there, but I didn't want the bloat. One interesting application of D's metaprogramming has been automatically recursively instrumenting the DirectX COM API just from the D interface definitions[3] (not IDLs).
As a side note, Windows XP support in Rust is partial. We don't support running the compiler on XP, but do support compiling _to_ it, but some parts of the standard library may not work. It's missing some primitives, basically.
Not that that matters in the context of writing a kernel driver, mind you...
I meant it's written in C++[0]. The interface is exported through standard C functions, but the header files also have the declarations guarded with "extern "C"".
"Legacy" is as much said. It still forms the basis interface that is used by WDF. Also you still need to use the WDM directly if you are writing a filesystem driver.
Besides that, the WDF source is available under a MIT license, so it might make more sense to just port it to Rust.
So, my suggestion for production by Rust developers is to simultaneously develop the driver in Rust and a C subset. Keep the two logically equivalent. Rust's checker will catch problems in C program possibly. More importantly, Microsoft's analysis tools will probably catch problems in both if it's a logical error. Should result in some pretty robust drivers.