×

zbMATH — the first resource for mathematics

Model checking data flows in concurrent network updates. (English) Zbl 1437.68115
Chen, Yu-Fang (ed.) et al., Automated technology for verification and analysis. 17th international symposium, ATVA 2019, Taipei, Taiwan, October 28–31, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11781, 515-533 (2019).
Summary: 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.
For the entire collection see [Zbl 1428.68012].
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
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 · Zbl 1046.68578
[4] Biere, A., Heljanko, K., Wieringa, S.: AIGER 1.9 and beyond. Tech. Rep. 11/2. Johannes Kepler University, Linz (2011)
[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 · Zbl 1317.68109
[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
[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 · Zbl 1393.68020
[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
[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
[13] Engelfriet, J.: Branching processes of Petri nets. Acta Informatica 28(6), 575-591 (1991). https://doi.org/10.1007/BF01463946 · Zbl 0743.68106
[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 · Zbl 1153.68035
[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)
[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
[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 · Zbl 1362.68211
[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 · Zbl 1381.68161
[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 · Zbl 1323.68114
[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 · Zbl 0762.68004
[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
[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
[27] Kordon, F., et al.: Complete Results for the 2019 Edition of the Model Checking Contest (2019)
[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
[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
[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
[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
[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
[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 · Zbl 1346.68027
[37] Reisig, W.: Petri Nets: An Introduction. Springer, Berlin (1985). https://doi.org/10.1007/978-3-642-69968-9 · Zbl 0555.68033
[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 · Zbl 0986.68684
[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
[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.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.