A Case for Systematic Detection and Rigorous Location of SDN Control Conflicts

摘要

We take the position that the interaction of multiple software-defined networking (SDN) apps running in parallel must be thoroughly understood, and the potential conflict arising from it must be carefully prevented. We first motivate the problem with a concrete case study that shows that two SDN apps can cause a network to enter a permanent oscillation state. We then sketch a rigorous approach for systematically reasoning about the joint effect of multiple SDN apps, including whether conflicts may occur. The proposed approach models individual SDN apps as automata, and then uses standard automaton operations to compute their interactions. We further propose to apply sequence-based specification, a well-established rigorous method for software specification, to derive the automata. The key novelty and strength of our approach is its ability to reason about the joint effect of multiple SDN apps precisely (with the capability of identifying when and how conflicts may occur), proactively (prior to running the apps), and without the knowledge of the apps' implementation details.