Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Automated Technology for Verification and Analysis

ATVA 2019: Automated Technology for Verification and Analysis pp 515–533Cite as

Model Checking Data Flows in Concurrent Network Updates

  • Conference paper
  • First Online:

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

Abstract

We present a model checking approach for the verification of data flow correctness in networks during concurrent updates of the network configuration. This verification problem is of great importance for software-defined networking (SDN), where errors can lead to packet loss, black holes, and security violations. Our approach is based on a specification of temporal properties of individual data flows, such as the requirement that the flow is free of cycles. We check whether these properties are simultaneously satisfied for all active data flows while the network configuration is updated. To represent the behavior of the concurrent network controllers and the resulting evolutions of the configurations, we introduce an extension of Petri nets with a transit relation, which characterizes the data flow caused by each transition of the Petri net. For safe Petri nets with transits, we reduce the verification of temporal flow properties to a circuit model checking problem that can be solved with effective verification techniques like IC3, interpolation, and bounded model checking. We report on encouraging experiments with a prototype implementation based on the hardware model checker ABC.

This work was supported by the German Research Foundation (DFG) Grant Petri Games (392735815) and the Collaborative Research Center “Foundations of Perspicuous Software Systems” (TRR 248, 389792660), and by the European Research Council (ERC) Grant OSARES (683300).

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. Ball, T., et al.: Vericon: towards verifying controller programs in software-defined networks. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom, 9–11 June 2014, pp. 282–293 (2014). https://doi.org/10.1145/2594291.2594317

  2. Berkeley Logic Synthesis and Verification Group: ABC: a system for sequential synthesis and verification, Release YMMDD. Version 1.01, Release 81030. http://www.eecs.berkeley.edu/~alanmi/abc/

  3. Biere, A., Clarke, E., Raimi, R., Zhu, Y.: Verifying safety properties of a PowerPC\(-\) microprocessor using symbolic model checking without BDDs. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 60–71. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48683-6_8

    Chapter  Google Scholar 

  4. Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep. 11/2. Johannes Kepler University, Linz (2011)

    Google Scholar 

  5. Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_7

    Chapter  Google Scholar 

  6. Canini, M., Venzano, D., Perešíni, P., Kostić, D., Rexford, J.: A NICE way to test openflow applications. In: Proceedings of NSDI 2012, San Jose, CA, pp. 127–140 (2012). http://dl.acm.org/citation.cfm?id=2228298.2228312

  7. Casado, M., Foster, N., Guha, A.: Abstractions for software-defined networks. Commun. ACM 57(10), 86–95 (2014). https://doi.org/10.1145/2661061.2661063

    Article  Google Scholar 

  8. Černý, P., Foster, N., Jagnik, N., McClurg, J.: Optimal consistent network updates in polynomial time. In: Gavoille, C., Ilcinkas, D. (eds.) DISC 2016. LNCS, vol. 9888, pp. 114–128. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53426-7_9

    Chapter  Google Scholar 

  9. Claessen, K., Eén, N., Sterin, B.: A circuit approach to LTL model checking. In: Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, 20–23 October 2013, pp. 53–60 (2013). http://ieeexplore.ieee.org/document/6679391/

  10. Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54792-8_15

    Chapter  Google Scholar 

  11. Eén, N., Mishchenko, A., Brayton, R.K.: Efficient implementation of property directed reachability. In: Proceedings of FMCAD, pp. 125–134 (2011). http://dl.acm.org/citation.cfm?id=2157675

  12. El-Hassany, A., Tsankov, P., Vanbever, L., Vechev, M.: Network-wide configuration synthesis. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 261–281. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_14

    Chapter  Google Scholar 

  13. Engelfriet, J.: Branching processes of Petri nets. Acta Informatica 28(6), 575–591 (1991). https://doi.org/10.1007/BF01463946

    Article  MathSciNet  MATH  Google Scholar 

  14. Esparza, J., Heljanko, K.: Unfoldings - A Partial-Order Approach to Model Checking. Springer, Berlin (2008). https://doi.org/10.1007/978-3-540-77426-6

    Book  MATH  Google Scholar 

  15. Finkbeiner, B., Gieseking, M., Hecking-Harbusch, J., Olderog, E.: Model checking data flows in concurrent network updates (full version). arXiv preprint. arXiv:1907.11061 (2019)

    Chapter  Google Scholar 

  16. Finkbeiner, B., Gieseking, M., Olderog, E.-R.: Adam: causality-based synthesis of distributed systems. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 433–439. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_25

    Chapter  Google Scholar 

  17. Finkbeiner, B., Olderog, E.: Petri games: synthesis of distributed systems with causal memory. Inf. Comput. 253, 181–203 (2017). https://doi.org/10.1016/j.ic.2016.07.006

    Article  MathSciNet  MATH  Google Scholar 

  18. Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for model checking HyperLTL and HyperCTL\(^*\). In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30–48. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_3

    Chapter  Google Scholar 

  19. Förster, K., Mahajan, R., Wattenhofer, R.: Consistent updates in software defined networks: on dependencies, loop freedom, and blackholes. In: Proceedings of IFIP Networking Conference, Networking 2016 and Workshops, Vienna, Austria, 17–19 May 2016, pp. 1–9 (2016). https://doi.org/10.1109/IFIPNetworking.2016.7497232

  20. Foster, N., et al.: Frenetic: a network programming language. In: Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, 19–21 September 2011, pp. 279–291 (2011). https://doi.org/10.1145/2034773.2034812

  21. Gieseking, M., Hecking-Harbusch, J.: AdamMC - a model checker for Petri nets with transits and flow-LTL (2019). https://doi.org/10.6084/m9.figshare.8313344

  22. Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, vol. 1. Springer, Berlin (1992). https://doi.org/10.1007/978-3-662-03241-1

    Book  MATH  Google Scholar 

  23. Jin, X., et al.: Dynamic scheduling of network updates. In: Proceedings of SIGCOMM 2014, Chicago, Illinois, USA, pp. 539–550 (2014). https://doi.org/10.1145/2619239.2626307

  24. Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_61

    Chapter  Google Scholar 

  25. Katta, N.P., Rexford, J., Walker, D.: Incremental consistent updates. In: Proceedings of HotSDN 2013, Hong Kong, China, pp. 49–54. ACM, New York (2013). https://doi.org/10.1145/2491185.2491191

  26. Knight, S., Nguyen, H.X., Falkner, N., Bowden, R.A., Roughan, M.: The internet topology zoo. IEEE J. Sel. Areas Commun. 29(9), 1765–1775 (2011). https://doi.org/10.1109/JSAC.2011.111002

    Article  Google Scholar 

  27. Kordon, F., et al.: Complete Results for the 2019 Edition of the Model Checking Contest (2019)

    Google Scholar 

  28. Kreutz, D., Ramos, F.M.V., Veríssimo, P.J.E., Rothenberg, C.E., Azodolmolky, S., Uhlig, S.: Software-defined networking: a comprehensive survey. Proceedings of the IEEE, vol. 103, no. 1, pp. 14–76 (2015). https://doi.org/10.1109/JPROC.2014.2371999

    Article  Google Scholar 

  29. Liu, H.H., Wu, X., Zhang, M., Yuan, L., Wattenhofer, R., Maltz, D.A.: zUpdate: updating data center networks with zero loss. In: Proceedings of ACM SIGCOMM 2013 Conference, SIGCOMM 2013, Hong Kong, China, 12–16 August 2013, pp. 411–422 (2013). https://doi.org/10.1145/2486001.2486005

  30. Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P.B., King, S.T.: Debugging the data plane with anteater. SIGCOMM Comput. Commun. Rev. 41(4), 290–301 (2011). https://doi.org/10.1145/2043164.2018470

    Article  Google Scholar 

  31. Majumdar, R., Tetali, S.D., Wang, Z.: Kuai: a model checker for software-defined networks. In: Proceedings of FMCAD, pp. 163–170 (2014). https://doi.org/10.1109/FMCAD.2014.6987609

  32. McClurg, J., Hojjat, H., Černý, P.: Synchronization synthesis for network programs. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 301–321. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_16

    Chapter  Google Scholar 

  33. McKeown, N., et al.: Openflow: enabling innovation in campus networks. Comput. Commun. Rev. 38(2), 69–74 (2008). https://doi.org/10.1145/1355734.1355746

    Article  Google Scholar 

  34. McMillan, K.L.: Craig interpolation and reachability analysis. In: Proceredings of Static Analysis, 10th International Symposium, SAS 2003, San Diego, CA, USA, 11–13 June 2003, p. 336 (2003). https://doi.org/10.1007/3-540-44898-5_18

    Chapter  Google Scholar 

  35. Monsanto, C., Reich, J., Foster, N., Rexford, J., Walker, D.: Composing software defined networks. In: Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2013, Lombard, IL, USA, 2–5 April 2013, pp. 1–13 (2013). https://www.usenix.org/conference/nsdi13/technical-sessions/presentation/monsanto

  36. Padon, O., Immerman, N., Karbyshev, A., Lahav, O., Sagiv, M., Shoham, S.: Decentralizing SDN policies. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 5–17 January 2015, pp. 663–676 (2015). https://doi.org/10.1145/2676726.2676990

  37. Reisig, W.: Petri Nets: An Introduction. Springer, Berlin (1985). https://doi.org/10.1007/978-3-642-69968-9

    Book  MATH  Google Scholar 

  38. Reitblatt, M., Canini, M., Guha, A., Foster, N.: Fattire: declarative fault tolerance for software-defined networks. In: Proceedings of the Second ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking, HotSDN 2013, The Chinese University of Hong Kong, Hong Kong, China, 16 August 2013, pp. 109–114 (2013). https://doi.org/10.1145/2491185.2491187

  39. Reitblatt, M., Foster, N., Rexford, J., Schlesinger, C., Walker, D.: Abstractions for network update. In: Proceedings of ACM SIGCOMM 2012 Conference, SIGCOMM 2012, Helsinki, Finland, 13–17 August 2012, pp. 323–334 (2012). https://doi.org/10.1145/2342356.2342427

  40. Schmidt, K.: LoLA a low level analyser. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 465–474. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44988-4_27

    Chapter  Google Scholar 

  41. Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231–237. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_20

    Chapter  Google Scholar 

  42. Tsankov, P., Dashti, M.T., Basin, D.: Access control synthesis for physical spaces. In: Proceedings of IEEE 29th Computer Security Foundations Symposium, CSF 2016, pp. 443–457 (2016). https://doi.org/10.1109/CSF.2016.38

  43. Wang, A., Moarref, S., Loo, B.T., Topcu, U., Scedrov, A.: Automated synthesis of reactive controllers for software-defined networks. In: Proceedings of 21st IEEE International Conference on Network Protocols, ICNP 2013, Göttingen, Germany, 7–10 October 2013, pp. 1–6 (2013). https://doi.org/10.1109/ICNP.2013.6733666

