상세정보
학술지
Process Algebra Based Symbolic Verification Framework for Software-Defined Networking
Cited - time in 
Download 1 time
Share 
Download 1 time
Share
- 저자
- 신명기, 곽희환, 최진영, 강미영
- 발행일
- 201310
- 출처
- Telecommunications Review, v.23 no.5, pp.583-593
- ISSN
- 1226-5586
- 출판사
- SK Telecom 중앙연구소
- 협약과제
- 13PI2500, 캐리어급 서비스 인프라를 위한 SDN 핵심 기술 개발, 양선희
- 초록
- There have been continuous efforts and progresses regarding the research on the verification for Software Defined Networks (SDN), since incomplete or malicious programmable SDN entities could cause break-down of underlying networks shared by heterogeneous devices and stake-holders. In SDN world, it becomes important to verify the safety properties of SDN using formal method before the deployment of SDN applications. In this paper, we propose VeriSDN, a novel framework for the symbolic verification of SDN based on the formal method, especially with process algebra called pACSR which is an extended version of packet based Algebra of Communicating Shared Resources (ACSR). In our framework, OpenFlow’s flow tables are translated into pACSR descriptions and analyzed by means of a symbolic algorithm. The result will be the Boolean expression that satisfies when the property holds. pACSR processes are well suited to expresses concurrently running communicating switches and a controller. Packets in SDN can be described in pACSR as parameters passed via channels and handled with predefined predicates (PP) and be modified with predefined functions (PF). Even though our method is developed mainly for verification of the off-line case where flow tables are dynamically modified, however, we believe that it can be applied to the running switches with reasonable numbers. Furthermore, our method is transparent to the operators so the underlying verification process is hidden to the operators and there is no burden to understand the details of formal verification method by the operators.
- KSP 제안 키워드
- Algebra of communicating shared resources, Break-down, Flow Table, Formal Verification, Off-line, Safety Properties, Software-Defined Networking(SDN), Symbolic verification, boolean expression, formal methods, heterogeneous devices