Windows Kernel-Mode Drivers Written in Rust | Hacker News Reader

Windows Kernel-Mode Drivers Written in Rust

github.com

216 pointsadamnemecek43 comments

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.

(https://github.com/Manishearth/rust-clippy)

Cpeterso already posted this link:

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

And here's a paper on the research underlying those tools: http://cacm.acm.org/magazines/2011/7/109893-a-decade-of-soft...

One of the more successful cases of research out of Microsoft Research making it into production use in regular-Microsoft.

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.

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...

Is there a Rust->C compiler? (I'm on phone or would check myself). That seems like it would provide the best of both worlds, no?

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.

If LLVM has a C backend, then yes, otherwise, no.

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).

[1]:https://github.com/draperlaboratory/llvm-cbe

Maintained fork https://github.com/JuliaComputing/llvm-cbe

no, just no.

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).

But couldn't the type system guarantee a sufficent subset of all the possible interactions with the api?

Like, you can't determine the halting problem for a turing complete language, but you can for s more restricted language.

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.

[1]: http://research.microsoft.com/en-us/projects/dafny/

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.

[1] https://blog.jourdant.me/ps-installing-drivers-from-untruste...

[2] https://technet.microsoft.com/en-us/library/dd819505.aspx

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).

  [1]: https://github.com/CyberShadow/SlimD
  [2]: https://github.com/CyberShadow/csfo4
  [3]: https://github.com/CyberShadow/csfo4/blob/master/dxlog/d3d11.d

Windows has been moving to C++ on kernel space since Vista, even newer C-like APIs are actually C++ code with extern "C" calling convention.

They have stated multiple times that C++ is the way forward for systems programming on Windows.

Any reference for this?

Yes, Herb Sutter's blog regarding C99.

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)....

I don't think it happened until much later than Vista.

Vista was when the wheels were set on march, not when the travel ended.

For example many of the new APIs were COM based, not plain C like ones.

Being able to integrate with C efficiently is one of the goals of the language.

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...

Yep, most of modern atomic primitives at WinAPI available since Vista (like SRWLock, Condition variables).

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...).

This is not at all true. Microsoft has recommended for a long time that new drivers use WDF which is a C++ library

Do you have a source for that? KMDF seems to be a C-API.

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"".

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/...

It has a C API, but everything under the hood is C++. The source is actually public now: https://github.com/Microsoft/Windows-Driver-Frameworks

It is very nice to see this effort. I have one suggestion - integrate with WDF APIs instead of the lower level and legacy WDM APIs.

"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.

It is not effort. It was just a fun :)

Except WDF is a C++ API.

Reply on news.ycombinator.com