nach oben

Journal of Reliable Intelligent Environments

Erschienen in:

29.07.2017 | Original Article

A characterisation of verification tools for software defined networks

verfasst von: Leticia Lavado, Laura Panizo, María-del-Mar Gallardo, Pedro Merino

Erschienen in: Journal of Reliable Intelligent Environments | Ausgabe 3/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Software-defined networking (SDN) is a new paradigm to introduce intelligence in communication networks through centralised programming. SDN separates data and control plane with two main components, the programmable switches (data plane) and the central controller where network applications are executed. This highly programmable and flexible network introduces many challenges from the point of view of reliability (or robustness), and operators need to ensure the same level of confidence as in previous less flexible deployments. This paper provides a first study of the current verification tools used to analyse different properties of SDNs before deployment and/or during the exploitation of the network. Most of these tools offer some kind of automatic verification, supported by algorithms based on formal methods, but they do not differentiate between fixed and mobile/wireless networks. In the paper, we provide a number of classifications of the tools to make this selection easier for potential users, and we also identify promising research areas where more effort needs to be made.

Vorheriger Artikel A secure remote user authentication scheme for smart cities e-governance applications

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

NICE is available at https://code.google.com/archive/p/nice-of/.

Hassel is available at https://bitbucket.org/peymank/hassel-public/src.

The implementation and invariant examples are available online at http://people.csail.mit.edu/shachari/.

The prototype tool can be found at https://github.com/nsg-ethz/SDNRacer

Ternary content addressable memory (TCAM) is a fast associative memory which is very common and useful in switches for building IP routing tables.

Frenetic family languages and the repository are available at http://www.frenetic-lang.org/.

Kinetic tool is available at http://kinetic.noise.gatech.edu/.

NetCore code can be downloaded from https://github.com/frenetic-lang/netcore-1.0.

The lastest version of FlowLog is available at http://cs.brown.edu/research/plt/dl/flowlog/.

Abiteboul S, Hull R, Vianu V (eds) (1995) Foundations of databases: the logical level, 1st edn. Addison-Wesley Longman Publishing Co., Inc, Boston

Al-Shaer E, Al-Haj S (2010) Flowchecker: configuration analysis and verification of federated openflow infrastructures. In: Proc of the 3rd ACM workshop on assurable and usable security configuration, ACM, New York, NY, USA, SafeConfig ’10, pp 37–44. doi:10.1145/1866898.1866905

Al-Shaer E, Alsaleh MN (2011) Configchecker: a tool for comprehensive security configuration analytics. In: Configuration analytics and automation (SAFECONFIG), 2011 4th symposium on, IEEE, Arlington, VA, USA, pp 1–2. doi:10.1109/SafeConfig.2011.6111667

Baldoni G, Melita M, Micalizzi S, Rametta C, Schembra G, Vassallo A (2016) Video broadcasting services over sdn-nfv enabled networks: a prototype. Proc Comput Sci 98:560–565. doi:10.1016/j.procs.2016.09.086 CrossRef

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. SIGPLAN Not 49(6):282–293. doi:10.1145/2666356.2594317 CrossRef

Beckett R, Zou X, Zhang S, Malik S, Rexford J, Walker D (2014) An assertion language for debugging sdn applications. In: Proc of the 3rd Workshop on Hot Topics in Software Defined Networking, ACM, New York, NY, USA, HotSDN ’14, pp 91–96. doi:10.1145/2620728.2620743

Bertot Y, Castran P (2004) Interactive theorem proving and program development, 1st edn. Springer, Berlin. doi:10.1007/978-3-662-07964-5

Bingham B, Bingham J, de Paula FM, Erickson J, Singh G, Reitblatt M (2010) Industrial strength distributed explicit state model checking. In: Proc of the 9th international workshop on parallel and distributed methods in verification and 2nd international workshop on high performance computational systems biology, IEEE, Enschede, Netherlands, pp 28–36. doi:10.1109/PDMC-HiBi.2010.13

Bochmann G, Rayner D, West CH (2010) Some notes on the history of protocol engineering. Comput Netw 54(18):3197–3209. doi:10.1016/j.comnet.2010.05.019 CrossRefMATH

10.

Cai Z, Cox AL, Ng TSE (2011) Maestro: a system for scalable OpenFlow control. Tech. rep., Rice University, Houston, USA, code at https://code.google.com/p/maestro-platform/

11.

Campbell AT, De Meer HG, Kounavis ME, Miki K, Vicente JB, Villela D (1999) A survey of programmable networks. SIGCOMM Comput Commun Rev 29(2):7–23. doi:10.1145/505733.505735 CrossRef

12.

Canini M, Venzano D, Perešíni P, Kostić D, Rexford J (2012) A NICE way to test OpenFlow applications. In: Proc of the 9th USENIX symposium on networked systems design and implementation (NSDI12). USENIX, San Jose, CA, pp 127–140

