A Verification Method of SDN Firewall Applications
Summary :
SDN (Software-Defined Networking) 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.
- Publication
- IEICE TRANSACTIONS on Communications Vol.E99-B No.7 pp.1408-1415
- Publication Date
- 2016/07/01
- Publicized
- Online ISSN
- 1745-1345
- DOI
- 10.1587/transcom.2015EBP3329
- Type of Manuscript
- PAPER
- Category
- Fundamental Theories for Communications
Authors
Miyoung KANG
Korea University
Jin-Young CHOI
Korea University
Inhye KANG
the University of Seoul
Hee Hwan KWAK
SOLiD
So Jin AHN
Korea University
Myung-Ki SHIN
ETRI
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Miyoung KANG, Jin-Young CHOI, Inhye KANG, Hee Hwan KWAK, So Jin AHN, Myung-Ki SHIN, "A Verification Method of SDN Firewall Applications" in IEICE TRANSACTIONS on Communications,
vol. E99-B, no. 7, pp. 1408-1415, July 2016, doi: 10.1587/transcom.2015EBP3329.
Abstract: SDN (Software-Defined Networking) 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.
URL: https://global.ieice.org/en_transactions/communications/10.1587/transcom.2015EBP3329/_p
Copy
@ARTICLE{e99-b_7_1408,
author={Miyoung KANG, Jin-Young CHOI, Inhye KANG, Hee Hwan KWAK, So Jin AHN, Myung-Ki SHIN, },
journal={IEICE TRANSACTIONS on Communications},
title={A Verification Method of SDN Firewall Applications},
year={2016},
volume={E99-B},
number={7},
pages={1408-1415},
abstract={SDN (Software-Defined Networking) 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.},
keywords={},
doi={10.1587/transcom.2015EBP3329},
ISSN={1745-1345},
month={July},}
Copy
TY - JOUR
TI - A Verification Method of SDN Firewall Applications
T2 - IEICE TRANSACTIONS on Communications
SP - 1408
EP - 1415
AU - Miyoung KANG
AU - Jin-Young CHOI
AU - Inhye KANG
AU - Hee Hwan KWAK
AU - So Jin AHN
AU - Myung-Ki SHIN
PY - 2016
DO - 10.1587/transcom.2015EBP3329
JO - IEICE TRANSACTIONS on Communications
SN - 1745-1345
VL - E99-B
IS - 7
JA - IEICE TRANSACTIONS on Communications
Y1 - July 2016
AB - SDN (Software-Defined Networking) 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.
ER -
English
