RecordFlux: Formal Message Specification and Generation of Verifiable Binary Parsers
This addresses security issues in protocol implementations for software developers, offering a formal verification approach to prevent bugs, though it is incremental in applying formal methods to binary parsing.
The authors tackled the problem of vulnerabilities in binary protocol parsers by proposing a formal model and domain-specific language for specifying message formats, enabling the generation of verifiable parsers with proven absence of runtime errors, as demonstrated with examples like Ethernet and TLS.
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.