1. 5

Published at Usenix Security 2019.

TL;DR generate formally verified C and F* implementations of parsers/serializers for arbitrary formats defined in a high-level RFC-like language or from F* directly.

Properties such as memory safety are guaranteed, and serializations are bijective with the accompanying parsers as their inverses.

Examples are provided: TLS, bitcoin blocks, ASN.1, …

  1.  

  2. 2

    This is some great work. One of my favorite things is how they also consider testing, interoperability, and performance. Many papers just do some proofs on one thing and call it a day. I especially like that they fuzzed it to test the verification was working. What I don’t like is that they only used SAGE. If possible, they should’ve tossed a few fuzzers at them with different strengths and weaknesses.