Packet generation is an important activity for network administration and security. Tools for packet generation work through template instantiation and are used in an imperative programming style. We describe a new design for a declarative packet generator that a ords users rich expressiveness to describe the packets they wish to generate. This relies on a domain-speci c language for describing packets and constraints over them. This is translated into bitvector constraints that are dispatched to an SMT solver. The resulting bitvector solutions are then concatenated and composed into the di erent layers of the network protocol stack, and can be sent over the network interface. In this paper we describe a library implementation of this approach, and evaluate its extensibility and scalability.
only be tested on `well-formed' network tra c|since Ethernet frames with incorrect checksums are usually silently dropped by the network interface.
By making such knowledge and assumptions explicit, we obtain a form of expression that can be used to generate packets. For the Ethernet part of a query, one would formulate: 48 48 16 P 32 frame = src add dst add ethtype pload fcs ( ) src add = 00 * * * * * ethtype = 08 00
fcs = crc32(src add; dst add; ethtype; pload)
In this notation, symbols like frame and src add stand for constants| xed but possibly unknown values. These values consist of bitstrings, the size of which is xed. For example, src add is 48 bits wide. It is not currently clear what the width of pload is, therefore its length value is represented by the variable P , which we italicise to indicate that it is a variable. crc32 is a special function that computes the frame's checksum.
We follow the structure of Ethernet frames;3 frame denotes the bitstring that comprises the whole frame, formed from the concatenation of the following substrings: src add (source address), dst add (destination address), ethtype (type of protocol encapsulated in the payload), pload (the payload bitstring) and fcs (frame check sequence|i.e., checksum value).
The equations given above constrain the value of frame, and of its substrings src add, ethtype, and fcs. Literals are shown in grey boxes|containing bytes in hexadecimal notation, in this example. An ethtype of 0800 indicates that an Ethernet frame encapsulates an IPv4 packet. Wildcards are indicated using asterixes, and by breaking out of the grey box back into a white background to indicate that wildcards are interpreted by the meta-language rather than the object-language. Thus, the source address constraint above speci es that it must start with a 0 byte, followed by any byte values.
The example given above is simple, but formulating and solving such problems can be di cult. Packet formats sometimes contain dependencies within packets, and even across di erent sorts of encapsulated packets. Generating such bitvector constraints is ripe for automation.
We noticed that packet encapsulation|that is, carrying packets of one protocol inside another, such as IPv4 over Ethernet|can be exploited to break up constraint problems into smaller problems that can be solved separately. For instance, in the problem described above on IP broadcast or multicast, we would rst solve the IP-related constraints to produce a candidate IP packet bitstring, let's equate it with the constant ip soln. We then use this to constrain the solution of the Ethernet frame in equation ( ) by asserting pload = ip soln. This gradual, inside-out generation of a frame is more tractable than attempting to immediately generate a bitstring for the entire Ethernet frame. (Standard frames can be around 1500 bytes long, or 12Kbits.) Later we describe an example of a stack of encapsulations that is six protocols deep. Contributions. We describe the rst application of SMT solvers to the problem of network tra c generation, and produce a more declarative interface to packet generation. For improved performance we exploit the layer-based abstractions used in network protocols to reduce the complexity of constraint-solving. We implement this method as a .NET library, and example F# code of its use can be seen in Figure 1. We evaluate our system using a non-trivial packet generation example, and make both code and data available online.4 3https://en.wikipedia.org/wiki/Ethernet_frame 4http://www.cl.cam.ac.uk/~ns441/kneecap/
We provide background and describe related work in the next section. In x3 we describe our model for packets and constraints, and in x4 our overall architecture and translation into bitvector formulas. We describe and evaluate our implementation in x5. 2
Tra c generation. A packet format describes a scheme or template that all packets in that
protocol must instantiate. All the packet generation tools that we are aware of are based on
instantiating templates, and their interface allows you to pick a packet type (say, DNS) and
specify the values of its elds. These tools range from software-only tools such as iperf, netsni
ng5, hping6, and Scapy7 to packet generators on specialised hardware [
5http://netsniff-ng.org/ 6http://www.hping.org/ 7http://www.secdev.org/projects/scapy/ 8The pcap le format is described at: https://wiki.wireshark.org/Development/LibpcapFileFormat
Often, additional constraints need to be satis ed in order for the tra c to be well-formed. For example, the checksum and length elds must contain the correct values.
Most existing tools implicitly model the packet as a scheme. Our system's main advantage is that it can handle arbitrary logical constraints between elds and values, and it allows a fully declarative style of expression (in terms of equations and inequations, and using standard arithmetic and Boolean operators). All other systems follow an imperative style of packet generation, where for-loops are used to test and set eld values of individual packets, to encode inter-layer constraints.
Bitvector formulas. Packet formats are described at the bit and byte level. Fixed-width bitvectors are among the theories supported by SMT solvers. The solutions found by SMT solvers can almost be sent directly onto the network, save for any reordering of bytes that the packet format might require.
Bitvector expressions consist of bits, strings of bits, their concatenation, and arithmetical
and logical operations over them|such as addition, shifting, etc. Bitvector formulas consist
of atoms asserting equality or inequality between bitvector expressions, and the usual logical
formation rules over them (such as negation). The precise details are not important here, and
a more detailed explanation is given by Kroening and Strichman [
Using existing packet-generation tools, we can generate packets by instantiating templates using directives such as src port = 22 and 17 < src port 22. Using the model-based approach described in this paper we can express more complex constraints relative to di erent elds across protocol layers, such as (p:src port = 22) _ (p:src port < (2 q:dst port)) where p and q are transport protocols at di erent layers. Using the design described in the next section, a user could express arbitrary constraints over a stack of encapsulated protocols. 3
In this section we describe the information communicated by a packet speci cation, which we will use to generate instances of that packet. Then in the next section we describe how we use an SMT solver to generate the packet.
A packet speci cation communicates three bits of information: (i) the packet formats involved, (ii) how the instances of di erent packet formats should be encapsulated, (iii) constraints within packets, or across encapsulated packets. Figure 2 illustrates these di erent sorts of constraints. 3.1
Our goal is to generate network tra c by exploiting the expressiveness and automation enabled by current SMT technology. More speci cally, we aim to provide a language that allows: 1. encapsulation of any packets inside payload-carrying packets;9 2. constraints on all packet elds; 3. constraints relating di erent elds in a packet; 4. constraints relating elds in di erent packets (which are related by encapsulation); 5. extension to support new packet formats (for instance, to support a modi ed form of TCP in a datacentre).
We later relaxed requirement 2 since constraints over \computational" elds (such as a checksum) do not make much practical sense, as described in x4.1.1. Consequently we also relaxed requirements 3 and 4 for such elds. 3.2
Conceptually, we aim to combine the expressive language that can be processed by SMT solvers, with a generic description of protocol interfaces. Constraints on packets consist of bitvector formulas over a signature that is extended to interpret protocol-related elds and their values. We now elaborate how these concepts are extracted from protocol speci cations, and how they are made available in our language.
A packet format is the de ning description of a packet, specifying its elds, their widths,
their dependencies on other elds, how bytes are ordered, and so forth. This information is
typically extracted from RFCs.10 Packet formats are usually simple, to facilitate parsing at
high speeds by network elements or end-hosts. Despite being simple, packet formats are highly
diverse. It is di cult to have a complete yet constrained language for describing packet formats,
and research on this is ongoing [
From a packet format we extract what we refer to as the packet interface. This speci es the vocabulary to refer to parts of the packet|the names of elds|or its values|legal contents of a eld. The interface largely consists of a presentation of the packet format to the user of our domain-speci c language. It speci es precisely what symbols can be used in constraints, and what they mean to the packet's description. There are three types of symbols: elds are names of elds, such as `ethertype' on line 6 in Figure 1; constants are more meaningful symbols for numeric values, such as `ethertype ipv4' for 08 00 ; protocol-speci c functions interpret values supplied by the user, into bitvectors. For instance, they parse notations such as \192.168.1.1" and \192.168.1.0/30". The meaning of these notations is local to a single packet format.
Note that the packet format speci es how elds are concatenated to form a packet, while the packet interface is not concerned with this. The interface describes the protocol-speci c meaning of elds, constants and protocol-speci c functions.
9Ethernet and IPv4 are examples of payload-carrying protocols, whereas ARP does not carry a payload. 10http://www.ietf.org/rfc.html
For example, the header formats for Ethernet, IPv4, and IPv6 have elds for a `source address', but they di er in the width and representation of what they each mean by `source address'. The packet interface allows us to resolve precisely what we mean when we speak of a `source address' in the context of a particular protocol.
The atoms making up the packet interface are combined through logical connectives and arithmetical operators to form constraints over packets. Unlike the symbols in a packet interface, the meaning of logical connectives and arithmetical operators is the same across all packets.
Using the vocabulary described above, we can form constraints over packets' elds, and thus over packets. Unconstrained elds can, by default, be assigned any value by the solver|unless we implicitly constrain the model to generate only well-formed tra c, as described in x4.1.2.
If the constraints are too strong, then it may be that there is no solution to constraints|this did arise during testing, when we mistakenly constrained a packet's eld to be equal to two distinct values. 4
We now turn to how the speci cation described in the previous section is translated into bitvector constraints and passed to a back-end solver. Recall that a speci cation may reference other packet speci cations when one packet encapsulates another.
Figure 3 outlines our architecture, which serves to translate high-level packet constraints into bitvector constraints for each protocol layer. The constraints of successive layers are solved, and the solutions are used to constrain the generation of lower-layer packets. Thus, we generate a packet gradually by taking advantage of how protocols are layered to form a stack, rather than generate a full outer-level packet at one go.
l o o t d n e t n o r F
The translation of user-supplied speci cations, such as that in Figure 1, is syntax directed
and covers the classes of syntax described in x3.2: theory (arithmetical and logical) constants
(such as conjunction, &&), protocol-speci c constants (such as ethernet.ethertype_ipv4), and
protocol-speci c functions (e.g., ethernet.mac_address "[
For example, lines 4-6 of Figure 1 are translated into the following bitvector problem when
written in SMT-LIB syntax:
(let ((a!1 (concat (concat (concat (concat range0 #x34) #x56) #x78) #x90)))
(let ((a!2 (= src_mac (concat a!1 wild1)))))
(and (= ethertype #x0800)
a!2
(or (= range0 #x0a)
(= range0 #x01)
(= range0 #x02)
(= range0 #x03)
(= range0 #x04)
(= range0 #x05))
)))
The symbol src_mac is a distinguished constant that is mapped from ethernet.source_address.
range0 and wild1 are fresh constants generated by the ethernet.mac_address
protocolspeci c function: range0 is constrained to the values in f1; 2; 3; 4; 5; 10g (following \[
Packet constraints can make reference to elds in other layers. We found it useful to limit the kinds of references that can be made, as follows: a packet's constraints may only refer to elds in encapsulated packets, not vice versa. This ts our model, drawn in Figure 3, in which solutions ow downwards in the packet stack: a solution at one layer becomes part of a solution at lower network layers. For example, in Figure 2, A's constraints may refer to the elds of B and C, but C's constraints may not refer to any other layer's elds.
Other than the careful handling of names, the translation to bitvector formulas is straightforward, since the target (bitvector constraint) language can directly interpret the operators used in our source language|such as addition, shift, negation, etc. Our implementation includes a straightforward analysis to compute any necessary extensions that are needed to bitvectors. For instance, in order to compare two values they must be of the same bit width; this is a matter of zero-extending the smaller one to be the same size as the other. The user is spared having to specify mundane details.
11The o cial list of values can be obtained from: http://standards-oui.ieee.org/ethertype/eth.txt We came across two computations that need to be frequently executed. The rst is checksum computation, and the second is byte-order transformation. We decided to exclude such computations from constraints.
In principle, checksums could be computed by the solver. We encoded the checksum algorithms used by IPv4 and by Ethernet. The rst is simple, and its data is small, consisting only of the IP header. In contrast, the CRC32 algorithm to compute the Ethernet checksum is much more complex, and its data consists of the entire Ethernet frame. We found that the CRC32 computation to be impossibly slow when done using the solver, even for relatively small frames. We therefore decided that this computation should occur outside the solver, after the solver has produced values for other elds. This means that users will not be able to specify constraints over checksum values, but it seems very unlikely they would need to.
Depending on the endianness of the host's architecture, it can happen that the multi-byte values generated by the solver need to be reversed before writing them to a pcap le or sending them over the network. Modifying the byte order could be done using the solver, but since it is not a search problem, it seems best to do this outside the solver to avoid incurring overhead. We identi ed four basic modes of operation for a packet generation tool. Each mode relates to di erent intended uses for the generated tra c, and involves strengthening the constraints supplied by the user through additional constraints.
1. In manual mode the user can specify any constraint. They may also specify checksum values since the checksum algorithm is not run in this mode. Byte-reordering is done however, otherwise the packets' contents would not be interpreted correctly by the receiving end. In this mode, the user may deliberately generate invalid instantiations, for example, by using an IPv4 template and setting the version eld to the value 3. 2. Checksum-supported mode is like manual mode, except that the checksum is computed for the solution obtained from the solver. This follows the description in x4.1.1. 3. Locally well-formed mode speci es that, in addition to having a valid checksum, for a packet to be well-formed its elds need to have values from a valid range for values. For instance, in IPv4 the `version' must be 4, the `Internet header length' eld's value must not be less than 5, and the `total length' eld must contain the correct value. 4. Fully well-formed mode additionally involves asserting inter-layer consistency. For example, encapsulating IPv4 in Ethernet will restrict the latter's range of ethertype values to precisely a single one: that for IPv4.
In manual mode the system does not provide any support. A packet generator operating in this mode could be used by another tool that might make its own processing. In other modes, the generator adds progressively stronger background constraints to those supplied by the user. 5
We implemented the method described in the paper in a library called Kneecap. This was
implemented in F# and uses Z3 as the backend solver [
Our implementation has the following limitations: currently only xed-sized packets may be generated|generating variable-sized packets is future work; and the system only works in manual mode, described in x4.1.2.
The library contains supporting functions to generate a number of packets, and write them to a pcap le, which can then be played out on a network interface using a tool like tcpreplay12 or examined using a tool like Wireshark.13 5.1
Encapsulation. We experimented with stacking di erent packets; for ease of expression we will refer to a given con guration of a stack of packets as a stacket. Our most complex stacket consisted of the following packets, in order: Ethernet, IPv4, IPv4, EtherIP, Ethernet, ARP. Each of these were assigned constraints. Those for the rst two layers are exactly those shown in the snippet in Figure 1, and those for the remaining layers are shown in x5.2. We then generated a pcap le for distinct sequences of this stacket, and checked that the les were readable by Wireshark.
Performance. We anticipate that our packet-generation method will be used o ine, and therefore its rate of generation is not a likely concern, but we sought to measure this nonetheless. We evaluated Kneecap in a Windows 8.1 VM with 8GB RAM running on a 2GHz Core i7 MacBook Pro with 16GB RAM and SSD secondary storage. We generated 1000 64-byte unique Ethernet frames four times, and found that the average time was 18.99ms. We then generated 1000 unique 584-byte Ethernet frames four times, and saw that the average time was 609.1ms. Carrying out a larger range of tests outside a VM is future work. 5.2
In x5.1 we used a speci cation involving a stack of six protocols. This stack is speci ed in this section. The stack builds on the \ip" instance de ned in line 2 of Figure 1 (and further constrained between lines 7 and 15 of the same gure). The extended speci cation is shown below.
ip +== [(new ipv4(150u)).constrain <@ ipv4.version = 4 && ipv4.source_address = ipv4.ipv4_address "192.168.4.[55-60]" && ipv4.destination_address =
ipv4.ipv4_address "194.100.[
Acknowledgements. We thank Markulf Kohlweiss, Carles Gomez Montenegro, Robert Soule, Daniel Thomas, Christoph Wintersteiger, and the anonymous reviewers for helpful feedback.