RecordFlux: Formal Message Specification and Generation of Verifiable Binary Parsers

TL;DR

This paper introduces RecordFlux, a formal language and method for specifying binary message formats, enabling the automatic generation of verifiable parsers that are free of runtime errors and suitable for complex protocols like Ethernet and TLS.

Contribution

It presents a novel domain-specific language for formal message specification, including invariants and cross-layer relations, and a technique to generate verifiable, error-free parsers from these specifications.

Findings

Successfully specified Ethernet and TLS message formats.

Generated parsers are verified to be free of runtime errors.

The approach improves security by reducing parser vulnerabilities.

Abstract

Various vulnerabilities have been found in message parsers of protocol implementations in the past. Even highly sensitive software components like TLS libraries are affected regularly. Resulting issues range from denial-of-service attacks to the extraction of sensitive information. The complexity of protocols and imprecise specifications in natural language are the core reasons for subtle bugs in implementations, which are hard to find. The lack of precise specifications impedes formal verification. In this paper, we propose a model and a corresponding domain-specific language to formally specify message formats of existing real-world binary protocols. A unique feature of the model is the capability to define invariants, which specify relations and dependencies between message fields. Furthermore, the model allows defining the relation of messages between different protocol layers and thus ensures correct interpretation of payload data. We present a technique to derive verifiable parsers based on the model, generate efficient code for their implementation, and automatically prove the absence of runtime errors. Examples of parser specifications for Ethernet and TLS demonstrate the applicability of our approach.