Modeling and verifying SDN under Multi‐controller architectures using CSP. (21st May 2019)

• Record Type: Journal Article
• Authors: Xiao, Lili; Zhu, Huibiao; Xiang, Shuangqing; Cong Vinh, Phan
• Other Names: Ko Hoon guestEditor.; Marreiros Goreti guestEditor.; Cong Vinh Phan guestEditor.
• Is Part Of: Concurrency and computation. Volume 33:Number 2(2021)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2019-05-21
• Subjects: CSP -- modeling -- multiple controllers -- Software Defined Networking (SDN) -- verification; Parallel processing (Electronic computers) -- Periodicals; Parallel computers -- Periodicals; 004.35
• DOI: 10.1002/cpe.5334
• Languages: English
• ISSNs: 1532-0626

Abstract

Summary: Software Defined Networking (SDN) with multiple controllers draws more attention for the increasing scale of the network. Multi‐controller architectures can handle what SDN with single controller is not able to address. In order to understand what these architectures can accomplish and face precisely, we analyze them with formal methods. In this paper, we apply Communicating Sequential Processes (CSP) to model the routing service of SDN under multi‐controller architectures, in particular the HyperFlow architecture and the Kandoo architecture based on OpenFlow protocol. By using model checker Process Analysis Toolkit (PAT), we verify that the models satisfy three properties, namely deadlock freeness, consistency, and fault tolerance. In addition, for studying the security of those models, some extension is added. We find that the extended models are capable of coping with Denial of Service and may suffer from Information Disclosure. Moreover, a fake path and a tampered message could be present in SDN.