상세정보
학술지
A Verification Method of SDN Firewall Applications
- 저자
- 강미영, 최진영, 강인혜, 곽희환, 안소진, 신명기
- 발행일
- 201607
- 출처
- IEICE Transactions on Communications, v.E99.B no.7, pp.1408-1415
- ISSN
- 0916-8516
- 출판사
- 일본, 전자정보통신학회 (IEICE)
- 협약과제
- 15MI2200, (통합)스마트 네트워킹 핵심 기술 개발, 양선희
- 초록
- SDN (Software-DefinedNetworking) 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.
- KSP 제안 키워드
- Firewall rules, Network devices, Network topology, Parallel composition, Software applications, Software-Defined Networking(SDN), Topology changes, deadlock-free, directly applied, formal modeling, process algebra