Liveness Verification of Stateful Network Functions

Authors: 

Farnaz Yousefi, Johns Hopkins University; Anubhavnidhi Abhashkumar and Kausik Subramanian, University of Wisconsin-Madison; Kartik Hans, IIT Delhi; Soudeh Ghorbani, Johns Hopkins University; Aditya Akella, University of Wisconsin-Madison

Abstract: 

Network verification tools focus almost exclusively on various safety properties such as reachability invariants, e.g., is there a path from host A to host B? Thus, they are inapplicable to providing strong correctness guarantees for modern programmable networks that increasingly rely on stateful network functions. Correct operations of such networks depend on the validity of a larger set of properties, in particular liveness properties. For instance, a stateful firewall that only allows solicited external traffic works correctly if it eventually detects and blocks malicious connections, e.g., if it eventually blocks an external host E that tries to reach the internal host I before receiving a request from I.

Alas, verifying liveness properties is computationally expensive and in some cases undecidable. Existing verification techniques do not scale to verify such properties. In this work, we provide a compositional programming abstraction that decouples reachability from stateful network functions. We then model the behavior of the programs expressed in this abstraction using compact Boolean formulas, and show that verification of complex properties is fast on these formulas, e.g., for a network with 100 hosts, these formulas result in 8x speedup in verifying key properties compared to the state-of-the-art. Finally, we provide a compiler that translates the programs written using our abstraction to P4 programs.

NSDI '20 Open Access Sponsored by NetApp

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.

BibTeX
@inproceedings {246364,
author = {Farnaz Yousefi and Anubhavnidhi Abhashkumar and Kausik Subramanian and Kartik Hans and Soudeh Ghorbani and Aditya Akella},
title = {Liveness Verification of Stateful Network Functions },
booktitle = {17th {USENIX} Symposium on Networked Systems Design and Implementation ({NSDI} 20)},
year = {2020},
isbn = {978-1-939133-13-7},
address = {Santa Clara, CA},
pages = {257--272},
url = {https://www.usenix.org/conference/nsdi20/presentation/yousefi},
publisher = {{USENIX} Association},
month = feb,
}

Presentation Video