DyNetKAT: An Algebra of Dynamic Networks
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 to provide an efficient reasoning method about safety properties for dynamic networks. 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 initial tool prototype.
Keywords
Cite
@article{arxiv.2102.10035,
title = {DyNetKAT: An Algebra of Dynamic Networks},
author = {Georgiana Caltais and Hossein Hojjat and Mohammad Mousavi and Hunkar Can Tunc},
journal= {arXiv preprint arXiv:2102.10035},
year = {2021}
}