Crypto 2017 - How Microsoft Wants to Fix the Internet (Spoiler: Without Blockchains)

In the second invited talk at Crypto, Cédric Fournet from Microsoft Research presented the recent efforts of Project Everest (Everest VERified End-to-end Secure Transport), which seems an attempt to fix implementing TLS once and for all. Appropriately for such a gigantic task, more than a dozen researchers on three continents (and the UK) work on making it verifiable and efficient at the same time.

As with every self-respecting talk in the area, it started with the disaster porn that is the history of TLS (our lifes depend on it, but it's complicated, there have been 20 years of failures, insert your favourite attack here). However, the Crypto audience hardly needs preaching to (just a reminder that the work isn't done with a proof sketch; performance and error handling also matters), so the talk swiftly moved on to the proposed solutions.

The story starts in 2013 with miTLS, which was the first verified standard-compliant implementation. However, it still involved hand-written proofs and was more of an experimental platform. Enter Everest: They want to tick all the boxes by providing verified drop-in replacements for the HTTPS ecosystem. It covers the whole range from security definitions to code with good performance and side-channel protection.

As an example, Cédric presented Poly1305, a MAC that uses arithmetic modulo $2^{130}-5$ and forms part of the upcoming TLS 1.3 specification. Unsurprisingly, there have already been found bugs in OpenSSL's implementation. Project Everest have implemented Poly1305 with ~3,000 lines of code in Low*, a subset of F* (a functional language) that allows both C-style programming (with pointer arithmetic) as well as verification. Compiling this code with KreMLin (another output of Project Everest) results in machine code that is as fast as hand-written C implementations. The same holds for ChaCha2 and Curve25519.

However, hand-written assembly is still faster. The project aims to catch up on this with Vale, which was published at Usenix this year. Vale promises extensible, automated assembly verification and side-channel protection.

So what is the way forward? TLS 1.3 is on the horizon, bringing various improvements at the cost of a considerable re-design. This requires new implementations, and the project hopes to be first to market with an efficient and verifiable one.

For the rest of talk, Cédric gave more details on how F* naturally lends itself to security games, and how they proved concrete security bounds for the TLS 1.2 and 1.3 record ciphersuites.

All in all, I think it was a great example for an invited talk at Crypto, putting cryptography in a bigger context and bringing work that isn't necessarily on a cryptographer's radar to our attention.