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.
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"".
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).
"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.
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.
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.
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.
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).
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.
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.
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.
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.
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.
44 comments
[ 3.5 ms ] story [ 97.3 ms ] threadNot that that matters in the context of writing a kernel driver, mind you...
But core of NT is stable since 3.1 (1993) and even there are structures which are dated 1989 (e.g. [FILE_OBJECT](https://msdn.microsoft.com/en-us/library/windows/hardware/ff...).
Microsoft do have some sample drivers that are written in C++, e.g. https://github.com/Microsoft/Windows-driver-samples/tree/mas...
[0]: https://github.com/Microsoft/Windows-Driver-Frameworks/tree/...
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 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).
They have stated multiple times that C++ is the way forward for systems programming on Windows.
https://herbsutter.com/2012/05/03/reader-qa-what-about-vc-an...
The new C runtime library was re-written in C++ with extern "C" for the entry points.
https://blogs.msdn.microsoft.com/vcblog/2014/06/10/the-great...
Vista introduced support for C++ in the kernel
https://msdn.microsoft.com/en-us/library/jj620896(v=vs.110)....
For example many of the new APIs were COM based, not plain C like ones.
Besides that, the WDF source is available under a MIT license, so it might make more sense to just port it to Rust.
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?
[1] https://blog.jourdant.me/ps-installing-drivers-from-untruste...
[2] https://technet.microsoft.com/en-us/library/dd819505.aspx
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.
https://msdn.microsoft.com/en-us/library/windows/hardware/ff...
[1]: http://research.microsoft.com/en-us/news/features/prefast.as... [2]: https://msdn.microsoft.com/en-us/library/windows/hardware/ff...
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...
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.
https://msdn.microsoft.com/en-us/library/windows/hardware/ff...
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).
[1]:https://github.com/draperlaboratory/llvm-cbe
(https://github.com/Manishearth/rust-clippy)
https://msdn.microsoft.com/en-us/library/windows/hardware/ff...
One of the more successful cases of research out of Microsoft Research making it into production use in regular-Microsoft.
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.
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.
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).
Like, you can't determine the halting problem for a turing complete language, but you can for s more restricted language.
[1]: http://research.microsoft.com/en-us/projects/dafny/