6 ms·

Hardening attack surfaces with formally proven binary format parsers

150 points by deterministic 4y ago

dataangel 4y ago
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.
tbrownaw 4y ago
> Software artifacts. The application of our toolchain to Windows includes proprietary source code and is not publicly available. However, the 3D toolchain, including the EverParse libraries, the F programming language, Z3 SMT solver, and the KaRaMeL C code generator are all open source and developed publicly on GitHub. Documentation, code samples, and links to our latest tool releases are available from https://project-everest.github.io/everparse https://project-everest.github.io/everparse. From the linked paper.
sbf501 4y ago
The thing I'd like to understand that the paper didn't touch on: how do we know the example TCP RFC English Language description isn't logically flawed? If the F* code adheres to the RFC, does the verification prove that the F* matches the 3D of the RFC, or does it find errors in the RFC itself? On a side note, rather than debating re-writing the Linux kernel in Rust so that it is memory safe(er), why not start working on a formally hardend kernel code? Or does this only apply to logical propositions, e.g. the RFC?
- codelion 4y ago
  There is already a formally verified kernel - https://sel4.systems/home.pml https://sel4.systems/home.pml
  - schoen 4y ago
    That's very important work, but I don't think it includes many of the features we would associate with an operating system. https://sel4.systems/About/seL4-whitepaper.pdf https://sel4.systems/About/seL4-whitepaper.pdf It's hard to overstate how (intentionally) tiny it is compared to something like Linux or a BSD kernel.
  - sbf501 4y ago
    I didn't know that existed. What a fantastic project. Thanks for the link.
- woodruffw 4y ago
  > how do we know the example TCP RFC English Language description isn't logically flawed? We don't, in the general case. In the specific case of TCP, the RFC has had many errata over the years[1] (many of which are logical errors). This is a recurring problem in formal verification: you verify with respect to a particular description of the system or protocol, which itself may be either ambiguous or fail to reflect actual implementations. You can tighten that by verifying with respect to a formal definition, which can eliminate the ambiguity, but only pushes the trust as far as the proof generator and verifier themselves. You then maybe have multiple independent proof systems arrive at the same conclusion to strengthen your belief in the result, but at that point you're doing differential testing and not formal verification. [1]: https://www.rfc-editor.org/errata/rfc793 https://www.rfc-editor.org/errata/rfc793
tshanmu 4y ago
https://project-everest.github.io/everparse/3d.html#d https://project-everest.github.io/everparse/3d.html#d has the details. Uses https://www.fstar-lang.org/ https://www.fstar-lang.org/
752963e64 4y ago
Hello microsoft o/ It strange u posting shit that way just a day after I shown some tricks with binaru... :) Anyway my slogan is "Everything is free, so deflate!" :D
Mikhail_K 4y ago
Beware microsoft bearing gifts
- jnash 4y ago
  Most of the code is open source. No problem with that.

150 points by deterministic 4y ago

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.

tbrownaw 4y ago

> Software artifacts. The application of our toolchain to Windows includes proprietary source code and is not publicly available. However, the 3D toolchain, including the EverParse libraries, the F programming language, Z3 SMT solver, and the KaRaMeL C code generator are all open source and developed publicly on GitHub. Documentation, code samples, and links to our latest tool releases are available from https://project-everest.github.io/everparse https://project-everest.github.io/everparse. From the linked paper.

sbf501 4y ago

The thing I'd like to understand that the paper didn't touch on: how do we know the example TCP RFC English Language description isn't logically flawed? If the F* code adheres to the RFC, does the verification prove that the F* matches the 3D of the RFC, or does it find errors in the RFC itself? On a side note, rather than debating re-writing the Linux kernel in Rust so that it is memory safe(er), why not start working on a formally hardend kernel code? Or does this only apply to logical propositions, e.g. the RFC?

codelion 4y ago
There is already a formally verified kernel - https://sel4.systems/home.pml https://sel4.systems/home.pml
- schoen 4y ago
  That's very important work, but I don't think it includes many of the features we would associate with an operating system. https://sel4.systems/About/seL4-whitepaper.pdf https://sel4.systems/About/seL4-whitepaper.pdf It's hard to overstate how (intentionally) tiny it is compared to something like Linux or a BSD kernel.
- sbf501 4y ago
  I didn't know that existed. What a fantastic project. Thanks for the link.
woodruffw 4y ago
> how do we know the example TCP RFC English Language description isn't logically flawed? We don't, in the general case. In the specific case of TCP, the RFC has had many errata over the years[1] (many of which are logical errors). This is a recurring problem in formal verification: you verify with respect to a particular description of the system or protocol, which itself may be either ambiguous or fail to reflect actual implementations. You can tighten that by verifying with respect to a formal definition, which can eliminate the ambiguity, but only pushes the trust as far as the proof generator and verifier themselves. You then maybe have multiple independent proof systems arrive at the same conclusion to strengthen your belief in the result, but at that point you're doing differential testing and not formal verification. [1]: https://www.rfc-editor.org/errata/rfc793 https://www.rfc-editor.org/errata/rfc793

tshanmu 4y ago

https://project-everest.github.io/everparse/3d.html#d https://project-everest.github.io/everparse/3d.html#d has the details. Uses https://www.fstar-lang.org/ https://www.fstar-lang.org/

752963e64 4y ago

Hello microsoft o/ It strange u posting shit that way just a day after I shown some tricks with binaru... :) Anyway my slogan is "Everything is free, so deflate!" :D

Mikhail_K 4y ago

Beware microsoft bearing gifts

jnash 4y ago
Most of the code is open source. No problem with that.