Liveness Verification of Stateful Network Functions


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


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


@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 },
year = {2020},
address = {Santa Clara, CA},
pages = {257--272},
url = {},
publisher = {{USENIX} Association},
month = feb,

Presentation Video