AdaCore Blog

RecordFlux: From Message Specifications to SPARK Code

by Alexander Senier

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:

Simplified Ethernet frame layout

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

package Ethernet is

   type Byte is mod 2**8;
   type Address is mod 2**48;
   type Type_Length is mod 2**16;
   type Payload is array (1..1500) of Byte;

   type Ethernet_Frame is
   record
      Destination : Address;
      Source      : Address;
      EtherType   : Type_Length;
      Data        : Payload;
   end record;

end Ethernet;

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:

package Ethernet is

   type Address is mod 2**48;
   type Type_Length is range 46 .. 2**16 - 1 with Size => 16;
   type TPID is range 16#8100# .. 16#8100# with Size => 16;
   type TCI is mod 2**16;

end Ethernet;

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:

type Simplified_Frame is
   message
      Destination : Address;
      Source      : Address;
      Type_Length : Type_Length;
      Data        : Payload;
   end message;

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:

   ...
   Type_Length : Type_Length
      then Data
         with Length => Type_Length * 8
         if Type_Length <= 1500,
      then Data
         with Length => Message’Last - Type_Length’Last
         if Type_Length >= 1536;
   ...

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:

package Ethernet is
   type Address is mod 2**48;
   type Type_Length is range 46 .. 2**16 - 1 with Size => 16;
   type TPID is range 16#8100# .. 16#8100# with Size => 16;
   type TCI is mod 2**16;

   type Frame is
      message
         Destination : Address;
         Source : Address;
         Type_Length_TPID : Type_Length
            then TPID
               with First => Type_Length_TPID’First
               if Type_Length_TPID = 16#8100#,
            then Type_Length
               with First => Type_Length_TPID’First
               if Type_Length_TPID /= 16#8100#;
         TPID : TPID;
         TCI : TCI;
         Type_Length : Type_Length
            then Data
               with Length => Type_Length * 8
               if Type_Length <= 1500,
            then Data
               with Length => Message’Last - Type_Length’Last
               if Type_Length >= 1536;
         Data : Payload
            then null
            if Data’Length / 8 >= 46
               and Data’Length / 8 <= 1500;
      end message;
end Ethernet;

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:

   ...
   Source : Address;
   Type_Length_TPID : Type_Length
      then TPID
         with First => Type_Length_TPID’First
         if Type_Length_TPID = 16#8100#,
      then Type_Length
         with First => Type_Length_TPID’First
         if Type_Length_TPID /= 16#8100#;
   TPID : TPID;
   TCI : TCI;
   Type_Length : Type_Length
   ...

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:

Graph representation of Ethernet spec

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:

$ rflx check ethernet.rflx
Parsing ethernet.rflx... OK

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:

$ rflx generate -p Example ethernet.rflx outdir
Parsing ethernet.rflx... OK
Generating... OK
Created outdir/example-ethernet.ads
Created outdir/example-ethernet-generic_frame.ads
Created outdir/example-ethernet-generic_frame.adb
Created outdir/example-ethernet-frame.ads
Created outdir/example-types.ads
Created outdir/example-types.adb
Created outdir/example-message_sequence.ads
Created outdir/example-message_sequence.adb
Created outdir/example-scalar_sequence.ads
Created outdir/example-scalar_sequence.adb

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.

with Ada.Text_IO; use Ada.Text_IO;
with Example.Ethernet.Frame;
with Example.Types;

procedure Ethernet
is
   package Eth renames Example.Ethernet.Frame;
   subtype Packet is Example.Types.Bytes (1 .. 1500);
   Buffer : Example.Types.Bytes_Ptr := new Packet'(Packet'Range => 0);
   Ctx    : Eth.Context := Eth.Create;
begin
   -- Retrieve the packet
   Buffer (1 .. 56) :=
      (16#ff#, 16#ff#, 16#ff#, 16#ff#, 16#ff#, 16#ff#, 16#04#, 16#d3#,
       16#b0#, 16#ab#, 16#f9#, 16#31#, 16#08#, 16#06#, 16#00#, 16#01#,
       16#08#, 16#00#, 16#06#, 16#04#, 16#00#, 16#01#, 16#04#, 16#d3#,
       16#b0#, 16#9c#, 16#79#, 16#53#, 16#ac#, 16#12#, 16#fe#, 16#b5#,
       16#00#, 16#00#, 16#00#, 16#00#, 16#00#, 16#00#, 16#ac#, 16#12#,
       16#64#, 16#6d#, 16#00#, 16#00#, 16#00#, 16#00#, 16#00#, 16#00#,
       16#00#, 16#00#, 16#00#, 16#00#, 16#00#, 16#00#, 16#00#, 16#00#);

   Eth.Initialize (Ctx, Buffer);
   Eth.Verify_Message (Ctx);
   if Eth.Structural_Valid_Message (Ctx) then
      Put_Line ("Source: " & Eth.Get_Source (Ctx)'Img);
      if Eth.Present (Ctx, Eth.F_TCI) and then Eth.Valid (Ctx, Eth.F_TCI)
      then
         Put_Line ("TCI: " & Eth.Get_TCI (Ctx)'Img);
      end if;
   end if;
end Ethernet;

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):

$ gnatprove -P ethernet.gpr
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
ethernet.adb:22:25: warning: unused assignment to "Buffer"
gnatprove: error during flow analysis and proof

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:

$ sudo ./obj/sniff_udp_in_ip

IP: Version: 4 IHL: 5 DSCP: 0 ECN: 0 TLen: 53 Id: 9059 DF: 1 MF: 0
FOff: 0 TTL: 64 Proto: UDP HCSum: 6483 Src: 127.0.0.1 Dst: 127.0.0.1,
UDP: SPort: 58423 DPort: 53 Len: 33 CSum: 65076 Payload: b9 7d 01
00 00 01 00 00 00 00 00 00 04 63 6f 61 70 02 6d 65 00 00 1c 00 01

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:

Performance impact for the handshake layer
Performance impact for the record layer

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.

Posted in #Formal Verification    #Formal Methods    #SPARK   

About Alexander Senier

Alexander Senier is founder and CEO of Componolit, a company dedicated to the development of highly trustworthy systems. Since he started programming, he has been looking for concepts, tools and technologies to develop better software. Consequently, he is a strong advocate of component-based architectures and has used SPARK as his preferred language for more than a decade. Componolit produces open source libraries and tools for building security-critical components and provides consulting to customers in the areas of high security, mobile security and industrial IoT.