Research Area:  Software Defined Networks
Software Defined Networking (SDN) is an emerging networking paradigm, which provides flexible network programmability and eases the complexity of network control and management. The OpenFlow protocol is the best-known southbound interface of SDN. As the core of a software-defined network, a controller collects topology information of the entire network in order to manage the network as well as provide services to topology-dependent applications. The accuracy of topology information gained by a controller is utmost important. However, most of the mainstream OpenFlow controllers suffer from two kinds of topology poisoning attacks: Link Fabrication Attack and Host Hijacking Attack. TopoGuard is the most famous security extension to traditional OpenFlow controllers, providing detection of the two attacks. In this paper, we model TopoGuard, OpenFlow switches, hosts and two kinds of attackers using Communication Sequential Processes (CSP). Moreover, we encode the proposed model into Process Analysis Toolkit (PAT), a model checker. Finally, we use PAT to verify whether TopoGuard is able to detect the two attacks in some specific scenarios.
Keywords:  
Modeling
Formal Verifying
SDN
TopoGuard
Author(s) Name:  Shuangqing Xiang; Huibiao Zhu; Lili Xiao; Wanling Xie
Journal name:  
Conferrence name:  2018 International Symposium on Theoretical Aspects of Software Engineering (TASE)
Publisher name:  IEEE
DOI:  10.1109/TASE.2018.00019
Volume Information:  
Paper Link:   https://ieeexplore.ieee.org/abstract/document/8560737