This is not new for MS. Windows 98 and XP would get a lot of BSOD because of third party drivers doing illegal things. MS have been investing heavily in formal verification since early 2000s because of that. My master’s adviser (and many more professors working in formal verification) would get most of their funding from MS. One early successful example I can think of is SLAM[1]

1. https://www.microsoft.com/en-us/research/project/slam/

Also, P. https://www.microsoft.com/en-us/research/blog/p-programming-...

> P got its start in Microsoft software development when it was used to ship the USB 3.0 drivers in Windows 8.1 and Windows Phone

Linux will probably get some Rust parsers in the future, which are IMHO even better because they are easy to write so you're sure they are robust - whereas formally verifying a parser may or may not be done depending on the coder's available time and willingness to do so.

Rust doesn’t stop you from writing buggy code. However I do agree that it is easier to write memory safe code in Rust compared with C/C++.

TBF lots of formal tools don’t either, because you still have to translate the proven code by hand.

It looks like Microsoft’s does the translation, so the only risk is bugs in the code generator, which seems nice.

There’s also Google’s wuffs, but I don’t think that is formal, it just ensures memory safety.

Yep if the translation is done by hand then that might be a potential problem. However a lot of modern proof tools have proven correct translators (based on the CompCert work).

No amount of formal verification stops you from writing buggy code.

I don't think you understand what "proven correct" means. If you formally prove a spec correct using modern proof tools then it is guaranteed to have zero bugs. Nobody has found even a single bug in the proven correct CompCert C compiler for example. However people find bugs in gcc all the time.

It means that a program has been verified against a model, and properties of that model are held true.

What it does not mean is that the program is bug free. That would, of course, violate the halting problem, or its generalization Rice's Theorem - non-trivial programs can not have arbitrary properties proven about them.

There's also Gödel's Incompleteness Theorem, obviously, as well as the fact that a proof is only as good as its model.

It wouldn’t break Rice’s Thm to prove it for a particular program. All Rice’s Thm says is that any algorithm must fail on some programs.

It would if you're talking about arbitrary classes of bugs.

Not so. Consider the algorithm that reports "Yes" for all inputs for all program properties. For a large number of programs and properties, this algorithm will report the correct information.

Not true for non-Turing complete languages. Which is why all proof tools require a proof of termination. Some do it automatically (essential ruling out Turing complete languages) others require a formal proof of termination by the user.

Ages ago my advisor had a paper proving WEP to be correct. Many years later, a serious flaw was discovered.

Even formal verification can be insufficient.

Was it a proof by hand or using a formal proof tool? Never trust proofs that aren’t formally verified by a modern proof tool.

Formal verification with model checking.

That frankly sounds hard to believe. Which proof tool did he use? Link to paper?

f* (one system on display in this paper) can extract to c/assembler suitable for inclusion in a hand-written c source tree, all the while giving a wider and more interesting set of guarantees with the added benefit that you won't have to depend on a rust toolchain to build your project (bootstrapping f* is considerably easier, and you only have to do it when you check in your verified bits)

funny enough, much like rust, one of its most widely-deployed applications lives in firefox; see project-everest.github.io

If I understand this property it takes a specification and generates a formally proven parser that lets you cast the bytes to a struct or runs code to do something with the data.

All automagic, can’t see how it could get much simpler than that.

formal verification is about functionality, not about your emotions.

Haven't you heard? The only bugs are those caused by memory safety, and only switching to Rust can save us from the insanity of managing our own memory.

You are joking right? Just checking :)

Yes, I was being quite sarcastic above

Windows' kernel is way ahead of Linux in many ways. It's a bit of a delusion that so many people think it hasn't advanced since Windows XP. Perhaps wilful denial.

It's going to take me a while to fully understand this paper. I wonder what the route to incorporating something like this in the Linux kernel would look like?

Generating readable C code was an important goal from early on. Parts of the linux kernel would have to be translated to Low*, which is the subset of F*, that can be extracted to C.

I guess there would be a new build step, that runs when code is checked in, to not burden everyone with all the new toolchain (F*, z3, karamel, maybe OCaml and more). While the generated C code can be read and understood by C programmers, changes to that part should be done in Low* and that may require changes to proofs in F* or to the extraction tool (karamel). That's a pretty big investment for a project like linux and I guess, any work in that direction will happen on forks for a while, before there is enough confidence that such changes are sustainable.

A good first candidate may be HACL* (https://hacl-star.github.io), a cryptographic library that is already used in several projects.

The end result is generated C code. So you could simply add the generated C code to the kernel like you would any other C code. And keep the proof chain separate from the kernel. My guess is that it is what Microsoft is doing with the kernel code.

My question was more around that it would have to replace existing code, so you'd need to advocate for it and come up with some way of incorporating it in the build. I'm not all that familiar with the development culture of the kernel but I imagine that large changes like this would have to be introduced slowly