ИСТИНА

We present a software toolset VERMONT (VERifying MONiTor) for runtime checking the consistency of Software Defined Network (SDN) configurations with formally specified invariants of Packet Forwarding Policies (PFPs). One of the main task of network engineering is to provide such a loading of SDN switches with forwarding rules as to guarantee its compliance with the PFP. VERMONT provides some automation to the solution of this task. Being installed in line with the control plane it 1) observes state changes of a network by intercepting the exchange of messages and commands between network switches and SDN controller, 2) builds an adequate formal model of a whole network, and 3) checks every event, 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 a switch VERMONT anticipates the result of its execution and checks the requirements of PFP. If a violation of some PFP invariant is detected then VERMONT blocks the change, alerts a network administrator, and gives some additional information to elucidate a possible source of an error. In this paper we discuss both mathematical and engineering issues of our toolset. We begin with defining a formal model of SDN and a formal language for PFP specification. After presenting the main algorithms used in VERMONT for SDN model building, model checking, and model modification, we 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.