ICE-TCS seminar: Georgiana Caltais
Explaining SDN Failures via Axiomatisations
ICE-TCS seminar #341
Date and time: Wednesday, 2 October 2019, 15:00-15:45
Location: Room M1.23
Speaker: Georgiana Caltais (University of Konstanz)
Title: Explaining SDN Failures via Axiomatisations
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.
We also provide an equational framework that computes all relevant explanations witnessing a bad, or an unsafe behaviour, whenever the case. In our setting, safety is characterised by a NetKAT policy which does not enable forwarding packets from ingress to an undesirable egress. The proposed equational framework is a slight modification of the sound and complete axiomatisation of NetKAT, and is parametric on the size of the considered hop-by-hop switch policy. Our approach is orthogonal to related works which rely on model-checking algorithms for computing all counterexamples witnessing the violation of a certain property.
