Process Algebra Based Formal Method for SDN Application Verification

최근 SDN (Software Defined Networking) 기반의 다양한 네트워크 제어 및 관리 플랫폼들이 서비스제공자 및 통신사업자들에 의해 연구되고 있다. SDN의 중요한 특징 중 하나는 소프트웨어 프로그램으로 작성된 간단한 응용에 의해 네트워크가 쉽게 제어되고 관리된다는 점에 있다. 이러한 관점에서 잘못 작성된 SDN 응용은 네트워크 전체에 오류를 발생시킬 수 있어, 해당 응용은 작성된 오픈플로우 포워딩 규칙(rule)을 SDN 컨트롤러(controller)를 통해 스위치에 반영하기 전에 토폴로지와 네트워크 환경의 안전성(safety)과 일관성(consistency)이 반드시 검증되어야 한다. 본 논문에서는 SDN 응용 검증을 위한 프로세스 알지브라 (process algebra) 기반의 언어인 pACSR (Packet based Algebra of Communicating Shared Resources)와 이를 기반으로 한 정형 검증 프레임워크를 제안하고, 이에 대한 SDN 정형검증 도구 연구시제품 구현 현황을 기술한다. Recently, there have been continuous efforts and progresses regarding the research on diverse network control and management platforms for SDN (Software Defined Networking). SDN is defined as a new technology to enable service providers/network operators easily to control and manage their networks by writing a simple application program. In SDN, incomplete or malicious programmable entities could cause break-down of underlying networks shared by heterogeneous devices and stake-holders. In this sense, any misunderstanding or diverse interpretations should be completely avoided. This paper proposes a new framework for SDN application verification and a prototype based on the formal method, especially with process algebra called pACSR which is an extended version of Algebra of Communicating Shared Resources (ACSR).