Skip to main content
SpringerLink
Log in
Book cover

International Conference on Integrated Formal Methods

IFM 2018: Integrated Formal Methods pp 172–193Cite as

Formal Modelling of Software Defined Networking

  • Conference paper
  • First Online:

  • 766 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11023))

Abstract

This paper investigates the application of Carma, a recently developed quantitative process-algebra-based modelling language, to the stochastic modelling of software defined networking (SDN). In SDN, a single controller (or hierarchy of controllers) determines the behaviour of the switches that forward traffic through the network, and it is used in a variety of settings including cloud and data centres. This research is the initial phase of developing a methodology for agile formal modelling of performance and security aspects of SDN, and focusses on the fat-tree network topology. The results demonstrate that the Carma language and its software tools which include the MultiVeStA statistical model checker provide a good basis for modelling SDN.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Abd Alrahman, Y., De Nicola, R., Loreti, M.: On the power of attribute-based communication. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 1–18. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-39570-8_1

    Chapter  Google Scholar 

  2. Al-Fares, M., Loukissas, A., Vahdat, A.: A scalable, commodity data center network architecture. In: Proceedings of the ACM SIGCOMM 2008, pp. 63–74 (2008)

    Google Scholar 

  3. Al-Shaer, E., Al-Haj, S.: FlowChecker: configuration analysis and verification of federated OpenFlow infrastructures. In: Proceedings of SafeConfig 2010, pp. 37–44 (2010)

    Google Scholar 

  4. Anderson, C., et al.: NetKAT: semantic foundations for networks. SIGPLAN Not. 49, 113–126 (2014)

    MATH  Google Scholar 

  5. Bilal, K., et al.: Quantitative comparisons of the state-of-the-art data center architectures. Concurr. Comput.: Pract. Exp. 25, 1771–1783 (2013)

    Article  Google Scholar 

  6. Calheiros, R., Ranjan, R., Beloglazov, A., Rose, C.D., Buyya, R.: CloudSim: a toolkit for modeling and simulation of cloud computing environments and evaluation of resource provisioning algorithms. Softw. Pract. Exp. 41, 23–50 (2011)

    Article  Google Scholar 

  7. Canini, M., Venzano, D., Perešíni, P., Kostić, D., Rexford, J.: A NICE way to test OpenFlow applications. In: Proceedings of NSDI 2012 (2012)

    Google Scholar 

  8. Castro, R., Kofman, E.: An integrative approach for hybrid modeling, simulation and control of data networks based on the DEVS formalism. In: Modeling and Simulation of Computer Networks and Systems, pp. 505–551. Morgan Kaufmann (2015)

    Google Scholar 

  9. Chaves, L., Garcia, I., Madeira, E.: OFSwitch13: enhancing ns-3 with OpenFlow 1.3 support. In: Proceedings of WNS3 2016, pp. 33–40 (2016)

    Google Scholar 

  10. Chen, W., Lin, Y., Galpin, V., Nigam, V., Lee, M., Aspinall, D.: Formal analysis of Sneak-Peek: a data centre attack and its mitigations. In: IFIP SEC 2018 (2018, to appear)

    Google Scholar 

  11. Ciocchetta, F., Hillston, J.: Bio-PEPA for epidemiological models. Electron. Not. Theor. Comput. Sci. 261, 43–69 (2010)

    Article  Google Scholar 

  12. Dacier, M.C., Dietrich, S., Kargl, F., Knig, H.: Network attack detection and defense (Dagstuhl Seminar 16361). Dagstuhl Rep. 6(9), 1–28 (2017)

    Google Scholar 

  13. De Nicola, R., Latella, D., Loreti, M., Massink, M.: A uniform definition of stochastic process calculi. ACM Comput. Surv. 46, 5 (2013)

    Article  Google Scholar 

  14. De Nicola, R., Loreti, M., Pugliese, R., Tiezzi, F.: A formal approach to autonomic systems programming: the SCEL language. ACM TAAS 9, 7:1–7:29 (2014)

    Google Scholar 

  15. Farhadi, H., Lee, H., Nakao, A.: Software-defined networking: a survey. Comput. Netw. 81, 79–95 (2015)

    Article  Google Scholar 

  16. Fehnker, A., van Glabbeek, R., Höfner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 295–315. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28869-2_15

    Chapter  Google Scholar 

  17. Fernandes, S.: Performance Evaluation for Network Services, Systems and Protocols. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-319-54521-9

    Book  Google Scholar 

  18. Galpin, V.: Modelling network performance with a spatial stochastic process algebra. In: Proceedings of AINA 2009, pp. 41–49 (2009)

    Google Scholar 

  19. Galpin, V.: Modelling ambulance deployment with Carma. In: Lluch Lafuente, A., Proença, J. (eds.) COORDINATION 2016. LNCS, vol. 9686, pp. 121–137. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-39519-7_8

    Chapter  Google Scholar 

  20. Galpin, V., et al.: CaSL at work. QUANTICOL Deliverable D4.3 (2017). http://blog.inf.ed.ac.uk/quanticol/deliverables

  21. Galpin, V., Zon, N., Wilsdorf, P., Gilmore, S.: Mesoscopic modelling of pedestrian movement using CARMA and its tools. ACM TOMACS 28, 11:1–11:26 (2018)

    Article  MathSciNet  Google Scholar 

  22. Heller, B., Sherwood, R., McKeown, N.: The controller placement problem. In: Proceedings of HotSDN 2012, pp. 7–12 (2012)

    Google Scholar 

  23. Hillston, J.: A compositional approach to performance modelling. CUP (1996)

    Google Scholar 

  24. Hillston, J., Loreti, M.: Specification and analysis of open-ended systems with CARMA. In: Weyns, D., Michel, F. (eds.) E4MAS 2014. LNCS (LNAI), vol. 9068, pp. 95–116. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23850-0_7

    Chapter  Google Scholar 

  25. Hillston, J., Loreti, M.: Carma eclipse plug-in: a tool supporting design and analysis of collective adaptive systems. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 167–171. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43425-4_12

    Chapter  Google Scholar 

  26. Ivey, J., Yang, H., Zhang, C., Riley, G.: Comparing a scalable SDN simulation framework built on ns-3 and DCE with existing SDN simulators and emulators. In: Proceedings of SIGSIM-PADS 2016, pp. 153–164 (2016)

    Google Scholar 

  27. Khurshid, A., Zou, X., Zhou, W., Caesar, M., Godfrey, P.: VeriFlow: verifying network-wide invariants in real time. In: Proceedings of NSDI 2013 (2013)

    Google Scholar 

  28. Kouzapas, D., Philippou, A.: A process calculus for dynamic networks. In: Bruni, R., Dingel, J. (eds.) FMOODS/FORTE 2011. LNCS, vol. 6722, pp. 213–227. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21461-5_14

    Chapter  Google Scholar 

  29. Lantz, B., Heller, B., McKeown, N.: A network in a laptop: rapid prototyping for software-defined networks. In: Proceedings of Hotnets-IX, pp. 19:1–19:6 (2010)

    Google Scholar 

  30. Laurito, A., Bonaventura, M., Astigarraga, M., Castro, R.: TopoGen: a network topology generation architecture with application to automating simulations of software defined networks. In: Proceedings of WSC 2017, pp. 1049–1060 (2017)

    Google Scholar 

  31. Lemos, M., Dantas, Y., Fonseca, I., Nigam, V.: On the accuracy of formal verification of selective defenses for TDoS attacks. J. Log. Algebraic Methods Program. 94, 45–67 (2018)

    Article  MathSciNet  Google Scholar 

  32. Loreti, M., Hillston, J.: Modelling and analysis of collective adaptive systems with CARMA and its tools. In: Bernardo, M., De Nicola, R., Hillston, J. (eds.) SFM 2016. LNCS, vol. 9700, pp. 83–119. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-34096-8_4

    Chapter  Google Scholar 

  33. Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P., King, S.: Debugging the data plane with Anteater. In: Proceedings of SIGCOMM 2011 (2011)

    Google Scholar 

  34. Majumdar, R., Tetali, S., Wang, Z.: Kuai: a model checker for software-defined networks. In: Proceedings of FMCAD 2014, pp. 27:163–27:170 (2014)

    Google Scholar 

  35. Pascoal, T.A., Dantas, Y.G., Fonseca, I.E., Nigam, V.: Slow TCAM Exhaustion DDoS Attack. In: De Capitani di Vimercati, S., Martinelli, F. (eds.) SEC 2017. IAICT, vol. 502, pp. 17–31. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-58469-0_2

    Chapter  Google Scholar 

  36. Prakash, C., et al.: PGA: using graphs to express and automatically reconcile network policies. In: Proceedings of SIGCOMM 2015, pp. 29–42 (2015)

    Google Scholar 

  37. Rotsos, C., Sarrar, N., Uhlig, S., Sherwood, R., Moore, A.W.: OFLOPS: an open framework for OpenFlow switch evaluation. In: Taft, N., Ricciato, F. (eds.) PAM 2012. LNCS, vol. 7192, pp. 85–95. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28537-0_9

    Chapter  Google Scholar 

  38. Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: Proceedings of ValueTools 2013, pp. 310–315 (2013)

    Google Scholar 

  39. Smolka, S., Kumar, P., Foster, N., Kozen, D., Silva, A.: Cantor meets Scott: semantic foundations for probabilistic networks. In: Proceedings of POPL 2017, pp. 557–571 (2017)

    Google Scholar 

  40. Son, S., Shin, S., Yegneswaran, V., Porras, P., Gu, G.: Model checking invariant security properties in OpenFlow. In: Proceedings of IEEE ICC 2013, pp. 1974–1979 (2013)

    Google Scholar 

  41. Tahir, R., et al.: Sneak-Peek: high speed covert channels in data center networks. In: Proceedings of IEEE INFOCOM 2016, pp. 1–9 (2016)

    Google Scholar 

  42. Zhou, W., Jin, D., Croft, J., Caesar, M., Godfrey, P.: Enforcing customizable consistency properties in software-defined networks. In: Proceedings of NSDI 2015 (2015)

    Google Scholar 

  43. Zoń, N., Gilmore, S., Hillston, J.: Rigorous graphical modelling of movement in collective adaptive systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 674–688. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_47

    Chapter  Google Scholar 

Download references

Acknowledgements

This work is supported by the EPSRC project Robustness-as-Evolvability, EP/L02277X/1 and the EPSRC Platform Grant EP/N014758/1. Thanks to David Aspinall, Wei Chen and Henry Clausen for their useful comments. The Carma models and experimental data can be obtained from groups.inf.ed.ac.uk/security/RasE/.

Author information

Authors and Affiliations

  1. Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh, Edinburgh, UK

    Vashti Galpin

Authors
  1. Vashti Galpin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vashti Galpin .

Editor information

Editors and Affiliations

  1. Università della Svizzera Italiana, Lugano, Switzerland

    Carlo A. Furia

  2. University of Queensland, Brisbane, Queensland, Australia

    Kirsten Winter

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Galpin, V. (2018). Formal Modelling of Software Defined Networking. In: Furia, C., Winter, K. (eds) Integrated Formal Methods. IFM 2018. Lecture Notes in Computer Science(), vol 11023. Springer, Cham. https://doi.org/10.1007/978-3-319-98938-9_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-98938-9_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-98937-2

  • Online ISBN: 978-3-319-98938-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation