Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Robots at the Edge of the Cloud Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Some Complexity Results for Stateful Network Verification

Authors : Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker, Sharon Shoham

Published in: Tools and Algorithms for the Construction and Analysis of Systems

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In modern networks, forwarding of packets often depends on the history of previously transmitted traffic. Such networks contain stateful middleboxes, whose forwarding behavior depends on a mutable internal state. Firewalls and load balancers are typical examples of stateful middleboxes.
This paper 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, we show that safety checking is EXPSPACE-complete in the number of hosts and middleboxes in the network. We further 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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Reasoning About Information Flow Security of Separation Kernels with Channel-Based Communication
next chapter Characteristic Formulae for Session Types
Footnotes
1
Switches are a degenerate case of middleboxes, whose state is constant and hence their forwarding behavior does not change over time.
 
2
A subsequence is a sequence that can be derived from another sequence by deleting some elements without changing the order of the remaining elements.
 
Literature
1.
2.
Abdulla, P., Jonsson, B.: Verifying programs with unreliable channels. In: Logic in Computer Science (LICS), pp. 160–170. IEEE (1993)
3.
Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Logic in Computer Science (LICS), pp. 313–321. IEEE (1996)
4.
Anderson, C.J., Foster, N., Guha, A., Jeannin, J.-B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: Semantic foundations for networks. In: POPL (2014)
5.
Aref, M., ten Cate, B., Green, T.J., Kimelfeld, B., Olteanu, D., Pasalic, E., Veldhuizen, T.L., Washburn, G.: Design and implementation of the logicblox system. In: ACM SIGMOD International Conference on Management of Data, pp. 1371–1382 (2015)
6.
Ball, T., Bjørner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: Vericon: towards verifying controller programs in software-defined networks. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, p. 31 (2014)
7.
Bochmann, G.V.: Finite state description of communication protocols. Comput. Netw. 2(4–5), 361–372 (1978)
8.
9.
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)
10.
Cardoza, E., Lipton, R., Meyer, A.R.: Exponential space complete problems for petri nets and commutative semigroups (preliminary report). In: Proceedings of the Eighth Annual ACM Symposium on Theory of Computing, pp. 50–54. ACM (1976)
11.
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. IFIP, pp. 87–106. Springer, Heidelberg (1998)CrossRef
12.
13.
Fogel, A., Fung, S., Pedrosa, L., Walraed-Sullivan, M., Govindan, R., Mahajan, R., Millstein, T.D.: A general approach to network configuration analysis. In: 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4–6, pp. 469–483 (2015)
14.
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 , Mumbai, India, 15–17 January 2015, pp. 343–355 (2015)
15.
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)
16.
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)
17.
Khurshid, A., Zhou, W., Caesar, M., Godfrey, B.: Veriflow: verifying network-wide invariants in real time. Comput. Commun. Rev. 42(4), 467–472 (2012)CrossRef
18.
Kuzniar, M., Peresini, P., Canini, M., Venzano, D., Kostic, D.: A soft way for openflow switch interoperability testing. In: CoNEXT, pp. 265–276 (2012)
19.
Lopes, N.P., Bjørner, N., Godefroid, P., Jayaraman, K., Varghese, G.: Checking beliefs in dynamic networks. In: 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4–6, pp. 499–512 (2015)
20.
Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, B., King, S.T.: Debugging the data plane with anteater. In: SIGCOMM (2011)
21.
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, Seattle, WA, USA, April 2–4, 2014, pp. 519–531 (2014)
22.
23.
Panda, A., Argyraki, K.J., Sagiv, M., Schapira, M., Shenker, S.: New directions for network verification. In: 1st Summit on Advances in Programming Languages, SNAPL 3–6, 2015, Asilomar, California, USA, pp. 209–220, May 2015
24.
Panda, A., Lahav, O., Argyraki, K., Sagiv, M., Shenker, S.: Verifying isolation properties in the presence of middleboxes (2014). arXiv preprint arXiv:​ 1409.​7687
25.
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, October 23–25, 2013, pp. 9–22 (2013)
26.
27.
Ritchey, R.W., Ammann, P.: Using model checking to analyze network vulnerabilities. In: Security and Privacy (2000)
28.
Schmidt, K.: LoLA a low level analyser. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, p. 465. Springer, Heidelberg (2000)CrossRef
29.
Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83(5), 251–261 (2002)MathSciNetCrossRefMATH
30.
Sethi, D., Narayana, S., Malik, S.: Abstractions for model checking SDN controllers. In: FMCAD (2013)
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)
32.
Skowyra, R., Lapets, A., Bestavros, A., Kfoury, A.: A verification platform for SDN-enabled applications. In: HiCoNS (2013)
33.
Stoenescu, R., Popovici, M., Negreanu, L., Raiciu, C.: Symnet: static checking for stateful networks. In: Proceedings of the 2013 Workshop on Hot Topics in Middleboxes and Network Function Virtualization, pp. 31–36. ACM (2013)
34.
35.
Zeng, H., Zhang, S., Ye, F., Jeyakumar, V., Ju, M., Liu, J., McKeown, N., Vahdat, A.: Libra: Divide and conquer to verify forwarding tables in huge networks. In: NSDI (2014)
Metadata
Title
Some Complexity Results for Stateful Network Verification
Authors
Yaron Velner
Kalev Alpernas
Aurojit Panda
Alexander Rabinovich
Mooly Sagiv
Scott Shenker
Sharon Shoham
Copyright Year
2016
Publisher
Springer Berlin Heidelberg
Book
Tools and Algorithms for the Construction and Analysis of Systems

Print ISBN: 978-3-662-49673-2

Electronic ISBN: 978-3-662-49674-9

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-662-49674-9_51

Premium Partner

    Image Credits