Correct by Construction Networks Using Stepwise Refinement

Authors: 
Leonid Ryzhyk, VMware Research; Nikolaj Bjørner, Microsoft Research; Marco Canini, King Abdullah University of Science and Technology (KAUST ); Jean-Baptiste Jeannin, Samsung Research America; Cole Schlesinger, Barefoot Networks; Douglas B. Terry, Amazon; George Varghese, University of California, Los Angeles
Abstract: 

Building software-defined network controllers is an exercise in software development and, as such, likely to introduce bugs. We present Cocoon, a framework for SDN development that facilitates both the design and verification of complex networks using stepwise refinement to move from a high-level specification to the final network implementation.

A Cocoon user specifies intermediate design levels in a hierarchical design process that delineates the modularity in complicated network forwarding and makes verification extremely efficient. For example, an enterprise network, equipped with VLANs, ACLs, and Level 2 and Level 3 Routing, can be decomposed cleanly into abstractions for each mechanism, and the resulting stepwise verification is over 200x faster than verifying the final implementation. Cocoon further separates static network design from its dynamically changing configuration. The former is verified at design time, while the latter is checked at run time using statically defined invariants. We present six different SDN use cases including B4 and F10. Our performance evaluation demonstrates that Cocoon is not only faster than existing verification tools but can also find many bugs statically before the network design has been fully specified.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

Presentation Video

Download Video

Presentation Audio

BibTeX
@inproceedings {201568,
author = {Leonid Ryzhyk and Nikolaj Bj{\o}rner and Marco Canini and Jean-Baptiste Jeannin and Cole Schlesinger and Douglas B. Terry and George Varghese},
title = {Correct by Construction Networks Using Stepwise Refinement},
booktitle = {14th {USENIX} Symposium on Networked Systems Design and Implementation ({NSDI} 17)},
year = {2017},
isbn = {978-1-931971-37-9},
address = {Boston, MA},
pages = {683--698},
url = {https://www.usenix.org/conference/nsdi17/technical-sessions/presentation/ryzhyk},
publisher = {{USENIX} Association},
}