Explaining safety failures in NetKAT. (English) Zbl 1518.68046
Summary: This work introduces a concept of explanations with respect to the violation of safe behaviours within software defined networks (SDNs) expressible in NetKAT. The latter is a network programming language based on a well-studied mathematical structure, namely, Kleene Algebra with Tests (KAT). Amongst others, the mathematical foundation of NetKAT gave rise to a sound and complete equational theory. In our setting, a safe behaviour is characterised by a NetKAT policy, or program, which does not enable forwarding packets from an ingress \(i\) to an undesirable egress \(e\). We show how explanations for safety violations can be derived in an equational fashion, according to a modification of the existing NetKAT axiomatisation. We propose an approach based on the Maude system for actually computing the undesired behaviours witnessing the forwarding of packets from \(i\) to \(e\) as above. SDN-SafeCheck is a tool based on Maude equational theories satisfying important properties such as Church-Rosser and termination. SDN-SafeCheck automatically identifies all the undesired behaviours leading to \(e\), covering forwarding paths up to a user specified size.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 03B70 | Logic in computer science |
| 68N15 | Theory of programming languages |
| 68N19 | Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) |
References:
| [1] | Buckl, C.; Knoll, A.; Schieferdecker, I.; Zander, J., Model-based analysis and development of dependable systems, (Giese, H.; Karsai, G.; Lee, E.; Rumpe, B.; Schätz, B., Model-Based Engineering of Embedded Real-Time Systems - International. Model-Based Engineering of Embedded Real-Time Systems - International, Dagstuhl Workshop, Dagstuhl Castle, Germany, November 4-9, 2007, Revised Selected Papers. Model-Based Engineering of Embedded Real-Time Systems - International. Model-Based Engineering of Embedded Real-Time Systems - International, Dagstuhl Workshop, Dagstuhl Castle, Germany, November 4-9, 2007, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6100 (2007), Springer), 271-293 |
| [2] | McKeown, N.; Anderson, T.; Balakrishnan, H.; Parulkar, G. M.; Peterson, L. L.; Rexford, J.; Shenker, S.; Turner, J. S., OpenFlow: enabling innovation in campus networks, Comput. Commun. Rev., 38, 2, 69-74 (2008) |
| [3] | Foster, N.; Harrison, R.; Freedman, M. J.; Monsanto, C.; Rexford, J.; Story, A.; Walker, D., Frenetic: a network programming language, (Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming. Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011 (2011)), 279-291 · Zbl 1323.68114 |
| [4] | Voellmy, A.; Hudak, P., Nettle: a language for configuring routing networks, (Taha, W. M., Domain-Specific Languages, IFIP TC 2 Working Conference, Proceedings. Domain-Specific Languages, IFIP TC 2 Working Conference, Proceedings, DSL 2009, Oxford, UK, July 15-17, 2009. Domain-Specific Languages, IFIP TC 2 Working Conference, Proceedings. Domain-Specific Languages, IFIP TC 2 Working Conference, Proceedings, DSL 2009, Oxford, UK, July 15-17, 2009, Lecture Notes in Computer Science, vol. 5658 (2009), Springer), 211-235 |
| [5] | Voellmy, A.; Wang, J.; Yang, Y. R.; Ford, B.; Hudak, P., Maple: simplifying SDN programming using algorithmic policies, (ACM SIGCOMM 2013 Conference. ACM SIGCOMM 2013 Conference, SIGCOMM’13, Hong Kong, China, August 12-16, 2013 (2013)), 87-98 |
| [6] | Anderson, C. J.; Foster, N.; Guha, A.; Jeannin, J.; Kozen, D.; Schlesinger, C.; Walker, D., NetKAT: semantic foundations for networks, (The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014 (2014)), 113-126 · Zbl 1284.68100 |
| [7] | Foster, N.; Kozen, D.; Milano, M.; Silva, A.; Thompson, L., A coalgebraic decision procedure for NetKAT, (Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015 (2015)), 343-355 · Zbl 1346.68132 |
| [8] | Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C. L., The Maude 2.0 system, (Nieuwenhuis, R., Rewriting Techniques and Applications, 14th International Conference, Proceedings. Rewriting Techniques and Applications, 14th International Conference, Proceedings, RTA 2003, Valencia, Spain, June 9-11, 2003. Rewriting Techniques and Applications, 14th International Conference, Proceedings. Rewriting Techniques and Applications, 14th International Conference, Proceedings, RTA 2003, Valencia, Spain, June 9-11, 2003, Lecture Notes in Computer Science, vol. 2706 (2003), Springer), 76-87 · Zbl 1038.68559 |
| [9] | Pelle, I.; Gulyás, A., An extensible automated failure localization framework using NetKAT, Felix, and SDN traceroute, Future Internet, 11, 5 (2019) |
| [10] | Deng, Y.; Zhang, M.; Lei, G., An algebraic approach to automatic reasoning for NetKAT based on its operational semantics, (Duan, Z.; Ong, L., Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, Proceedings. Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, Proceedings, ICFEM 2017, Xi’an, China, November 13-17, 2017. Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, Proceedings. Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods, Proceedings, ICFEM 2017, Xi’an, China, November 13-17, 2017, Lecture Notes in Computer Science, vol. 10610 (2017), Springer), 464-480 |
| [11] | Caltais, G., Explaining SDN failures via axiomatisations, (Marin, M.; Craciun, A., Proceedings Third Symposium on Working Formal Methods. Proceedings Third Symposium on Working Formal Methods, FROM 2019, Timişoara, Romania, 3-5 September 2019. Proceedings Third Symposium on Working Formal Methods. Proceedings Third Symposium on Working Formal Methods, FROM 2019, Timişoara, Romania, 3-5 September 2019, EPTCS, vol. 303 (2019)), 48-60 |
| [12] | Gill, P.; Arlitt, M. F.; Li, Z.; Mahanti, A., The flattening internet topology: natural evolution, unsightly barnacles or contrived collapse?, (Claypool, M.; Uhlig, S., Passive and Active Network Measurement, 9th International Conference, Proceedings. Passive and Active Network Measurement, 9th International Conference, Proceedings, PAM 2008, Cleveland, OH, USA, April 29-30, 2008. Passive and Active Network Measurement, 9th International Conference, Proceedings. Passive and Active Network Measurement, 9th International Conference, Proceedings, PAM 2008, Cleveland, OH, USA, April 29-30, 2008, Lecture Notes in Computer Science, vol. 4979 (2008), Springer), 1-10 |
| [13] | Kozen, D., Kleene algebra with tests, ACM Trans. Program. Lang. Syst., 19, 3, 427-443 (1997) |
| [14] | Kozen, D., A completeness theorem for Kleene algebras and the algebra of regular events, Inf. Comput., 110, 2, 366-390 (1994) · Zbl 0806.68082 |
| [15] | Halpern, J. Y., Causality, responsibility, and blame: a structural-model approach, (Benferhat, S.; Grant, J., Scalable Uncertainty Management - 5th International Conference, Proceedings. Scalable Uncertainty Management - 5th International Conference, Proceedings, SUM 2011, Dayton, OH, USA, October 10-13, 2011. Scalable Uncertainty Management - 5th International Conference, Proceedings. Scalable Uncertainty Management - 5th International Conference, Proceedings, SUM 2011, Dayton, OH, USA, October 10-13, 2011, Lecture Notes in Computer Science, vol. 6929 (2011), Springer), 1 |
| [16] | Halpern, J. Y., A modification of the Halpern-Pearl definition of causality, (Yang, Q.; Wooldridge, M. J., Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015 (2015), AAAI Press), 3022-3033 |
| [17] | Durán, F.; Rocha, C.; Álvarez, J. M., Towards a Maude formal environment, (Agha, G.; Danvy, O.; Meseguer, J., Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday. Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday, Lecture Notes in Computer Science, vol. 7000 (2011), Springer), 329-351 · Zbl 1225.68006 |
| [18] | Giesl, J.; Aschermann, C.; Brockschmidt, M.; Emmes, F.; Frohn, F.; Fuhs, C.; Hensel, J.; Otto, C.; Plücker, M.; Schneider-Kamp, P.; Ströder, T.; Swiderski, S.; Thiemann, R., Analyzing program termination and complexity automatically with AProVE, J. Autom. Reason., 58, 1, 3-31 (2017) · Zbl 1409.68255 |
| [19] | Beckett, R.; Greenberg, M.; Walker, D., Temporal NetKAT, (Krintz, C.; Berger, E., Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016 (2016), ACM), 386-401 |
| [20] | Leitner-Fischer, F.; Leue, S., Causality checking for complex system models, (Giacobazzi, R.; Berdine, J.; Mastroeni, I., Verification, Model Checking, and Abstract Interpretation, 14th International Conference, Proceedings. Verification, Model Checking, and Abstract Interpretation, 14th International Conference, Proceedings, VMCAI 2013, Rome, Italy, January 20-22, 2013. Verification, Model Checking, and Abstract Interpretation, 14th International Conference, Proceedings. Verification, Model Checking, and Abstract Interpretation, 14th International Conference, Proceedings, VMCAI 2013, Rome, Italy, January 20-22, 2013, Lecture Notes in Computer Science, vol. 7737 (2013), Springer), 248-267 · Zbl 1426.68173 |
| [21] | Caltais, G.; Guetlein, S. L.; Leue, S., Causality for general LTL-definable properties, (Finkbeiner, B.; Kleinberg, S., Proceedings 3rd Workshop on Formal Reasoning About Causation, Responsibility, and Explanations in Science and Technology. Proceedings 3rd Workshop on Formal Reasoning About Causation, Responsibility, and Explanations in Science and Technology, CREST@ETAPS 2018, Thessaloniki, Greece, 21st April 2018. Proceedings 3rd Workshop on Formal Reasoning About Causation, Responsibility, and Explanations in Science and Technology. Proceedings 3rd Workshop on Formal Reasoning About Causation, Responsibility, and Explanations in Science and Technology, CREST@ETAPS 2018, Thessaloniki, Greece, 21st April 2018, EPTCS, vol. 286 (2018)), 1-15 |
| [22] | Lewis, D., Causation, J. Philos., 70, 556-567 (1973) |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
