Many security problems have been discovered in communication protocols in the past, examples are:

• BlueBorne, a set of security vulnerabilities in the Bluetooth implementation which affect millions of devices
• Heartbleed, a security bug in the OpenSSL library that lead to exposure of sensitive data
• CVE-2018-10933, a critical bug in libssh which allows successful authentication without any credentials

Still today many critical issues remain in protocol implementations, as their root causes have not been addressed. Two classes of faults dominate: runtime errors like buffer overflows, and logic errors in protocol state machines. The main reasons for runtime errors is the use of unsafe programming languages. Better alternatives with formal guarantees like Rust, SPARK or Frama-C exist, but re-implementing complex protocols means a lot of effort. Logic errors are caused by the complexity of protocols and imprecise specifications in natural language.

RecordFlux is a framework for the secure implementation of communication protocols. From a formal protocol specification written in a domain-specific language the tools generate SPARK code, for which the absence of runtime errors can be proven automatically. In the future RecordFlux will also allow the specification of dynamic protocol semantics and support formal correctness proofs for protocol state machines. In this talk we give an overview of the current state and speak about an upcoming project that uses RecordFlux for a complex real-world application, the compartmentalized implementation of TLS 1.3 for component-based operating systems.