Checking-in on Network Functions

TL;DR

This paper introduces a novel approach within the NetBricks framework for specifying and verifying static and dynamic checks in network function programming, simplifying dependency management without significant overhead.

Contribution

It presents a new method for integrating static checks and dynamic contracts into network function development, addressing runtime dependency invariants.

Findings

Enables specification of packet processing invariants

Simplifies dependency management during development

Maintains low overhead in network functions

Abstract

When programming network functions, changes within a packet tend to have consequences---side effects which must be accounted for by network programmers or administrators via arbitrary logic and an innate understanding of dependencies. Examples of this include updating checksums when a packet's contents has been modified or adjusting a payload length field of a IPv6 header if another header is added or updated within a packet. While static-typing captures interface specifications and how packet contents should behave, it does not enforce precise invariants around runtime dependencies like the examples above. Instead, during the design phase of network functions, programmers should be given an easier way to specify checks up front, all without having to account for and keep track of these consequences at each and every step during the development cycle. In keeping with this view, we present a unique approach for adding and generating both static checks and dynamic contracts for specifying and checking packet processing operations. We develop our technique within an existing framework called NetBricks and demonstrate how our approach simplifies and checks common dependent packet and header processing logic that other systems take for granted, all without adding much overhead during development.

Figures

Tables

Table 1. Table 1. Syntax additions for our MTU NF (unexpanded)

LoC run	lang	files	lines	code
mtu-too-big: Contracts ON	rust	2	214	183
mtu-too-big: Contracts OFF	rust	2	189	158
mtu-too-big: Contracts ON	toml	1	19	16
mtu-too-big: Contracts OFF	toml	1	16	13
mtu-too-big: Contracts ON	total	3	233	199
mtu-too-big: Contracts OFF	total	3	205	171
Change		0	+28	+28

Table 2. Table 2. Compile times running “cargo build” for extension header NF example and MTU NF example

compile times / cargo build	example	mean (s)	stddev (s)	user (s)	system (s)	min (s)	max (s)
Contracts - Off	srv6-change-pkt	26.039	3.286	0.631	10.715	22.330	33.230
Contracts - On	srv6-change-pkt	25.099	2.398	0.549	11.697	20.238	28.220
Effect		-0.94	-0.888	-0.082	+0.982	-2.092	-5.01
Contracts - Off	mtu-too-big	21.652	2.202	0.537	9.201	18.528	25.191
Contracts - On	mtu-too-big	26.052	1.858	0.650	10.851	22.165	28.346
Effect		+4.4	-0.344	+0.113	+1.65	+3.637	+3.155

Full text

network functions, design-by-contract, software verification

††journalyear: 2019††copyright: acmcopyright††conference: ANRW ’19: Applied Networking Research Workshop; July 22, 2019; Montreal, QC, Canada††booktitle: ANRW ’19: Applied Networking Research Workshop (ANRW ’19), July 22, 2019, Montreal, QC, Canada††price: 15.00††doi: 10.1145/3340301.3341131††isbn: 978-1-4503-6848-3/19/07††ccs: Networks Programming interfaces

1. Introduction

Writing network functions (NFs) today is as capable as ever, with numerous frameworks and domain-specific languages to choose from. Some target development ease, reusable abstractions, or a familiar programming model that is in vogue within software development at large, while others stress performance guarantees or deployment at scale. Irrespective of which framework or model is used, NFs tend to be comprised of code exercising arbitrary logic and domain knowledge that only network programmers or administrators would know, or should know.

Consider the payload length field of an IPv6 header, a field whose value is dependent upon the consequence of processing and manipulating the rest of the packet it’s a part of. If an extension header (Deering and Hinden, 1998) is added to or removed from the packet, or a layer 4 protocol’s payload is modified in any way, then this payload length field must be incremented or decremented accordingly. Other “middleboxes” downstream in the network will apply functionality based on the value held in this field—without calculating the length of the rest of the packet—or just drop the packet outright if it’s wrong. Handling this effect is often taken for granted, a piece of arbitrary logic that network programmers have to remember to apply and validate at different steps in a function pipeline or at egress. For example, in the still widely used (Dobrescu et al., 2009; Medhat et al., 2017; Kablan et al., 2015) packet processing system Click (Kohler et al., 2000), a CheckIP6Header module provides validation on the payload length field via:

⬇

if(ntohs(ip->ip6_plen) > (plen - |\colorbox{BurntOrange}{40}|))

|\colorbox{Apricot}{goto bad}|;

