Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Some complexity results for stateful network verification

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

In modern networks, forwarding of packets often depends on the history of previously transmitted traffic. Such networks contain stateful middleboxes, whose forwarding behaviour depends on a mutable internal state. Firewalls and load balancers are typical examples of stateful middleboxes. This work addresses the complexity of verifying safety properties, such as isolation, in networks with finite-state middleboxes. Unfortunately, we show that even in the absence of forwarding loops, reasoning about such networks is undecidable due to interactions between middleboxes connected by unbounded ordered channels. We therefore abstract away channel ordering. This abstraction is sound for safety, and makes the problem decidable. Specifically, safety checking becomes EXPSPACE-complete in the number of hosts and middleboxes in the network. To tackle the high complexity, we identify two useful subclasses of finite-state middleboxes which admit better complexities. The simplest class includes, e.g., firewalls and permits polynomial-time verification. The second class includes, e.g., cache servers and learning switches, and makes the safety problem coNP-complete. Finally, we implement a tool for verifying the correctness of stateful networks.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13

Similar content being viewed by others

Notes

  1. In this work we do not distinguish between routers and switches, since they obey similar forwarding models.

  2. Routers may be considered a degenerate case of middleboxes, whose state is constant and hence their forwarding behaviour does not change over time.

  3. A subsequence is a sequence that can be derived from another sequence by deleting some elements without changing the order of the remaining elements.

References

  1. Abdulla P, Jonsson B (1993) Verifying programs with unreliable channels. In: Logic in computer science (LICS). IEEE, pp 160–170

  2. Abdulla PA, Čerāns K, Jonsson B, Tsay YK (1996) General decidability theorems for infinite-state systems. In: Logic in computer science (LICS). IEEE, pp 313–321

  3. Anderson CJ, Foster N, Guha A, Jeannin JB, Kozen D, Schlesinger C, Walker D (2014) NetKAT: semantic foundations for networks. In: POPL

  4. Aref M, ten Cate B, Green TJ, Kimelfeld B, Olteanu D, Pasalic E, Veldhuizen TL, Washburn G (2015) Design and implementation of the LogicBlox system. In: ACM SIGMOD international conference on management of data, pp 1371–1382

  5. Ball T, Bjørner N, Gember A, Itzhaky S, Karbyshev A, Sagiv M, Schapira M, Valadarsky A (2014) Vericon: towards verifying controller programs in software-defined networks. In: ACM SIGPLAN conference on programming language design and implementation, PLDI, p 31

  6. Bochmann GV (1978) Finite state description of communication protocols. Comput Netw 2(4):361–372 (1976)

    Google Scholar 

  7. Brand D, Zafiropulo P (1983) On communicating finite-state machines. J ACM 30(2):323–342

    Article  MathSciNet  Google Scholar 

  8. Canini M, Venzano D, Peres P, Kostic D, Rexford J (2012) A nice way to test openflow applications. In: 9th USENIX symposium on networked systems design and implementation (NSDI’12)

  9. Cardoza E, Lipton R, Meyer AR (1976) Exponential space complete problems for Petri nets and commutative semigroups (preliminary report). In: Proceedings of the eighth annual ACM symposium on theory of computing. ACM, pp 50–54

  10. Clarke EM, Jha S, Marrero WR (1998) Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: IFIP TC2/WG2.2,2.3 international conference on programming concepts and methods (PROCOMET ’98), Shelter Island, New York, USA, 8–12 June 1998, pp 87–106

  11. Finkel A, Schnoebelen P (2001) Well-structured transition systems everywhere!. Theor Comput Sci 256(1):63–92

    Article  MathSciNet  Google Scholar 

  12. Fogel A, Fung S, Pedrosa L, Walraed-Sullivan M, Govindan R, Mahajan R, Millstein TD (2015) A general approach to network configuration analysis. In: 12th USENIX symposium on networked systems design and implementation, NSDI 15, Oakland, CA, USA, 4–6 May 2015, pp 469–483

  13. Foster N, Kozen D, Milano M, Silva A, Thompson L (2015) A coalgebraic decision procedure for NetKat. In: Proceedings of the 42nd annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2015, Mumbai, India, 15–17 Jan 2015, pp 343–355

  14. Hengartner U, Moon S, Mortier R, Diot C (2002) Detection and analysis of routing loops in packet traces. In: Proceedings of the 2nd ACM SIGCOMM workshop on internet measurement. ACM, pp 107–112

  15. Higman G (1952) Ordering by divisibility in abstract algebras. In: Proceedings of the London Mathematical Society, pp 326–336

    Article  MathSciNet  Google Scholar 

  16. Kazemian P, Chang M, Zeng H, Varghese G, McKeown N, Whyte S (2013) Real time network policy checking using header space analysis. In: 10th USENIX symposium on networked systems design and implementation (NSDI ’13)

  17. Kazemian P, Varghese G, McKeown N (2012) Header space analysis: static checking for networks. In: 9th USENIX symposium on networked systems design and implementation (NSDI ’12)

  18. Khurshid A, Zhou W, Caesar M, Godfrey B (2012) Veriflow: verifying network-wide invariants in real time. Comput Commun Rev 42(4):467–472

    Article  Google Scholar 

  19. Kozen D (1977) Lower bounds for natural proof systems. In: 18th annual symposium on foundations of computer science. IEEE, pp 254–266

  20. Kuzniar M, Peresini P, Canini M, Venzano D, Kostic D (2012) A soft way for OpenFlow switch interoperability testing. In: CoNEXT, pp 265–276

  21. Lipton R (1976) The reachability problem requires exponential space. Technical report 62, Department of Computer Science, Yale University

  22. LogicBlox. http://www.logicblox.com/. Retrieved 7 July 2015

  23. Lola 2.0 sources. http://download.gna.org/service-tech/lola/lola-2.0.tar.gz

  24. Lopes NP, Bjørner N, Godefroid P, Jayaraman K, Varghese G (2015) Checking beliefs in dynamic networks. In: 12th USENIX symposium on networked systems design and implementation, NSDI 15, Oakland, CA, USA, 4–6 May 2015, pp 499–512

  25. Mai H, Khurshid A, Agarwal R, Caesar M, Godfrey B, King ST (2011) Debugging the data plane with anteater. In: SIGCOMM

  26. Minsky ML (1961) Recursive unsolvability of post’s problem of “tag” and other topics in theory of turing machines. Ann Math 74:437–455

    Article  MathSciNet  Google Scholar 

  27. Nelson T, Ferguson AD, Scheer MJG, Krishnamurthi S (2014) Tierless programming and reasoning for software-defined networks. In: Proceedings of the 11th USENIX symposium on networked systems design and implementation, NSDI 2014, Seattle, WA, USA, 2–4 Apr 2014, pp 519–531

  28. Panda A, Argyraki KJ, Sagiv M, Schapira M, Shenker S (2015) New directions for network verification. In: 1st summit on advances in programming languages, SNAPL 2015, Asilomar, California, USA, 3–6 May 2015, pp 209–220

  29. Panda A, Lahav O, Argyraki K, Sagiv M, Shenker S (2014) Verifying isolation properties in the presence of middleboxes. arXiv preprint arXiv:1409.7687

  30. Peterson JL (1977) Petri nets. ACM Comput Surv 9(3):223–252

    Article  Google Scholar 

  31. Potharaju R, Jain N (2013) Demystifying the dark side of the middle: a field study of middlebox failures in datacenters. In: Proceedings of the 2013 internet measurement conference, IMC 2013, Barcelona, Spain, 23–25 Oct 2013, pp 9–22

  32. Rackoff C (1978) The covering and boundedness problems for vector addition systems. Theor Comput Sci 6(2):223–231

    Article  MathSciNet  Google Scholar 

  33. Ritchey RW, Ammann P (2000) Using model checking to analyze network vulnerabilities. In: Security and privacy

  34. Schmidt K (2000) Lola a low level analyser. In: Application and theory of Petri nets 2000. Springer, pp 465–474

  35. Schnoebelen P (2002) Verifying lossy channel systems has nonprimitive recursive complexity. Inf Process Lett 83(5):251–261

    Article  MathSciNet  Google Scholar 

  36. Sen K, Viswanathan M (2006) Model checking multithreaded programs with asynchronous atomic methods. In: International conference on computer aided verification. Springer, pp 300–314

  37. Sethi D, Narayana S, Malik S (2013) Abstractions for model checking SDN controllers. In: FMCAD

  38. Sherry J, Hasan S, Scott C, Krishnamurthy A, Ratnasamy S, Sekar V (2012) Making middleboxes someone else’s problem: network processing as a cloud service. In: SIGCOMM

  39. Skowyra R, Lapets A, Bestavros A, Kfoury A (2013) A verification platform for SDN-enabled applications. In: HiCoNS

  40. Stoenescu R, Popovici M, Negreanu L, Raiciu C (2013) Symnet: static checking for stateful networks. In: Proceedings of the 2013 workshop on Hot topics in middleboxes and network function virtualization. ACM, pp 31–36

  41. Velner Y, Alpernas K, Panda A, Rabinovich A, Sagiv M, Shenker S, Shoham S (2016) Some complexity results for stateful network verification. In: International conference on tools and algorithms for the construction and analysis of systems. Springer, pp 811–830

  42. Zeng H, Zhang S, Ye F, Jeyakumar V, Ju M, Liu J, McKeown N, Vahdat A (2014) Libra: divide and conquer to verify forwarding tables in huge networks. In: NSDI

