Advertisement

Abstract Interpretation of Stateful Networks

  • Kalev AlpernasEmail author
  • Roman Manevich
  • Aurojit Panda
  • Mooly Sagiv
  • Scott Shenker
  • Sharon Shoham
  • Yaron Velner
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

Modern networks achieve robustness and scalability by maintaining states on their nodes. These nodes are referred to as middleboxes and are essential for network functionality. However, the presence of middleboxes drastically complicates the task of network verification. Previous work showed that the problem is undecidable in general and EXPSPACE-complete when abstracting away the order of packet arrival.

We describe a new algorithm for conservatively checking isolation properties of stateful networks. The asymptotic complexity of the algorithm is polynomial in the size of the network, albeit being exponential in the maximal number of queries of the local state that a middlebox can do, which is often small.

Our algorithm is sound, i.e., it can never miss a violation of safety but may fail to verify some properties. The algorithm performs on-the fly abstract interpretation by (1) abstracting away the order of packet processing and the number of times each packet arrives, (2) abstracting away correlations between states of different middleboxes and channel contents, and (3) representing middlebox states by their effect on each packet separately, rather than taking into account the entire state space. We show that the abstractions do not lose precision when middleboxes may reset in any state. This is encouraging since many real middleboxes reset, e.g., after some session timeout is reached or due to hardware failure.

Notes

Acknowledgments