13.

Cimatti A, Clarke E, Giunchiglia F, Roveri M (1999) NuSMV: a new symbolic model verifier. In: Halbwachs N, Peled D (eds) Proceedings eleventh conference on computer-aided verification (CAV’99), Springer, Trento, Italy, no. 1633 in Lecture Notes in Computer Science, pp 495–499

14.

Della Penna G, Intrigila B, Melatti I, Tronci E, Venturini Zilli M (2004) Exploiting transition locality in automatic verification of finite-state concurrent systems. Int J Softw Tools Technol Transf 6(4):320–341. doi:10.1007/s10009-004-0149-6 CrossRefMATH

15.

Dhawan M, Poddar R, Mahajan K, Mann V (2015) SPHINX: detecting security attacks in software-defined networks. In: Network and distributed system security symposium (NDSS Symposium 2015), USENIX Association, San Diego, CA, USA

16.

El-Hassany A, Miserez J, Bielik P, Vanbever L, Vechev M (2016) Sdnracer: concurrency analysis for software-defined networks. SIGPLAN Not 51(6):402–415. doi:10.1145/2980983.2908124 CrossRef

17.

Feamster N, Rexford J, Zegura E (2014) The road to sdn: an intellectual history of programmable networks. SIGCOMM Comput Commun Rev 44(2):87–98. doi:10.1145/2602204.2602219 CrossRef

18.

Foster N, Harrison R, Freedman MJ, Monsanto C, Rexford J, Story A, Walker D (2011) Frenetic: a network programming language. SIGPLAN Not 46(9):279–291. doi:10.1145/2034574.2034812 CrossRefMATH

19.

Gallardo MM, Martínez J, Merino P (2005) Model checking active networks with spin. Comput Commun 28(6):609–622. doi:10.1016/j.comcom.2004.08.006 CrossRef

20.

Gnesi S, Margaria T (2013) Formal methods for industrial critical systems : a survey of applications. Wiley, Hoboken. doi:10.1002/9781118459898

21.

GSMA’s Network 2020 (2016) Unlocking commercial opportunities from 4G Evolution to 5G. Tech. rep., GSMA Association, London, United Kingdom. http://www.gsma.com/network2020/wp-content/uploads/2016/02/704_GSMA_unlocking_comm_opp_report_v5.pdf

22.

Gude N, Koponen T, Pettit J, Pfaff B, Casado M, McKeown N, Shenker S (2008) Nox: towards an operating system for networks. SIGCOMM Comput Commun Rev 38(3):105–110. doi:10.1145/1384609.1384625, tool avaliable at https://github.com/noxrepo/nox

23.

Guha A, Reitblatt M, Foster N (2013) Machine-verified network controllers. SIGPLAN Not 48(6):483–494. doi:10.1145/2499370.2462178 CrossRef

24.

Handigol N, Heller B, Jeyakumar V, Maziéres D, McKeown N (2012) Where is the debugger for my software-defined network? In: Proc of the 1st Workshop on Hot Topics in Software Defined Networks, ACM, New York, NY, USA, HotSDN ’12, pp 55–60, doi:10.1145/2342441.2342453

25.

Holzmann G (2003) Spin model checker, the: primer and reference manual, 1st edn. Addison-Wesley, Boston

26.

Holzmann GJ (1991) Design and validation of computer protocols. Prentice-Hall, Inc, Upper Saddle River

27.

Jackson D (2012) Software abstractions: logic, language, and analysis. MIT press, London

28.

Karimzadeh M, Sperotto A, Pras A (2014) Software defined networking to improve mobility management performance. In: Sperotto A, Doyen G, Latré S, Charalambides M, Stiller B (eds) Monitoring and securing virtualized networks and services: proc of the 8th IFIP WG 6.6 international conference on autonomous infrastructure, management, and security, AIMS 2014, Brno, Czech Republic, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 118–122, doi:10.1007/978-3-662-43862-6_14

29.

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). USENIX, Lombard, IL, pp 113–126

30.

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). USENIX, Lombard, IL, pp 99–111

31.

Khurshid A, Zhou W, Caesar M, Godfrey PB (2012) Veriflow: verifying network-wide invariants in real time. SIGCOMM Comput Commun Rev 42(4):467–472. doi:10.1145/2377677.2377766 CrossRef

32.

Kim H, Reich J, Gupta A, Shahbaz M, Feamster N, Clark R (2015) Kinetic: verifiable dynamic network control. In: 12th USENIX symposium on networked systems design and implementation (NSDI 15), USENIX Association, Oakland, CA, pp 59–72. https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/kim

33.

Kong C, Alexander P, Dieckman D (2000) Formal modeling of active network nodes using pvs. In: Proc of the 3rd workshop on formal methods in software practice, ACM, New York, NY, USA, FMSP ’00, pp 49–59. doi:10.1145/349360.351130

