Hacker News Reader

Comment by nickpsecurity | Hacker News Reader

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.

View on HN

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.

Reply on news.ycombinator.com