The migration from ASIC-based to software-based implementations of middleboxes has both benefits and drawbacks: while software provides shorter development cycles and flexibility to deploy network functionality on demand, it is presents reliability challenges because of bugs, unpredictable behavior, and security vulnerabilities.
This project focuses on the code that implements the core packet processing functionality of the middlebox, referred to as the “network function” (NF). We aim to develop NFs that are guaranteed to be semantically correct while offering competitive performance and preserving developer productivity.
Vigor is a software stack and toolchain for building and running software network middleboxes that are guaranteed to be correct, while preserving competitive performance and developer productivity.
Developers write the core of the middlebox — the network function (NF) — in C, on top of a standard packet-processing framework (DPDK), putting persistent state in data structures from Vigor’s library (libVig). The Vigor toolchain then automatically verifies that the resulting software stack correctly implements a specification, which is written in Python.
Vigor has three key properties:
- Push-button: Network function developers need no verification expertise, and the verification process does not require their assistance.
- Pay-as-you-go: Verification can be done in a pay-as-you-go manner, i.e., instead of investing upfront a lot of time in writing and verifying a complete specification, one can specify one-off properties in a few lines of Python and verify them without concern for the rest.
- Full-stack: The entire software stack (framework, driver, OS) is verified, down to the hardware.
We developed several representative NFs (NAT, Maglev load balancer, MAC-learning bridge, stateful firewall, traffic policer, etc.) and verified with Vigor that they satisfy standards-derived specifications, are memory-safe, and do not crash or hang. Verifying them took minutes to hours, depending on whether we verified only the NF or the entire software stack. In our experiments, the verified NFs performed on par with standard, functionally equivalent, non-verified NFs.
Please see https://vigor-nf.github.io for further details.