Explaining SDN Failures via Axiomatisations
Formal Languages and Automata Theory
2019-09-05 v1 Programming Languages
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 that is 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 which does not enable forwarding packets from ingress to an undesirable egress. Explanations for safety violations are derived in an equational fashion, based on a modification of the existing NetKAT axiomatisation.
Cite
@article{arxiv.1909.01745,
title = {Explaining SDN Failures via Axiomatisations},
author = {Georgiana Caltais},
journal= {arXiv preprint arXiv:1909.01745},
year = {2019}
}
Comments
In Proceedings FROM 2019, arXiv:1909.00584