TY - GEN
T1 - Verifying reachability in networks with mutable datapaths
AU - Panda, Aurojit
AU - Lahav, Ori
AU - Argyraki, Katerina
AU - Sagiv, Mooly
AU - Shenker, Scott
N1 - Funding Information:
We thank Shivaram Venkatraman, Colin Scott, Kay Ousterhout, Amin Tootoonchian, Justine Sherry, Sylvia Ratnasamy, Nate Foster, the anonymous reviewers and our shepherd Boon Thau Loo for the many helpful comments that have greatly improved both the techniques described within this paper and their presentation. This work was supported in part by a grant from Intel Corporation, NSF grant 1420064, and an ERC grant (agreement number 321174-VSSC).
PY - 2017/1/1
Y1 - 2017/1/1
N2 - Recent work has made great progress in verifying the forwarding correctness of networks [26–28, 35]. However, these approaches cannot be used to verify networks containing middleboxes, such as caches and firewalls, whose forwarding behavior depends on previously observed traffic. We explore how to verify reachability properties for networks that include such “mutable datapath” elements, both for the original network and in the presence of failures. The main challenge lies in handling large and complicated networks. We achieve scaling by developing and leveraging the concept of slices, which allow network-wide verification to only require analyzing small portions of the network. We show that with slices the time required to verify an invariant on many production networks is independent of the size of the network itself.
AB - Recent work has made great progress in verifying the forwarding correctness of networks [26–28, 35]. However, these approaches cannot be used to verify networks containing middleboxes, such as caches and firewalls, whose forwarding behavior depends on previously observed traffic. We explore how to verify reachability properties for networks that include such “mutable datapath” elements, both for the original network and in the presence of failures. The main challenge lies in handling large and complicated networks. We achieve scaling by developing and leveraging the concept of slices, which allow network-wide verification to only require analyzing small portions of the network. We show that with slices the time required to verify an invariant on many production networks is independent of the size of the network itself.
UR - http://www.scopus.com/inward/record.url?scp=85071273649&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85071273649&partnerID=8YFLogxK
M3 - Conference contribution
T3 - Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017
SP - 699
EP - 718
BT - Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017
PB - USENIX Association
T2 - 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017
Y2 - 27 March 2017 through 29 March 2017
ER -