Explaining Safety Failures in NetKAT

TL;DR

This paper presents a method for explaining safety violations in SDN policies written in NetKAT by deriving equational explanations and implementing a tool for automatic detection of unsafe forwarding behaviors.

Contribution

It introduces an equational approach to explain safety violations in NetKAT and develops SDN-SafeCheck, a tool for automatic detection of unsafe forwarding paths in SDNs.

Findings

SDN-SafeCheck effectively identifies all undesired forwarding behaviors.

The approach is based on a modified NetKAT axiomatisation.

The tool handles forwarding paths up to a user-defined size.

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.