We thank our anonymous shepherd, and anonymous referees for insightful comments which improved this paper. We thank LogicBlox for providing us with an academic license for their software, and Todd J. Green and Martin Bravenboer for providing technical support and helping with optimization. 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) grants No. 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.
    Alpernas, K., et al.: Abstract interpretation of stateful networks. arXiv preprint arXiv:1708.05904 (2018)
  2. 2.
    Anderson, C.J., et al.: NetKAT: semantic foundations for networks. In: POPL (2014)Google Scholar
  3. 3.
    Aref, M., et al.: Design and implementation of the LogicBlox system. In: ACM SIGMOD International Conference on Management of Data, pp. 1371–1382 (2015)Google Scholar
  4. 4.
    Ball, T., et al.: VeriCon: towards verifying controller programs in software-defined networks. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, p. 31 (2014)Google Scholar
  5. 5.
    Canini, M., Venzano, D., Peres, P., Kostic, D., Rexford, J.: A NICE way to test OpenFlow applications. In: 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2012) (2012)Google Scholar
  6. 6.
    Clarke, E.M., Jha, S., Marrero, W.: Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: Gries, D., de Roever, W.-P. (eds.) Programming Concepts and Methods PROCOMET 1998. ITIFIP, pp. 87–106. Springer, Boston, MA (1998).  https://doi.org/10.1007/978-0-387-35358-6_10CrossRefGoogle Scholar
  7. 7.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 269–282. ACM (1979)Google Scholar
  8. 8.
    Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 124–140. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_8CrossRefGoogle Scholar
  9. 9.
    Fayaz, S.K., Yu, T., Tobioka, Y., Chaki, S., Sekar, V., Vyas, S.: BUZZ: testing context-dependent policies in stateful networks. In: NSDI (2016)Google Scholar
  10. 10.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1–2), 63–92 (2001)Google Scholar
  11. 11.
    Flanagan, C., Freund, S.N., Qadeer, S., Seshia, S.A.: Modular verification of multithreaded programs. Theor. Comput. Sci. 338(1–3), 153–183 (2005)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: 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 January 2015, pp. 343–355 (2015)Google Scholar
  13. 13.
    Hoenicke, J., Majumdar, R., Podelski, A.: Thread modularity at many levels: a pearl in compositional verification. In: POPL, pp. 473–485 (2017)Google Scholar
  14. 14.
    Kazemian, P., Chang, M., Zeng, H., Varghese, G., McKeown, N., Whyte, S.: Real time network policy checking using header space analysis. In: 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2013) (2013)Google Scholar
  15. 15.
    Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2012) (2012)Google Scholar
  16. 16.
    Khurshid, A., Zhou, W., Caesar, M., Godfrey, B.: VeriFlow: verifying network-wide invariants in real time. Comput. Commun. Rev. 42(4), 467–472 (2012)CrossRefGoogle Scholar
  17. 17.
    Kuzniar, M., Peresini, P., Canini, M., Venzano, D., Kostic, D.: A SOFT way for OpenFlow switch interoperability testing. In: CoNEXT, pp. 265–276 (2012)Google Scholar
  18. 18.
    Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, B., King, S.T.: Debugging the data plane with anteater. In: SIGCOMM (2011)Google Scholar
  19. 19.
    Marmorstein, R.M., Kearns, P.: A tool for automated iptables firewall analysis. In: USENIX Annual Technical Conference, Freenix Track, pp. 71–81 (2005)Google Scholar
  20. 20.
    Mayer, A., Wool, A., Ziskind, E.: Fang: a firewall analysis engine. In: Proceedings of 2000 IEEE Symposium on Security and Privacy, S&P 2000, pp. 177–187. IEEE (2000)Google Scholar
  21. 21.
    Namjoshi, K.S., Trefler, R.J.: Uncovering symmetries in irregular process networks. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 496–514. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-35873-9_29CrossRefGoogle Scholar
  22. 22.
    Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The margrave tool for firewall analysis. In: LISA (2010)Google Scholar
  23. 23.
    Nelson, T., Ferguson, A.D., Scheer, M.J.G., Krishnamurthi, S.: 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 April 2014, pp. 519–531 (2014)Google Scholar
  24. 24.
    Panda, A., Lahav, O., Argyraki, K.J., Sagiv, M., Shenker, S.: Verifying reachability in networks with mutable datapaths. In: 14th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2017, Boston, MA, USA, 27–29 March 2017, pp. 699–718 (2017)Google Scholar
  25. 25.
    Plotkin, G.D., Bjørner, N., Lopes, N.P., Rybalchenko, A., Varghese, G.: Scaling network verification using symmetry and surgery. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20–22 January 2016, pp. 69–83 (2016)Google Scholar
  26. 26.
    Pnueli, A., Xu, J., Zuck, L.: Liveness with \((0,1, \infty )\)-counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107–122. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45657-0_9CrossRefGoogle Scholar
  27. 27.
    Potharaju, R., Jain, N.: 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 October 2013, pp. 9–22 (2013)Google Scholar
  28. 28.
    Ritchey, R.W., Ammann, P.: Using model checking to analyze network vulnerabilities. In: Security and Privacy (2000)Google Scholar
  29. 29.
    Roscoe, A.W., Hoare, C.A.R.: The laws of OCCAM programming. Theor. Comput. Sci. 60(2), 177–229 (1988)MathSciNetCrossRefGoogle Scholar
  30. 30.
    Sethi, D., Narayana, S., Malik, S.: Abstractions for model checking SDN controllers. In: FMCAD (2013)Google Scholar
  31. 31.
    Sherry, J., Hasan, S., Scott, C., Krishnamurthy, A., Ratnasamy, S., Sekar, V.: Making middleboxes someone else’s problem: network processing as a cloud service. In: SIGCOMM (2012)Google Scholar
  32. 32.
    Sivaraman, A., et al.: Packet transactions: high-level programming for line-rate switches. In: Proceedings of the ACM SIGCOMM 2016 Conference, Florianopolis, Brazil, 22–26 August 2016, pp. 15–28 (2016)Google Scholar
  33. 33.
    Skowyra, R., Lapets, A., Bestavros, A., Kfoury, A.: A verification platform for SDN-enabled applications. In: HiCoNS (2013)Google Scholar
  34. 34.
    Stoenescu, R., Popovici, M., Negreanu, L., Raiciu, C.: Scalable symbolic execution for modern networks. In: SIGCOMM (2016)Google Scholar
  35. 35.
    Velner, Y., et al.: Some complexity results for stateful network verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 811–830. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_51CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Kalev Alpernas
    • 1
    Email author
  • Roman Manevich
    • 2
  • Aurojit Panda
    • 3
  • Mooly Sagiv
    • 1
  • Scott Shenker
    • 4
  • Sharon Shoham
    • 1
  • Yaron Velner
    • 5
  1. 1.Tel Aviv UniversityTel AvivIsrael
  2. 2.Ben-Gurion University of the NegevBeer-ShevaIsrael
  3. 3.NYUNew YorkUSA
  4. 4.UC BerkeleyBerkeleyUSA
  5. 5.Hebrew University of JerusalemJerusalemIsrael

Personalised recommendations