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.
Network function developers need no verification expertise, and the verification process does not require their assistance.
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.
The entire software stack (framework, driver, OS) is verified, down to the hardware.
We developed five representative NFs:
and verified with Vigor that they satisfy standards-derived specifications, are memory-safe, and do not crash or hang.
We measure runtime performance on Intel Xeon E5email@example.com GHz machines with 10 Gbps NICs at 90% occupancy of the NF’s main data structure and compare it with performance of Click modular router based on DPDK kernel bypass framework. Only for the policer we couldn’t find off-the-shelf Click element so we use moonpol instead.
Vigor does not support batching, so all Vigor NFs process 1 packet at a time. However we measure performance of the default batching mode for the baseline NFs as well as their non-batching versions.
All NFs run on a single core.
This chart reports maximul throughput achievable with an NF before it starts dropping more than 0.1% of traffic, using the minimal size 64-byte packets.
Vigor NFs have competitive throughput with the non-batching baselines. The batching benefit shows here as about 2x better throughput on some NFs.
We believe that the Vigor NFs sustain sufficient throughput for most non-performance critical applications.
This is the average latency for the packets/frames that take the longest path through the NF, measured using hardware timestamps (here’s why).
Vigor NFs have minimal latency across all experiments, likely because of their monolithic structure. The monolithic structure poses no issue, since we verify correctness of the whole software stack.
Note, how batching always degrades the average latency due to the necessary delay of accumulating a batch.
Verifying Software Network Functions with No Verification Expertise. Arseniy Zaostrovnykh, Solal Pirelli, Rishabh Iyer, Matteo Rizzo, Luis Pedrosa, Katerina Argyraki, George Candea. ACM Symposium on Operating Systems Principles (SOSP), Ontario, Canada, Oct 2019
A Formally Verified NAT Stack. Solal Pirelli, Arseniy Zaostrovnykh, George Candea. ACM SIGCOMM Kernel Bypassing Networks workshop (KBNets), Budapest, Hungary, August 2018 (Best Paper Award) (talk video)
Vigor’s code and Vigor-based NFs are available on GitHub.
There are several ways you can help the project:
Arseniy Zaostrovnykh, Solal Pirelli, Rishabh Iyer, Matteo Rizzo, Luis Pedrosa, Katerina Argyraki, George Candea