Verifying Reachability in Networks with Mutable Datapaths

TitleVerifying Reachability in Networks with Mutable Datapaths
Publication TypeConference Paper
Year of Publication2017
AuthorsPanda, A., Lahav O., Argyraki K. J., Sagiv M., & Shenker S.
Published inProceedings of NSDI '17
Abstract

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.

Acknowledgment

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). 

URLhttps://www.usenix.org/system/files/conference/nsdi17/nsdi17-panda-mutable-datapaths.pdf
ICSI Research Group

Networking and Security