Vermont – a toolset for verification of software defined networks

In this paper we present the software toolset VERMONT (VERifying MONiTor) for runtime checkingthe consistency of Software Defined Network (SDN) configurations with formally specified invariants of Packet Forwarding Policies (PFPs). VERMONT can be installed in line with the control plane to observe state changes of a network by intercepting the exchange of messages and commands between network switches and SDN controller, to build an adequate formal model of the whole network, and to check everyevent, such as installation, deletion, or modification of rules, port and switch up and down events, against a set of PFP invariants. Before retransmitting a network updating command to the switch, VERMONT simulates the result of its execution and checks PFP requirements. If a violation of some PFP invariant is detected, VERMONT blocks the change, alerts a network administrator, and gives some additional information to elucidate a possible source of the error. We define a SDN mathematical model used in our toolset, discuss some algorithmic and engineering issues of our toolset. After introducing a formal model of SDN and a formal language for PFP specification, we outline the main algorithms used in VERMONT for SDN model building, model checking, and model modification, and describe the structure of VERMONT and the functionality of its components. Finally, we demonstrate the results of our experiments on the application of VERMONT to a real-life network.