SDN verification plane for consistency establishment

Software Defined Networking (SDN) is the new promise towards an easily configured and centrally controlled network. Based on this centralized control, SDN technology has proved its positive impact in the world of network communications from different aspects. Consistency in SDN, as in any rule-based network, is an essential feature that every communication system should possess. In this paper, we propose an SDN verification layer based on formal techniques to establish flow consistency between SDN switches before the flow insertion process takes place. We show how such an approach can be used to prevent loopbacks, deadlocks, security domain breaches, and to verify the time delay for a controller to update a switch versus the switch to forward a packet. This last point ensures that the update process is synchronized and no packet would be checked against old rules during this update process. The solution lies in introducing a verification plane enabling our verification module to interact with a third party verification tool (UPPAAL) translating the controller's view of the network to a state machine and verifying each flow before being installed. The verification tool checks each flow against a predefined set of rules by applying the new flow to the scheme and testing if a packet can pass from point A to B without violating these rules. Our evaluation shows the capability of the proposed system to enforce different levels of consistency verification in case of flow update and topology change in a SDN network.