Verifying Reachability in Networks with Mutable Datapaths


Aurojit Panda, University of California, Berkeley; Ori Lahav, Max Planck Institute for Software Systems (MPI-SWS); Katerina Argyraki, École Polytechnique Fédérale de Lausanne (EPFL); Mooly Sagiv, Tel Aviv University; Scott Shenker, University of California, Berkeley, and International Computer Science Institute


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.

NSDI '17 Open Access Videos Sponsored by
King Abdullah University of Science and Technology (KAUST)

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

@inproceedings {201569,
author = {Aurojit Panda and Ori Lahav and Katerina Argyraki and Mooly Sagiv and Scott Shenker},
title = {Verifying Reachability in Networks with Mutable Datapaths},
booktitle = {14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)},
year = {2017},
isbn = {978-1-931971-37-9},
address = {Boston, MA},
pages = {699--718},
url = {},
publisher = {USENIX Association},
month = mar

Presentation Video 

Presentation Audio