Formal Verification of SDN-Based Firewalls by Using TLA & x002B;
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Kim, Young-Mi | - |
dc.contributor.author | Kang, Miyoung | - |
dc.date.accessioned | 2021-08-31T16:01:33Z | - |
dc.date.available | 2021-08-31T16:01:33Z | - |
dc.date.created | 2021-06-19 | - |
dc.date.issued | 2020 | - |
dc.identifier.issn | 2169-3536 | - |
dc.identifier.uri | https://scholar.korea.ac.kr/handle/2021.sw.korea/58958 | - |
dc.description.abstract | Software-defined networking (SDN) has generated increased interest due to the rapid growth in the amount of data generated by the development of the Internet and communications, the commercialization of 5G, and increasingly complex networks. While SDN is more advantageous than traditional networks in terms of efficient network management, rapid deployment, and dynamic scalability, the correctness of a network configuration must be ensured in advance. In other words, SDN components such as network devices, SDN controllers, and applications need to be deployed correctly and must be free of rule conflicts, particularly between various application policies; otherwise, it may result in network paralysis in the worst case. This paper assumes that the SDN network is free of rule conflicts when the rules in the SDN switches correctly obey firewall application or policies. To solve this problem, this paper proposes a verification framework for SDN using TLA & x002B;. We show that the firewall rule behavior of switches can be formalized using TLA & x002B;, and this is verified with the TLC model checker that uses TLA & x002B; as the model description language. We check two different types of topology models through our verification framework to ensure that the same firewall rules are maintained even if the topology changes. The findings show that the firewall rules may be inconsistent as the topology changes. | - |
dc.language | English | - |
dc.language.iso | en | - |
dc.publisher | IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC | - |
dc.subject | PROCESS ALGEBRAIC APPROACH | - |
dc.subject | SPECIFICATION | - |
dc.title | Formal Verification of SDN-Based Firewalls by Using TLA & x002B; | - |
dc.type | Article | - |
dc.contributor.affiliatedAuthor | Kang, Miyoung | - |
dc.identifier.doi | 10.1109/ACCESS.2020.2979894 | - |
dc.identifier.scopusid | 2-s2.0-85082523911 | - |
dc.identifier.wosid | 000524748500080 | - |
dc.identifier.bibliographicCitation | IEEE ACCESS, v.8, pp.52100 - 52112 | - |
dc.relation.isPartOf | IEEE ACCESS | - |
dc.citation.title | IEEE ACCESS | - |
dc.citation.volume | 8 | - |
dc.citation.startPage | 52100 | - |
dc.citation.endPage | 52112 | - |
dc.type.rims | ART | - |
dc.type.docType | Article | - |
dc.description.journalClass | 1 | - |
dc.description.journalRegisteredClass | scie | - |
dc.description.journalRegisteredClass | scopus | - |
dc.relation.journalResearchArea | Computer Science | - |
dc.relation.journalResearchArea | Engineering | - |
dc.relation.journalResearchArea | Telecommunications | - |
dc.relation.journalWebOfScienceCategory | Computer Science, Information Systems | - |
dc.relation.journalWebOfScienceCategory | Engineering, Electrical & Electronic | - |
dc.relation.journalWebOfScienceCategory | Telecommunications | - |
dc.subject.keywordPlus | PROCESS ALGEBRAIC APPROACH | - |
dc.subject.keywordPlus | SPECIFICATION | - |
dc.subject.keywordAuthor | Tools | - |
dc.subject.keywordAuthor | Network topology | - |
dc.subject.keywordAuthor | Topology | - |
dc.subject.keywordAuthor | Model checking | - |
dc.subject.keywordAuthor | Firewalls (computing) | - |
dc.subject.keywordAuthor | Scalability | - |
dc.subject.keywordAuthor | Companies | - |
dc.subject.keywordAuthor | Firewall | - |
dc.subject.keywordAuthor | formal methods | - |
dc.subject.keywordAuthor | software-defined networking | - |
dc.subject.keywordAuthor | TLA plus | - |
Items in ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.
(02841) 서울특별시 성북구 안암로 14502-3290-1114
COPYRIGHT © 2021 Korea University. All Rights Reserved.
Certain data included herein are derived from the © Web of Science of Clarivate Analytics. All rights reserved.
You may not copy or re-distribute this material in whole or in part without the prior written consent of Clarivate Analytics.