Advertisement

SDN-Actors: Modeling and Verification of SDN Programs

  • Elvira Albert
  • Miguel Gómez-Zamalloa
  • Albert Rubio
  • Matteo Sammartino
  • Alexandra Silva
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

Software-Defined Networking (SDN) is a recent networking paradigm that has become increasingly popular in the last decade. It gives unprecedented control over the global behavior of the network and provides a new opportunity for formal methods. Much work has appeared in the last few years on providing bridges between SDN and verification. This paper advances this research line and provides a link between SDN and traditional work on formal methods for verification of distributed software—actor-based modelling. We show how SDN programs can be seamlessly modelled using actors, and thus existing advanced model checking techniques developed for actors can be directly applied to verify a range of properties of SDN networks, including consistency of flow tables, violation of safety policies, and forwarding loops.

References

  1. 1.
    The ABS tool suite. http://abs-models.org
  2. 2.
    Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)Google Scholar
  3. 3.
    Albert, E., Arenas, P., de la Banda, M.G., Gómez-Zamalloa, M., Stuckey, P.J.: Context-sensitive dynamic partial order reduction. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 526–543. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63387-9_26CrossRefGoogle Scholar
  4. 4.
    Albert, E., Gómez-Zamalloa, M., Isabel, M.: SYCO: a systematic testing tool for concurrent objects. In: CC, pp. 269–270 (2016)Google Scholar
  5. 5.
    Albert, E., Gómez-Zamalloa, M., Rubio, A., Sammartino, M., Silva, A.: SDN-Actors: Modeling and Verification of SDN Programs. Technical report (2018). http://costa.ls.fi.upm.es/papers/costa/AlbertGRSS18TR.pdf
  6. 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: PLDI, pp. 282–293 (2014)CrossRefGoogle Scholar
  7. 7.
    Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: POPL, pp. 651–662 (2015)CrossRefGoogle Scholar
  8. 8.
    Canini, M., Venzano, D., Peresíni, P., Kostic, D., Rexford, J.: A NICE way to test OpenFlow applications. In: NSDI, pp. 127–140 (2012)Google Scholar
  9. 9.
    Christakis, M., Gotovos, A., Sagonas, K.F.: Systematic testing for detecting concurrency errors in Erlang programs. In: ICST, pp. 154–163 (2013)Google Scholar
  10. 10.
    de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-71316-6_22CrossRefGoogle Scholar
  11. 11.
    Eckhardt, J., Mühlbauer, T., Meseguer, J., Wirsing, M.: Statistical model checking for composite actor systems. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 143–160. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37635-1_9CrossRefGoogle Scholar
  12. 12.
    El-Hassany, A., Miserez, J., Bielik, P., Vanbever, L., Vechev, M.T.: SDNRacer: concurrency analysis for software-defined networks. In: POPL, pp. 402–415 (2016)CrossRefGoogle Scholar
  13. 13.
    Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp. 110–121 (2005)CrossRefGoogle Scholar
  14. 14.
    Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-25271-6_8CrossRefGoogle Scholar
  15. 15.
    Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: NSDI, pp. 113–126 (2012)Google Scholar
  16. 16.
    Lauterburg, S., Karmani, R.K., Marinov, D., Agha, G.: Basset: a tool for systematic testing of actor programs. In: SIGSOFT FSE, pp. 363–364 (2010)Google Scholar
  17. 17.
    Liang, H., Feng, X.: A program logic for concurrent objects under fair scheduling. In: POPL, pp. 385–399 (2016)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Majumdar, R., Tetali, S.D., Wang, Z.: Kuai: a model checker for software-defined networks. In: FMCAD, pp. 163–170 (2014)Google Scholar
  19. 19.
    Openflow switch specification, October 2013. Version 1.4.0. http://www.opennetworking.org/software-defined-standards/specifications
  20. 20.
    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_2CrossRefGoogle Scholar
  21. 21.
    Sen, K., Agha, G.: Automated systematic testing of open distributed programs. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 339–356. Springer, Heidelberg (2006).  https://doi.org/10.1007/11693017_25CrossRefGoogle Scholar
  22. 22.
    Sethi, D., Narayana, S., Malik, S.: Abstractions for model checking SDN controllers. In: FMCAD, pp. 145–148 (2013)Google Scholar
  23. 23.
    Tasharofi, S., et al.: TransDPOR: a novel dynamic partial-order reduction technique for testing actor programs. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE -2012. LNCS, vol. 7273, pp. 219–234. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-30793-5_14CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Elvira Albert
    • 1
  • Miguel Gómez-Zamalloa
    • 1
  • Albert Rubio
    • 2
  • Matteo Sammartino
    • 3
  • Alexandra Silva
    • 3
  1. 1.Complutense University of MadridMadridSpain
  2. 2.Universitat Politècnica de CatalunyaBarcelonaSpain
  3. 3.University College LondonLondonUK

Personalised recommendations