Advertisement

Some complexity results for stateful network verification

  • Kalev AlpernasEmail author
  • Aurojit Panda
  • Alexander Rabinovich
  • Mooly Sagiv
  • Scott Shenker
  • Sharon Shoham
  • Yaron Velner
Article
  • 27 Downloads

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.

Keywords

Safety verification Stateful networks Middleboxes Channel systems Petri nets Complexity bounds 

Notes

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.

References

  1. 1.
    Abdulla P, Jonsson B (1993) Verifying programs with unreliable channels. In: Logic in computer science (LICS). IEEE, pp 160–170Google Scholar
  2. 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–321Google Scholar
  3. 3.
    Anderson CJ, Foster N, Guha A, Jeannin JB, Kozen D, Schlesinger C, Walker D (2014) NetKAT: semantic foundations for networks. In: POPLGoogle Scholar
  4. 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–1382Google Scholar
  5. 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 31Google Scholar
  6. 6.
    Bochmann GV (1978) Finite state description of communication protocols. Comput Netw 2(4):361–372 (1976)Google Scholar
  7. 7.
    Brand D, Zafiropulo P (1983) On communicating finite-state machines. J ACM 30(2):323–342MathSciNetCrossRefzbMATHGoogle Scholar
  8. 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)Google Scholar
  9. 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–54Google Scholar
  10. 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–106Google Scholar
  11. 11.
    Finkel A, Schnoebelen P (2001) Well-structured transition systems everywhere!. Theor Comput Sci 256(1):63–92MathSciNetCrossRefzbMATHGoogle Scholar
  12. 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–483Google Scholar
  13. 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–355Google Scholar
  14. 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–112Google Scholar
  15. 15.
    Higman G (1952) Ordering by divisibility in abstract algebras. In: Proceedings of the London Mathematical Society, pp 326–336Google Scholar
  16. 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)Google Scholar
  17. 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)Google Scholar
  18. 18.
    Khurshid A, Zhou W, Caesar M, Godfrey B (2012) Veriflow: verifying network-wide invariants in real time. Comput Commun Rev 42(4):467–472CrossRefGoogle Scholar
  19. 19.
    Kozen D (1977) Lower bounds for natural proof systems. In: 18th annual symposium on foundations of computer science. IEEE, pp 254–266Google Scholar
  20. 20.
    Kuzniar M, Peresini P, Canini M, Venzano D, Kostic D (2012) A soft way for OpenFlow switch interoperability testing. In: CoNEXT, pp 265–276Google Scholar
  21. 21.
    Lipton R (1976) The reachability problem requires exponential space. Technical report 62, Department of Computer Science, Yale UniversityGoogle Scholar
  22. 22.
    LogicBlox. http://www.logicblox.com/. Retrieved 7 July 2015
  23. 23.
  24. 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–512Google Scholar
  25. 25.
    Mai H, Khurshid A, Agarwal R, Caesar M, Godfrey B, King ST (2011) Debugging the data plane with anteater. In: SIGCOMMGoogle Scholar
  26. 26.
    Minsky ML (1961) Recursive unsolvability of post’s problem of “tag” and other topics in theory of turing machines. Ann Math 74:437–455MathSciNetCrossRefzbMATHGoogle Scholar
  27. 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–531Google Scholar
  28. 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–220Google Scholar
  29. 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. 30.
    Peterson JL (1977) Petri nets. ACM Comput Surv 9(3):223–252CrossRefzbMATHGoogle Scholar
  31. 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–22Google Scholar
  32. 32.
    Rackoff C (1978) The covering and boundedness problems for vector addition systems. Theor Comput Sci 6(2):223–231MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Ritchey RW, Ammann P (2000) Using model checking to analyze network vulnerabilities. In: Security and privacyGoogle Scholar
  34. 34.
    Schmidt K (2000) Lola a low level analyser. In: Application and theory of Petri nets 2000. Springer, pp 465–474Google Scholar
  35. 35.
    Schnoebelen P (2002) Verifying lossy channel systems has nonprimitive recursive complexity. Inf Process Lett 83(5):251–261MathSciNetCrossRefzbMATHGoogle Scholar
  36. 36.
    Sen K, Viswanathan M (2006) Model checking multithreaded programs with asynchronous atomic methods. In: International conference on computer aided verification. Springer, pp 300–314Google Scholar
  37. 37.
    Sethi D, Narayana S, Malik S (2013) Abstractions for model checking SDN controllers. In: FMCADGoogle Scholar
  38. 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: SIGCOMMGoogle Scholar
  39. 39.
    Skowyra R, Lapets A, Bestavros A, Kfoury A (2013) A verification platform for SDN-enabled applications. In: HiCoNSGoogle Scholar
  40. 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–36Google Scholar
  41. 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–830Google Scholar
  42. 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: NSDIGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2019

Authors and Affiliations

  1. 1.Tel Aviv UniversityTel AvivIsrael
  2. 2.NYUNew YorkUSA
  3. 3.UC BerkeleyBerkeleyUSA
  4. 4.Hebrew University of JerusalemJerusalemIsrael

Personalised recommendations