Hardening attack surfaces with formally proven binary format parsers

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

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

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.

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

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!

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 ]