Software constantly needs to interact with its environment. It may read data from sensors, receive requests from other software  components or control hardware devices based on the calculations performed. While this interaction is what makes software useful in the first place, processing messages from untrusted sources inevitably creates an attack vector an adversary may use to exploit software vulnerabilities. The infamous Heartbleed is only one example where a security critical software was attacked by specially crafted messages.

Implementing those interfaces to the outside world in SPARK and proving the absence of runtime errors is a way to prevent such attacks. Unfortunately, manually implementing and proving message parsers is a tedious task which needs to be redone for every new protocol. In this article we'll discuss the challenges that arise when creating provable message parsers and present RecordFlux, a framework which greatly simplifies this task.

Specifying Binary Messages

Ethernet: A seemingly simple example

At a first glance, Ethernet has a simple structure: A 6 bytes destination field, a 6 bytes source field and a 2 bytes type field followed by the payload:

We could try to model an Ethernet frame as a simple record in SPARK:

When looking closer, we realize that this solution is a bit short-sighted. Firstly, defining the payload as a fixed-size array as above will either waste memory when handling a lot of small (say, 64 bytes) frames or be too short when handling jumbo frames which exceed 1500 bytes. More importantly, the Ethernet header is not as simple as we pretended earlier. Looking at the standard, we realize that the EtherType field actually has a more complicated semantics to allow different frame types to coexist on the same medium.

If the value of EtherType is greater or equal to 1536, then it contains an Ethernet II frame. The EtherType is treated as a type field which determines the protocol contained in Data. In that case, the Data field uses up the remainder of the Ethernet frame. If the value of EtherType is less or equal to 1500, then it contains a IEEE 802.3 frame and the EtherType field represents the length of the Data field. Frames with an EtherType value between 1501 and 1535 are considered invalid.

To make things even worse, both variants may contain an optional IEEE 802.1Q tag to identify the frames priority and VLAN. The tag is inserted after the source field and itself is comprised of two 16 bit fields, TPID and TCI. It is present if the bytes that would contain the TPID field have a hexadecimal value of 8100. Otherwise these bytes contain the EtherType field.

Lastly, the Data field will usually contain higher-level protocols. Which protocol is contained and how the payload is to be interpreted depends on the value of EtherType. With our naive approach above, we have to manually convert Data into the correct structured message format. Without tool support, this conversion will be another source of errors.

Formal Specification with RecordFlux

Next, we'll specify the Ethernet frame format using the RecordFlux domain specific language and demonstrate how the specification is used to create real-world parsers. RecordFlux, deliberately has a syntax similar to SPARK, but deviates where more expressiveness was required to specify complex message formats.

Packages and Types

Just like SPARK, entities are grouped into packages. By convention, a package contains one protocol like IPv4, UDP or TLS. A protocol will typically define many types and different message formats. Range types and modular types are identical to those found in SPARK. Just like in SPARK, entities can be qualified using aspects, e.g. to specify the size of a type using the Size aspect:

The first difference to SPARK is the message keyword which is similar to records, but has important differences to support the non-linear structure of messages. The equivalent of the naive Ethernet specification in RecordFlux syntax would be:

Graph Structure

As argued above, such a simple specification is insufficient to express the complex corner-cases found in Ethernet. Luckily, RecordFlux messages allow for expressing conditional, non-linear field layouts. While SPARK records are linear sequences of fixed-size fields, messages should rather be thought of as a graph of fields where the next field, its start position, its length and constraints imposed by the message format can be specified in terms of other message fields. To ensure that the parser generated by RecordFlux is deadlock-free and able to parse messages sequentially, conditionals must only reference preceding fields.

We can extend our simple example above to express the relation of the value of Type_Length and length of the payload field:

For a field, the optional then keyword defines the field to follow in the graph. If that keyword is missing, this defaults to the next field appearing in the message specification as in our Simplified_Frame example above. To have different fields follow under different conditions, an expression can be added using the if keyword. Furthermore, an aspect can be added using the with keyword, which can be used to conditionally alter properties like start or length of a field. If no succeeding field is specified for a condition, as for Type_Length in the range between 1501 and 1535, the message is considered invalid.

In the fragment above, we use the value of the field Type_Length as the length of the Data field if its value is less or equal to 1500 (IEEE 802.3 case). If Type_Length is greater or equal to 1536, we calculate the payload length by subtracting the end of the Type_Length field from the end of the message. The 'Last (and also 'First and 'Length) attribute is similar to the respective SPARK attribute, but refer to the bit position (or bit length) of a field within the message. The Message field is special and refers to the whole message being handled.

Optional Fields

The graph structure described above can also be used to handle optional fields, as for the IEEE 802.1Q tag in Ethernet. Let's have a look at the full Ethernet specification first:

Most concepts should look familiar by now. The null field used in the then expression of the Data field is just a way to state that the end of the message is expected. This way, we are able to express that the payload length must be between 46 and 1500. As there is only one then branch for payload (pointing to the end of the message), values outside this range will be considered invalid. This is the general pattern to express invariants that have to hold for a message.