While this code does do a “check” on the field, it hard codes the value as part the conditional check instead of using a constant or variable to better express meaning (40 is the fixed size of an IPv6 header). Additionally, if the check is invalid, goto bad executes a jump, leaving very little in the way of failure handling and unambiguous messaging. Besides a few per-field validations within the element file, the module does not account for related changes downstream when composed with other modules or the possibility of extension headers or variable-length fields. The functionality expressed in this snippet need not be so unwieldy, as validations should be a first-class part of programmable network architecture.

In this paper, we present a novel approach that clearly describes and validates these arbitrary effects via the addition and generation of both static checks and dynamic, runtime contracts for specifying conditional dependencies in common packet processing actions. Our work makes use of three well-known programming paradigms.

Static Assertions and Types Our prototype is incorporated within a framework built using the Rust programming language, which emphasizes a strong, static type system with first-class polymorphism (Weiss, 2018) (parametric and ad-hoc). Headers within a packet are explicitly-typed, e.g. Ipv4Hdr or Ipv6Hdr for instance, and contain associated types (Developers, 2018) that define which header(s) can precede it, e.g. an IPv6 Header relies on an Ethernet header existing before it within a packet. We leverage the type system along with the concept of static assertions (Klarer et al., 2008) to provide compile-time checking for a subset of network function components, including constant checks at the call site of these functions and ensuring that packet order and definitions adhere to specification.

Design by Contract We take inspiration from D’s contract system (Foundation, 2018), whose design was inspired by contract schemes (Meyer, 1992) where contracts are provided and run during testing, debugging, and development stages—the design phase—but are usually omitted for release builds in order to maximize performance. In using this style of contracts, programmers are able to code, test, and simulate NF’s around pre (ingress) and post (egress) invariants, checking which conditions must hold as packets are transformed by functions. These contracts allow developers to identify the intentional consequences of their packet processing algorithms.

Code Generation Though contract programming aids in checking and asserting if specifications and dependencies between operations hold, these checks are only (recommended to be) provided during time of development or within testing environments. Additionally, we do not want developers to have to sprinkle contracts throughout their NFs or implement logic to traverse or backtrack from one header, payload, or set of bytes to another just for the sake of validation. Instead, our approach allows developers to specify a set of dependencies and conditions up front via macros (Kohlbecker and Wand, 1987), which in turn get translated into contracts.

We develop our technique as an extension to the NetBricks framework and programming model (Panda et al., 2016), illustrating the efficacy of our approach through two examples: 1) updating the IPv6 payload length of a packet in the context of changes to an extension header; and 2) transitioning an invalid TCP request (based on an MTU—Maximum Transmission Unit—threshold), into that of an ICMPv6 Packet Too Big response (Conta et al., 2006). We evaluate our prototype by examining syntax additions, compilation times, and possible runtime overheads. In Section 6, we discuss our examples within the context of a couple real-world implementations, Onos and Facebook network code, where our approach could be beneficial.

2. Motivation

Choosing between NF architectures and/or network programming languages has become a non-trivial process: What kind of programming paradigm should one choose for packet processing, e.g. functional, dataflow, or imperative? Should the framework support the OpenFlow protocol or be composed of its own data plane and control plane layers? What are the most important facets of the system or application: performance, usability and reconfiguration, reliability? There are many choices and abstractions to deliberate on, see sections 6 and 1, yet most only provide a subset of safety, design benefits, or degrees of freedom for which kinds of applications can be executed. We illustrate two specific challenges in defining a better way forward.

The Limits of Correctness

In the interest of handling correctness and ensuring network programs satisfy specification, there are several efforts which have experimented with verifying networking constructs. For example, a language like NetKat (Anderson et al., 2014), based on proven semantic and type theoretic foundations, provides static checking for reachability, guarantees non-interference between programs, and supports first-class primitives for the filtering, modifying, and transmitting of packets. However, though powerful, NetKat is limited in what logic it can check for and what protocols and actions it can support, as all programs must conform to the OpenFlow flow table—its compilation target. While OpenFlow is used in practice, its model is limited in terms of interface, protocol, and field support, especially for newer, experimental features. Due to this coupling with OpenFlow, along with a lack for handling arbitrary logic in packet processing, NetKat does not present a generalized solution.

Arbitrary Logic & Variable-length Data

As described in Section 1, many network programs contain operational logic that’s only applied based on the IETF or similar specifications they conform to. Some even define their own inspired-by protocols without a formalized spec (Jin et al., 2018). One major component of the IPv6 protocol specification that has been left unsupported by many NF frameworks is that of IPv6 extension headers. Traffic containing such a header is usually dropped in practice and considered a “threat to the Internet” (Hendriks et al., 2017). In skipping support for extension headers, packet-processing paradigms can avoid dealing with variable-length data—the specs of these headers contain fields with variable-byte-sized data—and complex header chaining dependencies, as these headers can be stacked upon each other to no end. However, as unique applications for programmable networks that make use of these extensions are constantly being explored (Desmouceaux et al., 2017), we must provide programmatic abstractions for adhering to the conditions of these protocols while also being amenable to new, experimental ones down the line whether they’re used in industry or proposed in research.

