Formal modeling and verification for SDN firewall application using pACSR

Miyoung Kang, Jin Young Choi, Hee Hwan Kwak, Inhye Kang, Myung Ki Shin, Jong Hwa Yi

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Scopus citations

Abstract

The main purpose of this paper is to describe the formal modeling using the process algebra language called pACSR and then suggest a method to verify the firewall application running on SDN using pACSR. In order to detect the violation of firewall rules in case of SDN network topology changes, we propose a verification framework that can check the deadlock through parallel composition of the specification (SPEC) and its implementation(IMPL). If any mismatches or inconsistencies between SPEC and IMPL occur, they could be detected within the formal framework. This framework provides in advance verification for consistency in SDN before critical error might occur by SDN controlling.

Original languageEnglish
Title of host publicationElectronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014
EditorsAmir Hussain, Mirjana Ivanovic
PublisherCRC Press/Balkema
Pages155-161
Number of pages7
ISBN (Print)9781138028302
DOIs
StatePublished - 2015
Event4th International Conference on Electronics, Communications and Networks, CECNet2014 - Beijing, China
Duration: 12 Dec 201415 Dec 2014

Publication series

NameElectronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014

Conference

Conference4th International Conference on Electronics, Communications and Networks, CECNet2014
Country/TerritoryChina
CityBeijing
Period12/12/1415/12/14

Fingerprint

Dive into the research topics of 'Formal modeling and verification for SDN firewall application using pACSR'. Together they form a unique fingerprint.

Cite this