Vigor: Developing Formally Verified Software Middleboxes

Poster.png: 2383x3370, 682k (November 02, 2019, at 04:43 PM)
Vigor Poster

We present the design and implementation of Vigor, a software stack and toolchain for building and running software middleboxes that are guaranteed to be correct, while providing competitive performance and preserving developer productivity. With Vigor, developers write the middlebox code (i.e., the software network function, or NF) in C atop a standard packet-processing framework, putting persistent state in data structures from a Vigor-provided library. Vigor then automatically verifies that the resulting software stack correctly implements a specification (written in Python).

Vigor extends prior work where we formally verified a NAT, but adds three points of novelty:

  1. NF developers need no verification expertise, and the verification process does not require their assistance (push-button verification).
  2. The entire software stack is verified, down to the hardware (full-stack verification).
  3. 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.

We present five NFs written using Vigor - a NAT, a Maglev load balancer, a learning bridge, a firewall, and a traffic policer - that are guaranteed to satisfy standard RFC-derived specifications, be memory-safe, and not crash or hang. We show that they provide competitive performance.

Further Reading

Arseniy Zaostrovnykh, Solal Pirelli, Rishabh Iyer, Matteo Rizzo, Luis Pedrosa, Katerina Argyraki, and George Candea; Verifying Software Network Functions with No Verification Expertise. In 27th ACM Symposium on Operating Systems Principles (SOSP'19). 2019
Open Website Download PDF Document More Information

Getting the Source

The Vigor source code is hosted on GitHub. To create a local copy of the repository run: 

git clone https://github.com/vigor-nf/vigor.git

Artifacts Available: this badge indicates that author-created artifacts relevant to this paper have been placed on a publicly accessible archival repository. Artifacts Evaluated - Functional: this badge indicates that the artifacts associated with the research are found to be documented, consistent, complete, exercisable, and include appropriate evidence of verification and validation. Results Replicated: The main results of the paper have been obtained in a subsequent study by a person or team other than the authors, using, in part, artifacts provided by the author.

People

  • Arseniy Zaostrovnykh (EPFL)
  • Solal Pirelli (EPFL)
  • Rishabh Iyer (EPFL)
  • Matteo Rizzo (EPFL)
  • Luis Pedrosa (EPFL)
  • Katerina Argyraki (EPFL)
  • George Candea (EPFL)