How can this be used to model optional fields of a message? We just need to cleverly craft the conditions and overlay the following alternatives. The relevant section of the above Ethernet specification is the following:

Remember that the optional IEEE 802.1Q tag consisting of the TPID and TCI fields is present after the Source only if the bytes that would contain the TPID field are equal to a hexadecimal value of 8100. We introduce a field Type_Length_TPID only for the purpose of checking whether this is the case. To avoid any confusion when using the parser later, we will overlay this field with properly named fields. If Type_Length_TPID equals 16#8100# (SPARK-style numerals are supported in RecordFlux), we define the next field to be TPID and set its first bit to the 'First attribute of the Type_Length_TPID field. If Type_Length_TPID does not equal 16#8100#, the next field is Type_Length, skipping TPID and TCI.

As stated above, the specification actually is a graph with conditions on its edges. Here is an equivalent graph representation of the full Ethernet specification:

Working with RecordFlux

RecordFlux comes with the command line tool rflx which parses specification files, transforms them into an internal representation and subsequently generates SPARK packages that can be used to parse the specified messages:

To validate specification files, which conventionally have the file ending .rflx, run RecordFlux in check mode. Note, that RecordFlux does not support search paths at the moment and all files need to be passed on the command line:

Code Generation

Code is generated with the generate subcommand which expects a list of RecordFlux specifications and an output directory for the generated SPARK sources. Optionally, a root package can be specified for the generated code using the -p switch:

Usage

To use the generated code, we need to implement a simple main program. It allocates a buffer to hold the received Ethernet packet and initializes the parser context with the pointer to that buffer. After verifying the message and checking whether it has the correct format, its content can be processed by the application.

The code can be proven directly using gnatprove (the remaining warning is a known issue in GNAT Community 2019 as explained in the Known Issues section of the README):

What guarantees can we obtain from this proof? Firstly, the absence of runtime errors is shown for the generated code as well as for the user code. No matter what input is read into the Buffer variable and presented to the parser, the program does not raise an exception at runtime. Furthermore, its control flow cannot be circumvented e.g. by buffer overflows or integer overflows. This is called "silver level" in SPARK parlance. Additionally, we prove key integrity properties ("gold level"), e.g. that optional fields are accessed if and only if all requirements defined in the RecordFlux specification are met.

Case Studies

RecordFlux greatly eases the specification and handling of binary messages. But is it suitable for real-world applications? We conducted a number of case studies to validate that it in fact is.

Packet Sniffer

Packet sniffers are tools often used by administrators to diagnose network problems. They capture and dissect all data received on a network interface to allow for a structured analysis of packet content. Famous open source examples are Wireshark and tcpdump. As packet sniffers need to handle a large amount of complex protocols, they also tend to be complex. There have been errors which allowed attackers to mount remote exploits against packet sniffers. For this reason, e.g. it is discouraged to run Wireshark under a privileged user account.

Obviously a formally verified packet sniffer is desirable to eliminate the risk of an attack when analyzing traffic from untrusted sources. We prototyped a very simple packet sniffer for IP/UDP on Linux for which we proved the absence of runtime errors. The output is similar to other packet sniffers:

TLS 1.3

Another area where correct parsers are essential are security protocols. The most important security protocol on the internet is TLS - whenever a browser connects to a remote server using the https protocol, in the background some version of TLS is used. We formalized the message format of the latest TLS version 1.3 according to RFC 8446 and generated a SPARK parser for TLS from the specification.

An open question remained, though: Can the generated code handle real-world TLS traffic and is there a performance penalty compared to unverified implementations? While we are working on a verified component-based TLS 1.3 implementation completely done in SPARK, it is not yet available for this experiment. As an alternative, we used an open source TLS 1.3 library by Facebook named Fizz and replaced its TLS parser by our generated code. As the C++ types used by Fizz (e.g. vectors) could not easily be bound to Ada, glue code had to be written manually to translate between the C++ and the SPARK world. We ensured that all untrusted data the library comes in touch with is handled by SPARK code. For the SPARK part, we proved the absence of runtime errors and the invariants stated in the specification.

Our constructive approach turned out to be effective for improving the security of existing software. In CVE-2019-3560 an integer overflow was found in the Fizz library. Just by sending a short, specially crafted sequence of messages, an attacker could mount a Denial of Service attack against an application using Fizz by putting it into an infinite loop. While Facebook fixed this bug by using a bigger integer type, the RecordFlux parser prevents this issue by rejecting packets with invalid length fields.

Despite the required transformations, the performance overhead was surprisingly low. For the TLS handshake layer - the part that negotiates cryptographic keys when the communication starts - the throughput was 2.7% lower than for the original version. For the TLS record layer, which encrypts and decrypts packets when a connection is active, the throughput was only 1.1% lower:

Conclusion and Further Information

With RecordFlux, creating SPARK code that handles complex binary data has become a lot easier. With a proper specification the generated code can often be proven automatically. In the future, we will extend RecordFlux to support the generation of binary messages and the modeling of the dynamic behavior of binary protocols.

For more information see our research paper and the language reference. If you have comments, found a bug or have suggestions for enhancements, feel free to open an issue on GitHub or write an email.