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 contribution

1 Citation (Scopus)

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
PublisherCRC Press/Balkema
Pages155-161
Number of pages7
ISBN (Print)9781138028302
Publication statusPublished - 2015
Event4th International Conference on Electronics, Communications and Networks, CECNet2014 - Beijing, China
Duration: 2014 Dec 122014 Dec 15

Other

Other4th International Conference on Electronics, Communications and Networks, CECNet2014
CountryChina
CityBeijing
Period14/12/1214/12/15

ASJC Scopus subject areas

  • Hardware and Architecture
  • Electrical and Electronic Engineering

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