Due to the development of SDN and NFV, the network becomes more and more complex. It is more difficult to verify the network as the network becomes more complicated. There has been studies to verify the network. We follow the way of Header Space Analysis, which defines header as a space and middlebox as transfer functions. As the header space passes through the transfer function, the space transfers to the different state. With the concept of intersection and subtraction for the match and AND and OR operations for the target, we can express the routing, NAT and other 1-to-1 mapping functions. However our tool, Stack Aided Verification Tool (SAVT), can support to verify the tunnel functions such as VPN with the concept of PUSH and POP operations with piggy-back stack. New expression for rules are defined in the thesis, which is more familiar to both human and computer.
The object for the SAVT is to check the reachability of the header. With misconfigurations, the reachability is harmed so that it causes loop and other errors for network. SAVT reports each error or reachability information as a form of text, and the range of reachability test could be selected which means the source and the destination node to be verified.
SAVT could be applied with central and distributed method. In this thesis, we follows the central method which is more similar to SDN to verify the logic network. By applying SAVT on NSF topology with 14 nodes and 42 links and NTT topology with 55 nodes and 144 links, we could verify them within 1 seconds when started in one node. We can find out the normal cases and error cases of routing and VPN. Also we could express the NAT in the network. As an error case of routing, loop might occur and SAVT reports the existence of loop when the header space starts to traverse from one node. Also the error of VPN, tunnel ID mismatch and absence of encapsulation and decapsulation are able to be reported.
소프트웨어 정의 네트워킹(SDN)과 네트워크 기능 가상화(NFV)로 인해 인터넷은 점점 복잡해지고 있다. 이에 따라 문제가 발생 했을 때 그 효과는 네트워크에 더 크게 영향을 주게 되고, 이를 검출하는 방법에 대한 연구가 필요하다. 이에 따라 다양한 연구가 진행되어 왔는데 그 중 Header Space Analysis는 패킷 헤더를 수학적 공간으로 정의하고 각 네트워크 장비를 함수로 정의하여 네트워크 검증을 수행한다. 본 논문의 스택 기반 검증 방법(SAVT)에서는 기존 기능에 더 보강하여, 교집합, 차집합, AND 연산, OR 연산 외에, 스택을 기반으로 한 피기백, PUSH 연산, POP연산을 정의하여 라우팅, NAT 등의 일대일의 함수뿐만 아닌, VPN 등의 캡슐화도 지원하도록 한다. 이 연산들은 좀 더 사용자 편의성을 고려해 재설계되었다. 정의한 기능들을 바탕으로 헤더의 도달가능성을 체크하는데, 잘못 구성된 노드가 있을 경우 루프 혹은 VPN 에러를 사용자에게 알려주게 된다. 또한 노드간 접근 가능성을 확인하기 위해, 출발지와 목적지를 지정해 검증을 수행할 수 있다.
SAVT는 중앙 처리식 방법과 분산 처리식 방법 모두 가능한데, 본 논문에서는 SDN 개념에 더 가까운 중앙 처리식 방법을 이용하여 논리적으로 구성한 네트워크를 검증하였다. NSF 네트워크와 KOR 네트워크 그리고 NTT 네트워크에 대해 검증을 수행하였고, 한 노드를 출발지로 지정해서 검증했을 경우 1초 이내에 결과를 얻을 수 있었다. 이 때, 의도적으로 설정한 특징인 VPN의 도달가능성, 루프, VPN에서의 에러를 검출 했고, 이 외의 다른 에러도 검증할 수 있다.
