Skip to content

Latest commit

 

History

History
181 lines (128 loc) · 6.14 KB

index.md

File metadata and controls

181 lines (128 loc) · 6.14 KB
Raw
layout title
default
Vigor: Verification of Software Network Functions with No Verification Expertise

{::options parse_block_html="true" /}

![Vigor workflow](images/vigor-workflow.png){: width="100%"}

{: #overview .text-center}

Verification of Software NFs with
No Verification Expertise

{: .lead} 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.

{: .text-justify} Developers write the core of the middlebox — the network function (NF) — in C, on top of a standard packet-processing framework ([DPDK](https://www.dpdk.org)), 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.

{::options parse_block_html="true" /}

{: .text-center}

Push-button

{: .text-justify} Network function developers need no verification expertise, and the verification process does not require their assistance.

{: .text-center}

Pay-as-you-go

{: .text-justify} 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.

{: .text-center}

Full-stack

{: .text-justify} The entire software stack (framework, driver, OS) is verified, down to the hardware.

{: .text-center}

Case Studies

{: .text-justify} We developed five representative NFs:

  • a NAT,
  • a Maglev load balancer,
  • a MAC-learning bridge,
  • a stateful firewall, and
  • a traffic policer,

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

{: .text-center}

Runtime Performance

{::options parse_block_html="true" /}

{: .text-justify} 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](images/throughput-barchart.png){: width="100%"}

{: .text-justify} 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.

{: .text-justify}
Latency

{: .text-justify} 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](images/latency-barchart.png){: width="100%"}

{: #publications .text-center}

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{:.underline}) (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

{: #thecode .text-center}

Getting the code

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

{: #contributing .text-center}

How Can I Contribute?

There are several ways you can help the project:

  • Use Vigor to develop and verify another network function
  • Extend libVig with a new efficient and verified component, useful for network functions, such as a regular expression matcher or cryptographic primitive.

{: #related .text-center}

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 .text-center}

Team

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