Modeling and verifying the topology discovery mechanism of OpenFlow controllers in software-defined networks using process algebra

Software-Defined Networking (SDN) is an emerging paradigm, providing separation of concerns between controllers that manage the network and switches that forward data flow. SDN enables network programmability and reduces the complexity of network control and management. The OpenFlow protocol is a widely accepted interface between SDN controllers and switches. OpenFlow controllers are the core of Software-Defined Networks (SDNs). They collect topology information to build a global and shared view of the network, which is used to provide services for topology-dependent core modules and applications. Therefore, the accuracy of the centralized abstract view of the network is of outermost importance for many essential SDN operations. However, the topology discovery mechanism used in almost all the mainstream OpenFlow controllers suffers from two kinds of topology poisoning attacks: Link Fabrication Attack and Host Hijacking Attack. TopoGuard is a wide-spread secure OpenFlow controller, which improves the standard topology discovery mechanism, providing automatic and real-time detection of these two attacks. However, the mechanism of TopoGuard lacks formal verification, especially in the situation where some hosts are migrating to their new locations. In this paper, we propose a general parameterized framework, including the Communicating Sequential Processes (CSP) models of the network components and the interfaces among them. Two loopholes of TopoGuard are found by implementing and verifying the proposed system model, which is an instance of the framework, in the model checker Process Analysis Toolkit (PAT). Moreover, we propose a new topology discovery mechanism based on TopoGuard, which solves the two loopholes.