Atomic Predicates-Based Data Plane Properties Verification in Software Defined Networking using Spark


Software-Defined Networking (SDN) is an innovational network architecture which gives network administrators the ability to directly control the whole network by programming on a centralized controller. Due to network complexity, networks are unlikely to be bug-free. The ability to verify data plane properties will make network management easier for network administrators in SDN. In this paper, we present a novel atomic predicates based data plane properties verification method for SDN using Spark which is a big data processing framework. First, we verify packet reachability which is a fundamental data plane property. Then, we verify other data plane properties such as loop-freedom and nonexistence of black holes. In addition, the proposed method can detect a security threat existing in SDN called firewall bypass threat with packet reachability verification. By adopting atomic predicates, we achieve less computational and storage overhead. We implement the methods and study the performance. The results of experiments show that we can efficiently and accurately detect loops, black holes and firewall bypass threats.


Computer Science

Research Center/Lab(s)

Center for High Performance Computing Research

Second Research Center/Lab

Intelligent Systems Center


This work was supported in part by the NSFC under Grant 61572323 and Grant 61932014, in part by Grant-in-Aid for Scientific Research from the Japan Society for Promotion of Science (JSPS) under Grant 26280027, and in part by the NSF under Grant CCF-1725755

Keywords and Phrases

data plane properties verification; network management; packet reachability verification; SDN; Spark

International Standard Serial Number (ISSN)

0733-8716; 1558-0008

Document Type

Article - Journal

Document Version


File Type





© 2020 Institute of Electrical and Electronics Engineers (IEEE), All rights reserved.

Publication Date

01 Jul 2020