Explaining SDN Failures via Axiomatisations

TL;DR

This paper develops a method to explain safety violations in SDNs by modifying the NetKAT axiomatisation, leveraging its mathematical foundation to derive equational explanations for failures.

Contribution

It introduces a novel approach to explain SDN failures using axiomatisations of NetKAT, enhancing understanding of safety violations in network policies.

Findings

Provides a formal method for explaining SDN failures

Uses modified NetKAT axioms for derivations

Enhances interpretability of network safety violations

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.