6 ms·

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

by 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
- sbf501 4y ago
  That's what I was getting at with the second sentence in my post: we can verify the code matches the spec, but not that the spec is flawed. So this verification is what CPU designers do: they create a RTL (HDL, VHDL, Verilog) and then a circuit (gates) and then Magma or Cadence or Synopsys tools formally verify that the logic in the behavioral model matches the implementation model. However, if the microarchitect had a brain fart, the RTL is bugged to begin with. I was hoping this could go backwards one step further and give the microarchitect/RFC-editor a swift kick in the pants. :)
  - drpixie 4y ago
    I think that's the real advantage of RISC architectures - a small spec leaves less space for problems. Not no space, but less space.
    - rurban 4y ago
      Yes, but the various HW bugs and exploits, e.g cache leaks and poisoning - Spectre, Meltdown, ..., are not handled. Also not in the mentioned and formally proven crypto libs.
    - sbf501 4y ago
      Advantage over what? The idea that RISC is somehow simpler went the way of the dinosaur 30 years ago. The ISA does not define performance, that is the microarchitecture, which is where all of the engineering effort is spent. You can have the classic ISA of the Turing Machine that we all learned about in comp-sci 101 classes: "Load/Store/Add/Compare/Jump" and it would be simple but dog-ass slow. Not to mention open to all sorts of attacks and exploits (buffer overflows, stack smashing), and meta attacks (side-channel), or Goedels incompleteness. The uarch is where the action happens.
      - drpixie 4y ago
        We were talking about correctness. RISCs by definition have simpler architectures that CISCs - that's what makes them RISCs. And simpler architectures leave less room for confusion/bugs/faults in the architecture, irrespective how they are implemented.
DannyBee 4y ago
Remember this is a set of parsers. So it's goal is to accept valid-according-to-spec data, and reject all other data, and do so in a safe way. In that sense, the spec can only be logically flawed in a few ways For example: 1. if it specifies impossible constraints on data it accepts (IE field1 < field2 && field2 > field1) 2. misses dependent constraints necessary to safely prove other things (field2 - field1 > 0 without specifying that field2 > field1) etc Assuming you specify the assertions in the code, it will find these errors because it will not be able to prove the arithmetic is sound. To the degree it is possible for the spec to be logically flawed, but not cause underflow/overflow/etc, it will not detect it.
schoen 4y ago
> how do we know the example TCP RFC English Language description isn't logically flawed? They'll surely have needed to translate the English specification into a formal specification. That act of translation isn't itself a formal process, so it's subject to errors, and also subject to dispute in case of ambiguities or underspecification or contradictions in the English text. You can never formally prove that an informal natural language specification corresponds to a formal specification written in a formal language (although you could try to take another abstraction step by writing a formal grammar and formal semantics for the natural language and then claiming that the interpretation of the natural language text, under that interpretation, agrees with your formal specification... I don't believe this is common or likely to yield useful results unless the natural language text was written in a very controlled way with this kind of application in mind). > 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? Rust's type system can actually be viewed as a formal proof system, where the type checker is verifying proofs about behaviors of the program. But the proofs in question are somewhat weak compared to other formal methods techniques, which can potentially be used to prove stronger claims about program behavior. The Rust ones aren't trivial, though; they rule out quite a few kinds of errors even without having a formal specification for the program's behavior beyond that given by the type annotations. And there are some other features inspired by formal methods, like the fact that match patterns must specify a behavior for every possible value of the expression: https://doc.rust-lang.org/book/ch18-03-pattern-syntax.html https://doc.rust-lang.org/book/ch18-03-pattern-syntax.html Writing formally verified code with a richer specification tool is harder and slower going. Microsoft is paying the equivalent of an academic department (in MSR) to do some of that work. I would hope we would soon see similar stuff in the free software world from a regular academic department at a university... maybe inspired by some of this work from MSR!
tialaramex 4y ago
The work of turning a technical document into something automated provers can work on is often revealing when it comes to logical flaws which is itself a valuable product. However, even when this appears to be successful and the proof tool verifies your design has the properties you wanted, there can be hidden assumptions in the proof which do not match the human understanding of the technical document. TLS 1.3 was proved this way before the RFC was signed off. We know TLS 1.3 does what it says on the tin, assuming the constituent elements work as specified (e.g. AES is a working block cipher, SHA256 is a working cryptographic hash function, Elliptic Curve Diffie Hellman is a working key agreement protocol). However, it turns out they proved something slightly different from what humans would have understood from the document. The result is the Selfie attack. NB This applies specifically to Pre-shared Key authentication, stuff like your web browser isn't affected. Here's how it goes: Alice and Bob are using a PSK to communicate securely, but their Cat would like to manipulate them. Based on their understanding of the pre-errata RFC document, Alice and Bob agreed a single Pre-shared Key, let's call that ABA, which the Cat doesn't know, and they use TLS 1.3. 0. Bob feeds the cat before leaving for work 1. Alice wakes up, notices the Cat's food bowl is empty and sends an encrypted message to Bob, Encrypt(ABA, "Did you feed the cat?") 2. The Cat intercepts Alice's encrypted message and sends it back to her. The Cat can't read the message, nor tamper with it, but just sends it unaltered and trusts that will have the desired effect. 3. Alice receives an authentic message encrypted with the ABA key, which she presumes is from Bob, it says "Did you feed the cat?" 4. Alice sends an encrypted reply, Encrypt(ABA, "No") 5. The Cat intercepts this message too and sends it back to Alice again 6. Alice receives the reply, which she presumes is from Bob, it says "No". 7. Alice feeds the cat again. The cat has now been fed twice. Attack successful. How did this attack sneak part the proof? Well, the proof says Alice and Bob should agree two keys, an Alice->Bob key (let's calls this AB1) and a Bob->Alice keys (call it BA1). When Alice receives her own message encrypted with AB1, she can see she sent it, not Bob, and so she detects the Cat's attack. So the proof is fine. The person writing the proof assumed this is what was meant in the human readable document describing TLS 1.3, but the other humans working from this document assumed it would be fine for Alice and Bob to agree a single key ABA. It's certainly not highlighted in the original document that this is a concern and you must agree two keys. [ There are also lots of other things you could do, if you're careful and know about this attack, but for some reason can't just agree twice as many keys. However the correct basic design to explain in the document is to just make separate keys for each direction ]