34.

Lakshman T, Stiliadis D (1998) High-speed policy-based packet forwarding using efficient multi-dimensional range matching. SIGCOMM Comput Commun Rev 28(4):203–214. doi:10.1145/285243.285283 CrossRef

35.

Leucker M, Schallhart C (2009) A brief account of runtime verification. J Logic Algebraic Program 78(5):293–303. doi:10.1016/j.jlap.2008.08.004 CrossRefMATH

36.

Li L, Mao ZM, Rexford J (2012) Toward software-defined cellular networks. In: Proc of the 2012 European workshop on software defined networking, IEEE Computer Society, Washington, DC, USA, EWSDN ’12, pp 7–1. doi:10.1109/EWSDN.2012.28

37.

Linux Fundation Collaborative Projects (2016) Opendaylight. http://www.opendaylight.org/

38.

Mai H, Khurshid A, Agarwal R, Caesar M, Godfrey PB, King ST (2011) Debugging the data plane with anteater. SIGCOMM Comput Commun Rev 41(4):290–301. doi:10.1145/2043164.2018470 CrossRef

39.

Majumdar R, Tetali SD, Wang Z (2014) Kuai: a model checker for software-defined networks. In: Formal methods in computer-aided design (FMCAD), 2014, IEEE, Lausanne, Switzerland, pp 163–170. doi:10.1109/FMCAD.2014.6987609

40.

McKeown N, Anderson T, Balakrishnan H, Parulkar G, Peterson Rexford J, Shenker S, Turner J (2008) Openflow: enabling innovation in campus networks. SIGCOMM Comput Commun Rev 38(2):69–74. doi:10.1145/1355734.1355746 CrossRef

41.

Miserez J, Bielik P, El-Hassany A, Vanbever L, Vechev M (2015) Sdnracer: detecting concurrency violations in software-defined networks. In: Proc of the 1st ACM SIGCOMM symposium on software defined networking research, ACM, New York, NY, USA, SOSR ’15, pp 22:1–22:7. doi:10.1145/2774993.2775004

42.

Monsanto C, Foster N, Harrison R, Walker D (2012) A compiler and run-time system for network programming languages. SIGPLAN Not 47(1):217–230. doi:10.1145/2103621.2103685 CrossRef

43.

de Moura L, Bjørner N (2008) Z3: An efficient smt solver. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction and analysis of systems: 14th international conference (TACAS 2008), Springer, Berlin Heidelberg, pp 337–340. doi:10.1007/978-3-540-78800-3_24

44.

Nayak AK, Reimers A, Feamster N, Clark R (2009) Resonance: dynamic access control for enterprise networks. In: Proc of the 1st ACM Workshop on Research on Enterprise Networking, ACM, New York, NY, USA, WREN ’09, pp 11–18. doi:10.1145/1592681.1592684

45.

Nelson T, Guha A, Dougherty DJ, Fisler K, Krishnamurthi S (2013) A balance of power: expressive, analyzable controller programming. In: Proc the 2nd ACM SIGCOMM workshop on hot topics in software defined networking, ACM, New York, NY, USA, HotSDN ’13, pp 79–84. doi:10.1145/2491185.2491201

46.

Nelson T, Ferguson AD, Scheer MJG, Krishnamurthi S (2014) Tierless programming and reasoning for software-defined networks. In: Proc the 11th USENIX conference on networked systems design and implementation, USENIX Association, Berkeley, CA, USA, NSDI’14, pp 519–531

47.

NGMN Alliance (2015) NGMN 5G White Paper. Tech. rep., Next Generation Mobile Networks, Frankfurt, Germany. www.ngmn.org/uploads/media/NGMN_5G_White_Paper_V1_0.pdf

48.

Nguyen V, Do T, Kim Y (2016) Sdn and virtualization-based lte mobile network architectures: a comprehensive survey. Wirel Pers Commun 86(3):1401–1438. doi:10.1007/s11277-015-2997-7 CrossRef

49.

Nunes BA, Mendonca M, Nguyen XN, Obraczka K, Turletti T (2014) A survey of software-defined networking: past, present, and future of programmable networks. IEEE Commun Surv Tutor 16(3):1617–1634. doi:10.1109/SURV.2014.012214.00180 CrossRef

50.

Open Networking Lab (2013) POX (Python Network Controller) Wiki. https://openflow.stanford.edu/x/TYBr

51.

Paulin-Mohring C (2012) Introduction to the coq proof-assistant for practical software verification. In: Meyer B, Nordio M (eds) Tools for practical software verification, LASER 2011 summerschool, revised tutorial lectures, Springer-Verlag, Elba Island, Italy, no. 7682 in Lecture Notes in Computer Science, pp 45–95

