Explaining Safety Failures in NetKAT
Abstract
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.
Cite
@article{arxiv.2102.12448,
title = {Explaining Safety Failures in NetKAT},
author = {Georgiana Caltais and Hunkar Can Tunc},
journal= {arXiv preprint arXiv:2102.12448},
year = {2021}
}
Comments
arXiv admin note: substantial text overlap with arXiv:1909.01745