ИСТИНА

Software-defined networks (SDNs) is a new type computer networks where data planes and control planes are separated from each other and a centralized controller manages a distributed set of switches. A set of commands for packet forwarding and flow-table updating was defined in the form of a protocol known as OpenFlow. SDNs can both simplify existing network applications and serve as a platform for developing new ones. The main advantage of this network architecture is that programmers are able to control the behaviour of the whole network by configuring appropriately the packet forwarding rules installed on the switches. Nevertheless, correct and safe management of SDNs is not an easy task. Every time the current load of flow tables should satisfy certain requirements: some packets have to reach their destination, although some other packets have to be dropped, certain switches are forbidden for some packets, whereas some other switches have to be obligatorily traversed. These and some other requirements constitute a Packet Forwarding Policies (PFPs). One of the aims of network engineering is to provide such a loading of switches with forwarding rules as to guarantee compliance with the PFP. The solution is to develop a toolset which could be able 1) to check correctness of a separate application operating on the controller w.r.t. a specified forwarding policy, 2) to check consistency of forwarding policies implemented by various applications, and 3) to monitor and check correctness and safety of the entire SDN. In an attempt to produce such a toolset we developed 1) a combined (relational and automata based) formal model which captures the most essential features of SDN behavior, 2) a multi-level formal language for specification of SDN forwarding policies which uses transitive closure operator to specify reachability properties of packet forwarding relation and temporal operators to specify behaviour of SDN as a whole, and 3) a BDD-based model-checking techniques for verification of SDN models against PFP specifications.