Download references

Author information

Authors and Affiliations

  1. Saarland University, Saarbrücken, Germany

    Bernd Finkbeiner & Jesko Hecking-Harbusch

  2. University of Oldenburg, Oldenburg, Germany

    Manuel Gieseking & Ernst-Rüdiger Olderog

Authors
  1. Bernd Finkbeiner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Manuel Gieseking
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jesko Hecking-Harbusch
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Ernst-Rüdiger Olderog
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Manuel Gieseking .

Editor information

Editors and Affiliations

  1. Institute of Information Science, Academia Sinica, Taipei, Taiwan

    Yu-Fang Chen

  2. DENSO AUTOMOTIVE Deutschland GmbH, Eching, Germany

    Chih-Hong Cheng

  3. Institute of Computer Science, TU München, Munich, Germany

    Javier Esparza

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Finkbeiner, B., Gieseking, M., Hecking-Harbusch, J., Olderog, ER. (2019). Model Checking Data Flows in Concurrent Network Updates. In: Chen, YF., Cheng, CH., Esparza, J. (eds) Automated Technology for Verification and Analysis. ATVA 2019. Lecture Notes in Computer Science(), vol 11781. Springer, Cham. https://doi.org/10.1007/978-3-030-31784-3_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-31784-3_30

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-31783-6

  • Online ISBN: 978-3-030-31784-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation