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: https://github.com/dslab-epfl/klint
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)