DyNetKAT: An Algebra of Dynamic Networks

TL;DR

DyNetKAT introduces a formal language and reasoning tools for modeling and verifying dynamic updates in Software Defined Networks, enhancing safety analysis capabilities for complex network behaviors.

Contribution

It extends NetKAT with constructs for dynamic updates, providing a complete axiomatisation and an efficient reasoning method implemented in a new tool.

Findings

Able to analyze networks with hundreds of switches

Provides a sound and complete axiomatisation

Demonstrates practical applicability through a case study

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.