A Verification Method of SDN Firewall Applications
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Kang, Miyoung | - |
dc.contributor.author | Choi, Jin-Young | - |
dc.contributor.author | Kang, Inhye | - |
dc.contributor.author | Kwak, Hee Hwan | - |
dc.contributor.author | Ahn, So Jin | - |
dc.contributor.author | Shin, Myung-Ki | - |
dc.date.accessioned | 2021-09-03T22:12:26Z | - |
dc.date.available | 2021-09-03T22:12:26Z | - |
dc.date.created | 2021-06-18 | - |
dc.date.issued | 2016-07 | - |
dc.identifier.issn | 0916-8516 | - |
dc.identifier.uri | https://scholar.korea.ac.kr/handle/2021.sw.korea/88118 | - |
dc.description.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. | - |
dc.language | English | - |
dc.language.iso | en | - |
dc.publisher | IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG | - |
dc.subject | PROCESS ALGEBRAIC APPROACH | - |
dc.title | A Verification Method of SDN Firewall Applications | - |
dc.type | Article | - |
dc.contributor.affiliatedAuthor | Kang, Miyoung | - |
dc.contributor.affiliatedAuthor | Choi, Jin-Young | - |
dc.identifier.doi | 10.1587/transcom.2015EBP3329 | - |
dc.identifier.scopusid | 2-s2.0-84976618259 | - |
dc.identifier.wosid | 000381561500002 | - |
dc.identifier.bibliographicCitation | IEICE TRANSACTIONS ON COMMUNICATIONS, v.E99B, no.7, pp.1408 - 1415 | - |
dc.relation.isPartOf | IEICE TRANSACTIONS ON COMMUNICATIONS | - |
dc.citation.title | IEICE TRANSACTIONS ON COMMUNICATIONS | - |
dc.citation.volume | E99B | - |
dc.citation.number | 7 | - |
dc.citation.startPage | 1408 | - |
dc.citation.endPage | 1415 | - |
dc.type.rims | ART | - |
dc.type.docType | Article | - |
dc.description.journalClass | 1 | - |
dc.description.journalRegisteredClass | scie | - |
dc.description.journalRegisteredClass | scopus | - |
dc.relation.journalResearchArea | Engineering | - |
dc.relation.journalResearchArea | Telecommunications | - |
dc.relation.journalWebOfScienceCategory | Engineering, Electrical & Electronic | - |
dc.relation.journalWebOfScienceCategory | Telecommunications | - |
dc.subject.keywordPlus | PROCESS ALGEBRAIC APPROACH | - |
dc.subject.keywordAuthor | software-defined networking | - |
dc.subject.keywordAuthor | pACSR | - |
dc.subject.keywordAuthor | formal modeling | - |
dc.subject.keywordAuthor | formal verification | - |
Items in ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.
145 Anam-ro, Seongbuk-gu, Seoul, 02841, Korea+82-2-3290-2963
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.