3. Kinds of Contracts

3.1. Design by Contract

The Eiffel programming language made design by contract first-class, focusing primarily on how runtime contracts can be turned on for monitoring and testing situations so that developers can “sit back, and just watch their contracts be violated” (Meyer, 2018). The key idea behind the approach is that elements of a software system collaborate with each other on the basis of mutual obligations and benefits, driven by dependencies and related components in the system. These contracts are usually separated into pre (input/ingress) and post conditions (output/egress), where invariants can be asserted on for incoming and outgoing data accordingly.

In our system, design by contract-styled assertions help programmers articulate what the values of fields in a header should be equal to, bound by, approximate to, or how these values may have shifted during packet transformation (e.g. swapping of MAC addresses). From a processing perspective, the input precondition runs when the packet enters a NF and the postcondition runs as the packet is exiting the function.

3.2. Static Assertions

Static assertions, popularized in the C, C++, and D languages, allow for compile-time assertions of statically defined expressions, e.g. constants, statics. Beyond just checking for specific values, static assertions can be used to enforce fields on struct types and check if a pointer’s underlying value is the same when coerced to another type. NF programs tend to be comprised of many constants referring to values derived from specifications. For example, the IPv6 minimum MTU value is $1280$ (Deering and Hinden, 1998), but is actually $1294$ in practice when the Ethernet header is included. Our approach can check this caveat statically at the call site where the NF is defined—not where it’s instantiated—via compile-time assertions in our prototype for constant checking. Additionally, thanks to conditional compilation (see 4.1 for more information), static assertions remain in release binaries.

3.3. Static Order-Persevering Headers

With our approach implemented in NetBricks, we were given a head start toward better validation mechanics with a strong, static type system and framework for programming NFs in a map-reduce fashion. To add packet headers in NetBricks, you define a struct with the appropriate fields, as you would do in C or P4 for example. All structs must implement a trait111Traits are used to define shared behavior in Rust, similar to interfaces in other languages (Developers, 2018). containing an associated type that is defined as PreviousHdr:

⬇

impl EndOffset for Ipv6Hdr {

|\colorbox{LimeGreen}{type PreviousHdr=EthHdr}|;

fn offset(&self) -> usize { 40 }

}

When parsing a packet within an NF, the order is guaranteed by the defined PreviousHdr. Given any other order (e.g. parsing an IPv6 header after a ICMPv6 header), the type checker will throw a compile-time error. In our prototype, we leverage this statically-defined order mechanism on headers (4) to ensure that incoming and outgoing packet header ordering is preserved according to encoded expectations.

4. Implementation

We have developed a prototype222Openly accessible as a branch on Github. that extends the NetBricks programming model via macro-based metaprogramming with very little additional syntax. Instead of having to manually incorporate or implement all of the contract methodologies described in section 3 throughout a NF code base, our contracts extension can be used gradually, i.e. on certain NFs and not others, as well as retroactively on existing NFs with just a few easy steps: (i.) import our check library into an NF module; then (ii.) identify an NF to validate, and mark it; and then (iii.) specify contracts at the beginning and end of a NF based on properties that the developer wants to uphold.

Once introduced, these contracts rewrite NFs to include mechanisms for storing runtime info (used for checking outgoing packets), generating validations, assertions, logging facilities, and flag checks for conditional compilation.

Initialization

As seen in Figure 4, the check attribute macro (surrounded by brackets) is responsible for three steps in the contract generation process. Firstly, it identifies that the developer wants this NF to be “checked,” which means it can be used gradually over time. Secondly, by designating that this function has contract-checking on, we are then able to parse specific keywords, i.e. pre, post, in the figure that we want to rewrite and generate assertions from. Lastly, it performs a series of initialization operations, including turning-on specialized logging facilities and lazily instantiating a runtime hashmap that’s used to store all the headers as part of the input packet to create a mirror of the contents of the packet entering the NF. Building this map allows us to store header information for tracing, analysis, and further checks throughout the processing lifecycle, all the while producing a series of iterative steps to parse through the packet header-by-header, based on the order specified by the code.

Macro Expansion

The generation of code from macros ingress_check! and egress_check! occurs prior to the NF program being subjected to Rust’s type-checker, i.e. occurring in a separate compilation step. Of note, the order key in both the pre and post assertions, specified by the developer, allows us to match on the header-order within the contents of the packet itself, as all parsing of headers requires explicit type annotations in NetBricks under the hood. If the expected order does not match up on either ingress or egress checks, a compile-time error is thrown (as per 3.3).