Network function developers want to prove the correctness of their code to operators without having to divulge their source code. They also must be able to use any data structure they want, not just choose from a small set of verified ones.

We present Klint, a tool implementing our new automated verification technique for network function binaries. Operators can use Klint on a binary to obtain correctness guarantees based on a specification, and developers can use any data structure as long as they provide contracts written in terms of maps. The data structures need not be verified, though it’s encouraged. They also do not have to be implemented in terms of maps, only described with maps.

Klint can verify the binaries of our network functions in a couple minutes. The resulting network functions are also faster than previous work because it is much easier to prototype new functions with new data structures.

Our code is publicly available:

Since the paper was published, we have verified additional network functions with the help of some talented undergrads. We currently have the following functions:

Name Description
Bridge Ethernet bridge with MAC learning
Firewall Firewall classifying flows based on IP + TCP/UDP
IPTables Filter that allows or denies packets based on custom rules, implemented by Elvric Trombert and Patrice Kast
Maglev Implementation of Google’s Maglev load balancer
NAT Dynamic Network Address Translator
Policer Traffic policer using token buckets. A version in Rust is also available.
Router IPv4 router using Longest-Prefix-Match.

Paper: Automated Verification of Network Function Binaries. Solal Pirelli, Akvilė Valentukonytė, Katerina Argyraki, George Candea. USENIX Symposium on Networked Systems Design and Implementation (NSDI), Renton, WA, April 2022 (talk video)