Download references

Acknowledgements

This publication is part of projects that have received funding from the European Research Council (ERC) under the European Union’s Seventh Framework Program (FP7/2007–2013)/ERC Grant Agreement No. 321174-VSSC, and Horizon 2020 research and innovation programme (Grant Agreement No. 759102-SVIS). The research was supported in part by Len Blavatnik and the Blavatnik Family foundation, the Blavatnik Interdisciplinary Cyber Research Center, Tel Aviv University, and the Pazy Foundation. This material is based upon work supported by the United States-Israel Binational Science Foundation (BSF) Grant Nos. 2016260 and 2012259. This research was also supported in part by NSF Grants 1704941 and 1420064, and funding provided by Intel Corporation.

Author information

Authors and Affiliations

  1. Tel Aviv University, Tel Aviv, Israel

    Kalev Alpernas, Alexander Rabinovich, Mooly Sagiv & Sharon Shoham

  2. NYU, New York, USA

    Aurojit Panda

  3. UC Berkeley, Berkeley, USA

    Scott Shenker

  4. Hebrew University of Jerusalem, Jerusalem, Israel

    Yaron Velner

Authors
  1. Kalev Alpernas
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aurojit Panda
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexander Rabinovich
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mooly Sagiv
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Scott Shenker
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Sharon Shoham
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Yaron Velner
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kalev Alpernas.

Additional information

A preliminary version of this work appeared in [41].

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Alpernas, K., Panda, A., Rabinovich, A. et al. Some complexity results for stateful network verification. Form Methods Syst Des 54, 191–231 (2019). https://doi.org/10.1007/s10703-018-00330-9

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-018-00330-9

Keywords

Search

Navigation