by sbf501 4y ago

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

sbf501 4y ago
That's what I was getting at with the second sentence in my post: we can verify the code matches the spec, but not that the spec is flawed. So this verification is what CPU designers do: they create a RTL (HDL, VHDL, Verilog) and then a circuit (gates) and then Magma or Cadence or Synopsys tools formally verify that the logic in the behavioral model matches the implementation model. However, if the microarchitect had a brain fart, the RTL is bugged to begin with. I was hoping this could go backwards one step further and give the microarchitect/RFC-editor a swift kick in the pants. :)
- drpixie 4y ago
  I think that's the real advantage of RISC architectures - a small spec leaves less space for problems. Not no space, but less space.
  - rurban 4y ago
    Yes, but the various HW bugs and exploits, e.g cache leaks and poisoning - Spectre, Meltdown, ..., are not handled. Also not in the mentioned and formally proven crypto libs.
  - sbf501 4y ago
    Advantage over what? The idea that RISC is somehow simpler went the way of the dinosaur 30 years ago. The ISA does not define performance, that is the microarchitecture, which is where all of the engineering effort is spent. You can have the classic ISA of the Turing Machine that we all learned about in comp-sci 101 classes: "Load/Store/Add/Compare/Jump" and it would be simple but dog-ass slow. Not to mention open to all sorts of attacks and exploits (buffer overflows, stack smashing), and meta attacks (side-channel), or Goedels incompleteness. The uarch is where the action happens.
    - drpixie 4y ago
      We were talking about correctness. RISCs by definition have simpler architectures that CISCs - that's what makes them RISCs. And simpler architectures leave less room for confusion/bugs/faults in the architecture, irrespective how they are implemented.

DannyBee 4y ago

Remember this is a set of parsers. So it's goal is to accept valid-according-to-spec data, and reject all other data, and do so in a safe way. In that sense, the spec can only be logically flawed in a few ways For example: 1. if it specifies impossible constraints on data it accepts (IE field1 < field2 && field2 > field1) 2. misses dependent constraints necessary to safely prove other things (field2 - field1 > 0 without specifying that field2 > field1) etc Assuming you specify the assertions in the code, it will find these errors because it will not be able to prove the arithmetic is sound. To the degree it is possible for the spec to be logically flawed, but not cause underflow/overflow/etc, it will not detect it.

