Correct by construction networks using stepwise refinement

Leonid Ryzhyk, Nikolaj Bjørner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, George Varghese

Research output: Chapter in Book/Report/Conference proceedingConference contribution

16 Scopus citations

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.
Original languageEnglish (US)
Title of host publicationNSDI'17 Proceedings of the 14th USENIX Conference on Networked Systems Design and Implementation
PublisherUSENIX Association Berkeley, CA, USA
StatePublished - Mar 2017

Fingerprint Dive into the research topics of 'Correct by construction networks using stepwise refinement'. Together they form a unique fingerprint.

Cite this