Verifying reachability in networks with mutable datapaths

Aurojit Panda, Ori Lahav, Katerina Argyraki, Mooly Sagiv, Scott Shenker

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

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017
PublisherUSENIX Association
Pages699-718
Number of pages20
ISBN (Electronic)9781931971379
StatePublished - Jan 1 2017
Event14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017 - Boston, United States
Duration: Mar 27 2017Mar 29 2017

Publication series

NameProceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017

Conference

Conference14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017
CountryUnited States
CityBoston
Period3/27/173/29/17

ASJC Scopus subject areas

  • Control and Systems Engineering
  • Computer Networks and Communications

Cite this

Panda, A., Lahav, O., Argyraki, K., Sagiv, M., & Shenker, S. (2017). Verifying reachability in networks with mutable datapaths. In Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017 (pp. 699-718). (Proceedings of the 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017). USENIX Association.