schoen 4y ago

> how do we know the example TCP RFC English Language description isn't logically flawed? They'll surely have needed to translate the English specification into a formal specification. That act of translation isn't itself a formal process, so it's subject to errors, and also subject to dispute in case of ambiguities or underspecification or contradictions in the English text. You can never formally prove that an informal natural language specification corresponds to a formal specification written in a formal language (although you could try to take another abstraction step by writing a formal grammar and formal semantics for the natural language and then claiming that the interpretation of the natural language text, under that interpretation, agrees with your formal specification... I don't believe this is common or likely to yield useful results unless the natural language text was written in a very controlled way with this kind of application in mind). > 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? Rust's type system can actually be viewed as a formal proof system, where the type checker is verifying proofs about behaviors of the program. But the proofs in question are somewhat weak compared to other formal methods techniques, which can potentially be used to prove stronger claims about program behavior. The Rust ones aren't trivial, though; they rule out quite a few kinds of errors even without having a formal specification for the program's behavior beyond that given by the type annotations. And there are some other features inspired by formal methods, like the fact that match patterns must specify a behavior for every possible value of the expression: https://doc.rust-lang.org/book/ch18-03-pattern-syntax.html https://doc.rust-lang.org/book/ch18-03-pattern-syntax.html Writing formally verified code with a richer specification tool is harder and slower going. Microsoft is paying the equivalent of an academic department (in MSR) to do some of that work. I would hope we would soon see similar stuff in the free software world from a regular academic department at a university... maybe inspired by some of this work from MSR!

tialaramex 4y ago

The work of turning a technical document into something automated provers can work on is often revealing when it comes to logical flaws which is itself a valuable product. However, even when this appears to be successful and the proof tool verifies your design has the properties you wanted, there can be hidden assumptions in the proof which do not match the human understanding of the technical document. TLS 1.3 was proved this way before the RFC was signed off. We know TLS 1.3 does what it says on the tin, assuming the constituent elements work as specified (e.g. AES is a working block cipher, SHA256 is a working cryptographic hash function, Elliptic Curve Diffie Hellman is a working key agreement protocol). However, it turns out they proved something slightly different from what humans would have understood from the document. The result is the Selfie attack. NB This applies specifically to Pre-shared Key authentication, stuff like your web browser isn't affected. Here's how it goes: Alice and Bob are using a PSK to communicate securely, but their Cat would like to manipulate them. Based on their understanding of the pre-errata RFC document, Alice and Bob agreed a single Pre-shared Key, let's call that ABA, which the Cat doesn't know, and they use TLS 1.3. 0. Bob feeds the cat before leaving for work 1. Alice wakes up, notices the Cat's food bowl is empty and sends an encrypted message to Bob, Encrypt(ABA, "Did you feed the cat?") 2. The Cat intercepts Alice's encrypted message and sends it back to her. The Cat can't read the message, nor tamper with it, but just sends it unaltered and trusts that will have the desired effect. 3. Alice receives an authentic message encrypted with the ABA key, which she presumes is from Bob, it says "Did you feed the cat?" 4. Alice sends an encrypted reply, Encrypt(ABA, "No") 5. The Cat intercepts this message too and sends it back to Alice again 6. Alice receives the reply, which she presumes is from Bob, it says "No". 7. Alice feeds the cat again. The cat has now been fed twice. Attack successful. How did this attack sneak part the proof? Well, the proof says Alice and Bob should agree two keys, an Alice->Bob key (let's calls this AB1) and a Bob->Alice keys (call it BA1). When Alice receives her own message encrypted with AB1, she can see she sent it, not Bob, and so she detects the Cat's attack. So the proof is fine. The person writing the proof assumed this is what was meant in the human readable document describing TLS 1.3, but the other humans working from this document assumed it would be fine for Alice and Bob to agree a single key ABA. It's certainly not highlighted in the original document that this is a concern and you must agree two keys. [ There are also lots of other things you could do, if you're careful and know about this attack, but for some reason can't just agree twice as many keys. However the correct basic design to explain in the document is to just make separate keys for each direction ]