# 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.

## Key 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.