Title
Correct By Construction Networks Using Stepwise Refinement
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.
Year
Venue
Field
2017
PROCEEDINGS OF NSDI '17: 14TH USENIX SYMPOSIUM ON NETWORKED SYSTEMS DESIGN AND IMPLEMENTATION
Computer science,Top-down and bottom-up design,Computational science,Distributed computing
DocType
Citations 
PageRank 
Conference
4
0.41
References 
Authors
0
7
Name
Order
Citations
PageRank
Leonid Ryzhyk121216.05
Nikolaj Bjørner23818181.02
Marco Canini385760.21
Jean-Baptiste Jeannin413612.59
Cole Schlesinger586241.41
Doug Terry643881498.27
George Varghese78149727.66