Vigor workflow

Verification of Software NFs with
No Verification Expertise

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.

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.

Case Studies

We developed five representative NFs:

and verified with Vigor that they satisfy standards-derived specifications, are memory-safe, and do not crash or hang.

Runtime Performance

We measure runtime performance on Intel Xeon E5-2667@3.30 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.

Throughput

Throughput barchart

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.

Latency

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.

Latency barchart

Publications

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)

A Formally Verified NAT. Arseniy Zaostrovnykh, Solal Pirelli, Luis Pedrosa, Katerina Argyraki, George Candea. ACM SIGCOMM Conference (SIGCOMM), Los Angeles, CA, August 2017

Getting the code

Vigor’s code and Vigor-based NFs are available on GitHub.

How Can I Contribute?

There are several ways you can help the project:

Related Projects

Vigor builds on top of KLEE symbolic execution engine and VeriFast theorem prover for C. Vigor has inspired the Bolt tool for reasoning about performance contracts.

Team

Arseniy Zaostrovnykh, Solal Pirelli, Rishabh Iyer, Matteo Rizzo, Luis Pedrosa, Katerina Argyraki, George Candea