利用邏輯程式設計來達到軟體定義網路之一致性

Abstract

軟體定義網路已廣泛地運用於雲端運算中心。在軟體定義網路的雲端運算中心環境中，租戶們可以為他們的虛擬機器指定網路需求，軟體定義網路的技術實現了相應的虛擬網路，滿足租戶們的網路需求。但是，當異常發生時，實際的網路配置設定可能會與使用者所期望的不一致。在這篇研究中我們展示了一套系統來驗證軟體定義的網路與其規範網路配置的一致性。為了實現這一目標，我們提出套基於圖型的網路模型來描述資料中心的實體網路拓撲和邏輯網路拓撲。此網路模型包括資料中心軟體定義網路的三個面向: 基礎設施的描述、虛擬網路規格需求、網路配置設定的描述。透過將模型轉換成邏輯條件式，並利用限制求解器進行求解，我們可偵測出不一致的網路配置情形。我們在一個使用GRE隧道網路服務的OpenStack環境底下建立雛形系統。透過實驗證明，該雛形系統提供VLAN異常檢測功能。

Software Defined Networking (SDN) has been widely used in today’s cloud datacenter environment. In a cloud datacenter environment, tenants can specify a virtual network for their virtual machines. SDN technologies are employed to realize the virtual network on top of the datacenter network infrastructure. Due to unavoidable component failures, software bugs, and human errors, inconsistencies in the software defined network configuration are anticipated. The inconsistencies could result in network outage or violation of network security policy. In this paper, we propose a system that verifies the consistency of the configurations of a software defined network. The system employs a graph-based network model to describe the physical network topology and the logical network topology of a datacenter. Specifically, the network model covers the infrastructure description, the virtual network specification description, and the configuration state description. Logic constraints are generated from the network model and then fed to a constraint solver to verify the satisfiability of the constraints. If the constraints can be satisfied, the network configuration is consistent. Otherwise, the network configuration is inconsistent. We built a prototype system based on OpenStack and OpenFlow. The experiment results confirmed the system is able to detect various inconsistent configurations of a software defined network. The experiment results also indicate the system is efficient. It takes about 1 second to verify the consistency of a network with 6 virtual machines.