Tobias Reiher

Security vulnerabilities are still very common in todays software. Formal methods could improve the situation, but program verification remains a complex and time-consuming task. Often, the verification of existing software is infeasible and a complete rewrite can be prohibitively expensive. Both, however, is not necessarily required to improve on the current state. By replacing critical parts of an existing software by verified code, security can be strengthened significantly with moderate effort.

We show the feasibility of this approach by the example of a FLOSS TLS implementation. The basis of our PoC is the TLS 1.3 library Fizz which is written in C++. The existing message parser was replaced by a verified version implemented in the SPARK language. Our RecordFlux toolset was used to automatically generate the parser based on a formal message specification. With the SPARK tools we can prove automatically that an attacker cannot cause any overflows, runtime errors or undefined state by sending malformed messages to the modified library. Because of mismatches in the data structures used in C++ and SPARK, some glue code had to be written manually to integrate the verified parser into Fizz. Still, the modified TLS implementation shows only a slight performance loss while providing higher security.

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.