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

doi:10.1201/b18592-31

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

School of Cybersecurity

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Citations (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 language	English
Title of host publication	Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014
Editors	Amir Hussain, Mirjana Ivanovic
Publisher	CRC Press/Balkema
Pages	155-161
Number of pages	7
ISBN (Print)	9781138028302
DOIs	https://doi.org/10.1201/b18592-31
Publication status	Published - 2015
Event	4th International Conference on Electronics, Communications and Networks, CECNet2014 - Beijing, China Duration: 2014 Dec 12 → 2014 Dec 15

Publication series

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

Other

Other	4th International Conference on Electronics, Communications and Networks, CECNet2014
Country/Territory	China
City	Beijing
Period	14/12/12 → 14/12/15

Bibliographical note

Funding Information:
This research was funded by the MSIP(Ministry of Science, ICT & Future Planning), Korea in the ICT R&D Program 2014, supported by the MSIP(Ministry of Science, ICT and Future Planning), Korea, under the ITRC(Information Technology Research Center) support program (NIPA-2014-H0301-14-1023) supervised by the NIPA(National IT Industry Promotion Agency), and was supported by Basic Science Research Program through the National Research Foundation of Korea(NRF) funded by the Ministry of Education, Science and Technology(MEST)(2012R1A1A2009354).

Publisher Copyright:
© 2015 Taylor & Francis Group, London.

ASJC Scopus subject areas

Hardware and Architecture
Electrical and Electronic Engineering

Access to Document

10.1201/b18592-31

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 A. Hussain, & M. Ivanovic (Eds.), Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014 (pp. 155-161). (Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014). CRC Press/Balkema. https://doi.org/10.1201/b18592-31

Formal modeling and verification for SDN firewall application using pACSR. / Kang, Miyoung; Choi, Jin Young; Kwak, Hee Hwan et al.
Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014. ed. / Amir Hussain; Mirjana Ivanovic. CRC Press/Balkema, 2015. p. 155-161 (Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014).

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 A Hussain & M Ivanovic (eds), Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014. 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. https://doi.org/10.1201/b18592-31

Kang M, Choi JY, Kwak HH, Kang I, Shin MK, Yi JH. Formal modeling and verification for SDN firewall application using pACSR. In Hussain A, Ivanovic M, editors, Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014. CRC Press/Balkema. 2015. p. 155-161. (Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014). doi: 10.1201/b18592-31

Kang, Miyoung ; Choi, Jin Young ; Kwak, Hee Hwan et al. / 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. editor / Amir Hussain ; Mirjana Ivanovic. CRC Press/Balkema, 2015. pp. 155-161 (Electronics, Communications and Networks IV - Proceedings of the 4th International Conference on Electronics, Communications and Networks, CECNet2014).

@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}",

note = "Funding Information: This research was funded by the MSIP(Ministry of Science, ICT & Future Planning), Korea in the ICT R&D Program 2014, supported by the MSIP(Ministry of Science, ICT and Future Planning), Korea, under the ITRC(Information Technology Research Center) support program (NIPA-2014-H0301-14-1023) supervised by the NIPA(National IT Industry Promotion Agency), and was supported by Basic Science Research Program through the National Research Foundation of Korea(NRF) funded by the Ministry of Education, Science and Technology(MEST)(2012R1A1A2009354). Publisher Copyright: {\textcopyright} 2015 Taylor & Francis Group, London.; 4th International Conference on Electronics, Communications and Networks, CECNet2014 ; Conference date: 12-12-2014 Through 15-12-2014",

year = "2015",

doi = "10.1201/b18592-31",

language = "English",

isbn = "9781138028302",

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

publisher = "CRC Press/Balkema",

pages = "155--161",

editor = "Amir Hussain and Mirjana Ivanovic",

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

}

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

N1 - Funding Information: This research was funded by the MSIP(Ministry of Science, ICT & Future Planning), Korea in the ICT R&D Program 2014, supported by the MSIP(Ministry of Science, ICT and Future Planning), Korea, under the ITRC(Information Technology Research Center) support program (NIPA-2014-H0301-14-1023) supervised by the NIPA(National IT Industry Promotion Agency), and was supported by Basic Science Research Program through the National Research Foundation of Korea(NRF) funded by the Ministry of Education, Science and Technology(MEST)(2012R1A1A2009354). Publisher Copyright: © 2015 Taylor & Francis Group, London.

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

U2 - 10.1201/b18592-31

DO - 10.1201/b18592-31

M3 - Conference contribution

AN - SCOPUS:85019296967

SN - 9781138028302

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

SP - 155

EP - 161

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

A2 - Hussain, Amir

A2 - Ivanovic, Mirjana

PB - CRC Press/Balkema

T2 - 4th International Conference on Electronics, Communications and Networks, CECNet2014

Y2 - 12 December 2014 through 15 December 2014

ER -

Formal modeling and verification for SDN firewall application using pACSR

Abstract

Publication series

Other

Bibliographical note

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this