Paper Info
Title
A Verification Method Of Sdn Firewall Applications
Abstract
SDN (Software-Defined Networking) enables software applications to program individual network devices dynamically and therefore control the behavior of the network as a whole. Incomplete programming and/or inconsistency with the network policy of SDN software applications may lead to verification issues. The objective of this paper is to describe the formal modeling that uses the process algebra called pACSR and then suggest a method to verify the firewall application running on top of the SDN controller. The firewall rules are translated into a pACSR process which acts as the specification, and packet's behaviors in SDN are also translated to a pACSR process which is a role as the implementation. Then we prove the correctness by checking whether the parallel composition of two pACSR processes is deadlock-free. Moreover, in the case of network topology changes, our verification can be directly applied to check whether any mismatches or inconsistencies will occur.
Year
DOI
Venue
2016
10.1587/transcom.2015EBP3329
IEICE TRANSACTIONS ON COMMUNICATIONS
Keywords
Field
DocType
software-defined networking, pACSR, formal modeling, formal verification
Functional verification,Programming language,Firewall (construction),Computer science,Intelligent verification,Verification,Formal specification,Formal methods,Distributed computing,Software verification,Formal verification
Journal
Volume
Issue
ISSN
E99B
7
0916-8516
Citations 
PageRank 
References 
0
0.34
9
Authors
6
Name
Order
Citations
PageRank
Miyoung Kang100.34
Jin-young Choi260650.44
Inhye Kang316917.91
Hee-Hwan Kwak4354.75
So Jin Ahn510.70
Myung-ki Shin625621.82