52.

Peled DA, Gries D, Schneider FB (eds) (2001) Software reliability methods. Springer-Verlag New York, Inc, SecaucusMATH

53.

Pentikousis K, Wang Y, Hu W (2013) Mobileflow: toward software-defined mobile networks. IEEE Commun Mag 51(7):44–53. doi:10.1109/MCOM.2013.6553677 CrossRef

54.

Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th annual symposium on foundations of computer science, IEEE Computer Society, Washington, DC, USA, SFCS ’77, pp 46–57. doi:10.1109/SFCS.1977.32

55.

Project Frenetic (2015) Pyretic documentation. http://frenetic-lang.org/pyretic/

56.

Qazi ZA, Tu C, Chiang L, Miao R, Sekar V, Yu M (2013) Simple-fying middlebox policy enforcement using sdn. SIGCOMM Comput Commun Rev 43(4):27–38. doi:10.1145/2534169.2486022 CrossRef

57.

Sethi D, Narayana S, Malik S (2013) Abstractions for model checking SDN controllers. In: Formal methods in computer-aided design, FMCAD, IEEE, Portland, OR, USA, pp 145–148. doi:10.1109/FMCAD.2013.6679403

58.

Shenker S, Casado M, Koponen T, McKeown N et al (2011) The future of networking, and the past of protocols. Open Networking Summit 20:1–30. http://opennetsummit.org/archives/oct11/site/

59.

Shu Z, Wan J, Lin J, Wang S, Li D, Rho S, Yang C (2016) Traffic engineering in software-defined networking: measurement and management. IEEE Access 4:3246–3256. doi:10.1109/ACCESS.2016.2582748 CrossRef

60.

Skowyra R, Lapets A, Bestavros A, Kfoury A (2014) A verification platform for sdn-enabled applications. In: Cloud engineering (IC2E), 2014 IEEE international conference on, IEEE, Boston, Massachussets, USA, pp 337–342. doi:10.1109/IC2E.2014.72

61.

Stehr M, Talcott CL (2002) Plan in maude: specifying an active network programming language. Electr Notes Theor Comput Sci 71:240–260. doi:10.1016/S1571-0661(05)82538-1 CrossRefMATH

62.

Tennenhouse DL, Wetherall D (2007) Towards an active network architecture. SIGCOMM Comput Commun Rev 37(5):81–94. doi:10.1145/1290168.1290180 CrossRef

63.

Tennenhouse DL, Smith JM, Sincoskie WD, Wetheral DJ, Minden GJ (1997) A survey of active network research. IEEE Commun Mag 35(1):80–86CrossRef

64.

Voellmy A, Hudak P (2011) Nettle: taking the sting out of programming network routers. In: International symposium on practical aspects of declarative languages. Springer, Austin, TX, USA, vol 6539, pp 235–249

65.

Wang G, Ng TE, Shaikh A (2012) Programming your network at run-time for big data applications. In: Proceedings of the first workshop on hot topics in software defined networks, ACM, New York, NY, USA, HotSDN ’12, pp 103–108. doi:10.1145/2342441.2342462

66.

West CH, Zafiropulo P (1978) Automated validation of a communications protocol: the ccitt x.21 recommendation. IBM J Res Dev 22(1):60–71. doi:10.1147/rd.221.0060

67.

J Woodcock, PG Larsen, J Bicarregui, Fitzgerald J (2009) Formal methods: practice and experience. ACM Comput Surv 41(4):19:1–19:36. doi:10.1145/1592434.1592436

68.

Xie GG, Zhan J, Maltz DA, Zhang H, Greenberg A, Hjalmtysson G, Rexford J (2005) On static reachability analysis of ip networks. In: Proc IEEE 24th annual joint conference of the IEEE computer and communications societies, IEEE, Miami, FL, vol 3, pp 2170–2183. doi:10.1109/INFCOM.2005.1498492

69.

Zope N, Pawar S, Saquib Z (2016) Firewall and load balancing as an application of sdn. In: 2016 Conference on advances in signal processing (CASP), pp 354–359. doi:10.1109/CASP.2016.7746195

Titel: A characterisation of verification tools for software defined networks
verfasst von: Leticia Lavado
Laura Panizo
María-del-Mar Gallardo
Pedro Merino
Publikationsdatum: 29.07.2017
Verlag: Springer International Publishing
Erschienen in: Journal of Reliable Intelligent Environments / Ausgabe 3/2017
Print ISSN: 2199-4668
Elektronische ISSN: 2199-4676
DOI: https://doi.org/10.1007/s40860-017-0045-y

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 3/2017

A secure remote user authentication scheme for smart cities e-governance applications

Reliability and human factors in Ambient Assisted Living environments

Editorial

Self-adaptive smart spaces by proactive means–end reasoning

Premium Partner