Abstract
We introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data-plane in dynamic updates. We provide a sound and ground-complete axiomatisation of our language. We exploit the equational theory and provide an efficient method for reasoning about safety properties. We implement our equational theory in DyNetiKAT – a tool prototype, based on the Maude Rewriting Logic and the NetKAT tool, and apply it to a case study. We show that we can analyse the case study for networks with hundreds of switches using our tool prototype.
The work of Georgiana Caltais and Hünkar Can Tunç was supported by the DFG project “CRENKAT”, proj. no. 398056821. The work of Mohammad Reza Mousavi was supported by the UKRI Trustworthy Autonomous Systems Node in Verifiability, Grant Award Reference EP/V026801/1. The authors would like to thank Alexandra Silva and Tobias Kappé for their useful insight into the NetKAT framework.
Chapter PDF
Similar content being viewed by others
Keywords
References
Luca Aceto, Bard Bloom, and Frits W. Vaandrager. Turning SOS rules into equations. Inf. Comput., 111(1):1–52, 1994. https://doi.org/10.1006/inco.1994.1040.
L. Aceto, W. J. Fokkink, and C. Verhoef. Conservative extension in structural operational semantics. Bull. EATCS, 69:110–132, 1999.
Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. NetKAT: semantic foundations for networks. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pages 113–126. ACM, 2014. https://doi.org/10.1145/2535838.2535862.
Jos C. M. Baeten and W. P. Weijland. Process algebra, volume 18 of Cambridge tracts in theoretical computer science. Cambridge University Press, 1990.
Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
Ryan Beckett, Michael Greenberg, and David Walker. Temporal netkat. In Chandra Krintz and Emery Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 386–401. ACM, 2016. https://doi.org/10.1145/2908080.2908108.
G. Caltais, H. Hojjat, M. R. Mousavi, and H. C. Tunc. DyNetKAT: An algebra of dynamic networks. CoRR, abs/2102.10035, 2021.
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Carolyn L. Talcott. Full Maude: Extending Core Maude. In Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and arolyn L. Talcott, editors, All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, volume 4350 of Lecture Notes in Computer Science, pages 559–597. Springer, 2007. https://doi.org/10.1007/978-3-540-71999-1_18.
Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic NetKAT. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 282–309. Springer, 2016. https://doi.org/10.1007/978-3-662-49498-1_12.
Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, and Laure Thompson. A Coalgebraic Decision Procedure for NetKAT. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 343–355. ACM, 2015. https://doi.org/10.1145/2676726.2677011.
Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness. CoRR, abs/2002.09682, 2020. URL: https://arxiv.org/abs/2002.09682, http://arxiv.org/abs/2002.09682.
Hyojoon Kim, Joshua Reich, Arpit Gupta, Muhammad Shahbaz, Nick Feamster, and Russell J. Clark. Kinetic: Verifiable dynamic network control. In 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4-6, 2015, pages 59–72. USENIX Association, 2015. URL: https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/kim.
Jedidiah McClurg, Hossein Hojjat, Nate Foster, and Pavol Cerný. Event-driven network programming. In Chandra Krintz and Emery Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 369–385. ACM, 2016. https://doi.org/10.1145/2908080.2908097.
Peter D. Mosses. Modular structural operational semantics. J. Log. Algebraic Methods Program. 60-61: 195-228, 2004. https://doi.org/10.1016/j.jlap.2004.03.008
Mohammad Reza Mousavi, Michel A. Reniers, and Jan Friso Groote. Notions of bisimulation and congruence formats for SOS with data. Information and Computation, 200(1):107 – 147, 2005. https://doi.org/10.1016/j.ic.2005.03.002.
Tim Nelson, Andrew D. Ferguson, Michael J. G. Scheer, and Shriram Krishnamurthi. Tierless programming and reasoning for software-defined networks. In Ratul Mahajan and Ion Stoica, editors, Proceedings of the 11th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2014, Seattle, WA, USA, April 2-4, 2014, pages 519–531. USENIX Association, 2014. URL: https://www.usenix.org/conference/nsdi14/technical-sessions/presentation/nelson.
Mark Reitblatt, Nate Foster, Jennifer Rexford, Cole Schlesinger, and David Walker. Abstractions for network update. In Lars Eggert, Jörg Ott, Venkata N. Padmanabhan, and George Varghese, editors, ACM SIGCOMM 2012 Conference, SIGCOMM ’12, Helsinki, Finland - August 13 - 17, 2012, pages 323–334. ACM, 2012. https://doi.org/10.1145/2342356.2342427.
Alexandra Silva. Models of Concurrent Kleene Algebra. In Elvira Albert and Laura Kovács, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, page 516. EasyChair, 2020. URL: https://easychair.org/publications/paper/6C8R.
Guido van Rossum. Python programming language. In Jeff Chase and Srinivasan Seshan, editors, Proceedings of the 2007 USENIX Annual Technical Conference, Santa Clara, CA, USA, June 17-22, 2007. USENIX, 2007.
Alexander Vandenbroucke and Tom Schrijvers. P\(\lambda \)\(\omega \)nk: functional probabilistic netkat. Proc. ACM Program. Lang., 4(POPL):39:1–39:27, 2020. https://doi.org/10.1145/3371107.
Jana Wagemaker, Paul Brunet, Simon Docherty, Tobias Kappé, Jurriaan Rot, and Alexandra Silva. Partially Observable Concurrent Kleene Algebra. In Igor Konnov and Laura Kovács, editors, 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), volume 171 of LIPIcs, pages 20:1–20:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. https://doi.org/10.4230/LIPIcs.CONCUR.2020.20.
Al-Fares, Mohammad and Loukissas, Alexander and Vahdat, Amin. A Scalable, Commodity Data Center Network Architecture. ACM SIGCOMM Comput. Commun. Rev. 38, 4, 63-74, 2008. https://doi.org/10.1145/1402946.1402967.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Caltais, G., Hojjat, H., Mousavi, M.R., Tunç, H.C. (2022). DyNetKAT: An Algebra of Dynamic Networks. In: Bouyer, P., Schröder, L. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2022. Lecture Notes in Computer Science, vol 13242. Springer, Cham. https://doi.org/10.1007/978-3-030-99253-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-030-99253-8_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99252-1
Online ISBN: 978-3-030-99253-8
eBook Packages: Computer ScienceComputer Science (R0)