5 ms·

I find it very impressive that the work actually made it into the Windows kernel. AFAIK the Linux kernel doesn't have formally verified parsers for any of the w

I find it very impressive that the work actually made it into the Windows kernel. AFAIK the Linux kernel doesn't have formally verified parsers for any of the wire formats it deals with, this seems like an improvement on actually-in-use-outside-the-lab state of the art.

anitil 4y ago
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?
- moby_click 4y ago
  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 https://hacl-star.github.io), a cryptographic library that is already used in several projects.
- mbrodersen 4y ago
  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.
  - anitil 4y ago
    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
HillBates 4y ago
bestouff 4y ago
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.
- UncleEntity 4y ago
  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.
- deterministic 4y ago
  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++.
  - masklinn 4y ago
    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.
    - jnash 4y ago
      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).
  - staticassertion 4y ago
    No amount of formal verification stops you from writing buggy code.
    - 4y ago
tonmoy 4y ago
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/ https://www.microsoft.com/en-us/research/project/slam/
- staticassertion 4y ago
  Also, P. https://www.microsoft.com/en-us/research/blog/p-programming-language-asynchrony/ 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
IshKebab 4y ago
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.

anitil 4y ago

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?

moby_click 4y ago
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 https://hacl-star.github.io), a cryptographic library that is already used in several projects.
mbrodersen 4y ago
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.
- anitil 4y ago
  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

HillBates 4y ago

bestouff 4y ago

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.

UncleEntity 4y ago
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.
deterministic 4y ago
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++.
- masklinn 4y ago
  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.
  - jnash 4y ago
    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).
- staticassertion 4y ago
  No amount of formal verification stops you from writing buggy code.
  - 4y ago

tonmoy 4y ago

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/ https://www.microsoft.com/en-us/research/project/slam/

staticassertion 4y ago
Also, P. https://www.microsoft.com/en-us/research/blog/p-programming-language-asynchrony/ 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

IshKebab 4y ago

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.