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

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

Fingerprint

Computer system firewalls
Specifications
Algebra
Topology
Software defined networking
Chemical analysis

ASJC Scopus subject areas

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Cite this

Kang, M., Choi, J. Y., Kwak, H. H., Kang, I., Shin, M. K., & Yi, J. H. (2015). Formal modeling and verification for SDN firewall application using pACSR. In Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014 (pp. 155-161). CRC Press/Balkema.

Formal modeling and verification for SDN firewall application using pACSR. / Kang, Miyoung; Choi, Jin Young; Kwak, Hee Hwan; Kang, Inhye; Shin, Myung Ki; Yi, Jong Hwa.

Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014. CRC Press/Balkema, 2015. p. 155-161.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kang, M, Choi, JY, Kwak, HH, Kang, I, Shin, MK & Yi, JH 2015, Formal modeling and verification for SDN firewall application using pACSR. in Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014. CRC Press/Balkema, pp. 155-161, 4th International Conference on Electronics, Communications and Networks, CECNet2014, Beijing, China, 14/12/12.
Kang M, Choi JY, Kwak HH, Kang I, Shin MK, Yi JH. Formal modeling and verification for SDN firewall application using pACSR. In Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014. CRC Press/Balkema. 2015. p. 155-161
Kang, Miyoung ; Choi, Jin Young ; Kwak, Hee Hwan ; Kang, Inhye ; Shin, Myung Ki ; Yi, Jong Hwa. / Formal modeling and verification for SDN firewall application using pACSR. Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014. CRC Press/Balkema, 2015. pp. 155-161
@inproceedings{0e29155ce01d406f97104ba98fb24ec7,
title = "Formal modeling and verification for SDN firewall application using pACSR",
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.",
author = "Miyoung Kang and Choi, {Jin Young} and Kwak, {Hee Hwan} and Inhye Kang and Shin, {Myung Ki} and Yi, {Jong Hwa}",
year = "2015",
language = "English",
isbn = "9781138028302",
pages = "155--161",
booktitle = "Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014",
publisher = "CRC Press/Balkema",

}

TY - GEN

T1 - Formal modeling and verification for SDN firewall application using pACSR

AU - Kang, Miyoung

AU - Choi, Jin Young

AU - Kwak, Hee Hwan

AU - Kang, Inhye

AU - Shin, Myung Ki

AU - Yi, Jong Hwa

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85019296967&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85019296967&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:85019296967

SN - 9781138028302

SP - 155

EP - 161

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

PB - CRC Press/Balkema

ER -