A verification method of SDN firewall applications

Miyoung Kang, Jin Young Choi, Inhye Kang, Hee Hwan Kwak, So Jin Ahn, Myung Ki Shin

Research output: Contribution to journalArticlepeer-review

8 Citations (Scopus)


SDN (Software-DefinedNetworking) 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.

Original languageEnglish
Pages (from-to)1408-1415
Number of pages8
JournalIEICE Transactions on Communications
Issue number7
Publication statusPublished - 2016 Jul

Bibliographical note

Publisher Copyright:
© Copyright 2016 The Institute of Electronics, Information and Communication Engineers.


  • Formal modeling
  • Formal verification
  • Software-defined networking

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications
  • Electrical and Electronic Engineering


Dive into the research topics of 'A verification method of SDN firewall applications'. Together they form a unique fingerprint.

Cite this