TS檢查器：SDN中的兩步沖突檢測整合機制

王 晗 葉家煒 嚴 明(復旦大學計算機科學技術學院 上海 200433)

0 引 言

軟件定義網絡(SDN)與OpenFlow[1]的出現和興起為網絡管理提供了便捷支持。在SDN架構中，數據平面和控制平面的解耦可以讓網絡開發者通過在Docker[2]容器或虛擬機中開發北向應用程序和調用SDN控制器提供的北向接口來操縱網絡設備[3]。然而，這種高度可編程的架構也面臨著一些問題，這些北向應用程序因為在開發中相互獨立，故可能因為發出匹配域中有重疊的請求而動作域不一致從而造成網絡狀態的不一致，我們稱這些匹配域中有重疊的請求為帶有重疊域的請求。根據OpenFlow規范，當數據包到達某個交換機時，會在其流表中查找第一條匹配的流表項，所以如果這些帶重疊域的請求直接發給SDN控制器時，會通過SDN控制器在交換機中生成相應流表項，當一個匹配重疊域的數據包到達交換機時它只會匹配到其中一條流表項并執行其動作指令，其他流表項的動作永遠不會被執行[4]。

因此，北向應用程序發出的請求在被發送到SDN控制器之前需要經過檢查和處理，以消除沖突并保證動作域的一致性。目前針對這種沖突檢測的方案有基于資源粒度和基于流表項粒度兩種方式。考慮到基于資源粒度的檢測方法無法滿足細粒度的需求，在本文中，我們提出了基于流表項粒度的TS(Two-Stage)檢查器。TS檢查器是位于應用層和控制層之間的檢查層，負責過濾、處理北向應用程序發往控制器的所有請求。對于北向應用程序發出的請求，要經過TS檢查器的兩次檢查，其中包括四個模塊，經過這些模塊處理，帶有重疊域且動作行為沖突的請求會被檢測并截斷，動作行為一致的請求會被整合，之后發給SDN控制器。

本文提出的TS檢查器支持基于最近最多匹配的部分檢查算法完成沖突檢測，使用基于RingBuffer實現的線程安全的請求隊列來緩沖存儲北向請求，在檢查、合并帶重疊域的請求時，使用字典樹數據結構從而保證處理的高效性。我們在Mininet[5]環境下驗證了TS檢查器的部分檢查算法的正確性和檢查器各模塊的性能。

1 相關研究

關于檢測SDN環境下流沖突的方案大體可以分為基于資源粒度和基于流表項粒度兩種。基于資源粒度的方案通過把來自北向應用程序的請求抽象成策略或意圖從而在資源層次進行意圖間的沖突檢測，而基于流表項粒度的方案的思想則是檢測每條流表項，通過和交換機中現有流表項逐一進行對比。

在基于資源粒度的方案中，AuYoung等[8-9]提出的Corybantic及其后續Athens，將Athens作為北向模塊和控制器之間的攔截者和代理者，接收并處理應用程序模塊發來的操作網絡資源的抽象意圖，例如虛擬機的放置等。這需要在對應用意圖進行抽象且在Athens和應用之間建立新的通信接口，而且不能解決細粒度的資源分配問題。PGA團隊[14]針對網絡提出了新的抽象模型——圖，但是這種抽象模型不支持set動作。Pyretic[7]在SDN環境下提出的新的開發語言和網絡架構，通過引入順序操作符和并行操作符解決沖突問題。但是Pyretic對網絡開發人員帶來的新技術的挑戰，并且這種新型架構對于現存的網絡應用而言難以遷移和擴展。

在基于流表項粒度的方案中，FortNOX[11]是針對NOX控制器的擴展，它通過基于角色的源認證和別名設置規則減少來實時檢測流表項之間的沖突。VeriFlow[12]是位于SDN控制器和網絡設備之間的一層，通過生成等價集和轉發圖來檢測變量之間的沖突。FlowChecker[10]把流表編碼成二分決策圖并且使用模型檢查器來檢測單個交換機內的錯誤配置，但它也不支持set動作。Flover[13]使用Yices SMT解決器檢查策略間的不一致，但僅限于網絡安全，對功能一致性沒有提及。

綜上，相比于基于資源粒度的解決方案，基于流表項粒度的解決方案對北向應用的一致性可以進行更細粒度的控制和檢測，而當前基于流表項粒度的解決方案中，盡管用到多種數學方法，但對于帶有重疊域的請求大多按照先到先處理的方式，并且對動作域不同的請求進行丟棄。然而動作域不同不代表動作域的沖突，對某些帶有重疊域的請求而言，其動作行為是可以無沖突共存的。上述基于流表項粒度的文章中沒有明確給出對重疊域請求進行整合的方案，因此我們提出了TS檢查器解決方案，對來自北向應用的請求進行沖突檢測和整合。

2 問題描述

考慮如下場景，應用層的路由應用程序負責計算生成轉發路徑，監控應用程序負責統計數據包流通情況。它們在相同時刻都發起了向同一交換機S中插入流表項的請求。請求A和C由路由應用程序發出，請求B由監控應用程序發出，為了簡化說明，我們把請求A、B、C抽象成表1所示的流表項，實際上應用請求一般是帶有JSON或XML格式數據的POST請求，需要經過簡單的解析處理才能轉化成一條或多條對應的流表項。

表1 來自兩個應用的三條請求

根據OpenFlow規范，每條流表項都隱式地包含一個計數器[4]，在本文中為了便于闡述問題，我們將計數器行為視為一個顯式的count動作，實際上當動作域沒有任何設定時就會執行count動作。

如果此時，交換機S中存在如表2所示的一條流表項。

表2 交換機S中的一條流表項

在這個場景下，如果對應用程序請求不作檢測處理而直接交給控制器，那么會有兩個問題：1)請求C和id=5的流表項存在沖突，對滿足src_ip=192.0.0.1/32條件的數據流其動作行為不一致，現存流表項的動作是丟棄，而請求C的動作是轉發到3號端口；2)請求A和請求B存在重疊域，即src_ip=20.0.0.1/32且dst_ip=20.0.0.2/32，對于滿足重疊域條件的數據包，只能執行轉發或計數其中一個動作，并且執行的具體動作也因請求A、B到達的先后順序而未知，而實際上轉發和計數分別是由路由應用和監控應用負責的，并且是兩個互不沖突的動作，所以可以被整合，請求B和C同理。

因此，在上述場景下，對于這些帶有重疊域并可能和現存流表項沖突的請求，我們可以歸納出在原有架構中存在如下所述的三個問題。

2.1 沖突問題

如果一個來自北向應用的請求交換機中某條現有流表項存在匹配域的交集并且因動作域不一致而產生沖突，我們稱之為沖突問題。在上述場景中，請求C與id=5的流表項間存在沖突問題。沖突問題在文獻[10-12]中得到了足夠的重視。它們使用了不同的數學公式或方法以消除和當前網絡狀態有沖突的請求從而保證網絡安全。在本文中，我們受到啟發并提出更高效地解決沖突問題的方案。

2.2 不公平競爭

在請求A和B是幾乎同時發出的前提下，受實際網絡因素控制，最終到達控制器的順序總有先后之分，按照先到先處理的原則，對于滿足其重疊匹配域的數據包X而言，其最終動作取決于優先到達控制器并生成的相應流表項的請求。在這種情況下，對于后到達控制器的請求是不公平的，并且請求到達的先后順序是受實際網絡情況影響而不可預測的。我們稱這種幾乎同時發出卻因到達時間的微小差別造成的現象為不公平競爭。在本文中，我們使用請求隊列來存儲短時間內到達的多個請求，通過批處理來解決部分不公平競爭的問題。

2.3 重疊問題

對于請求A和B而言，如果不進行處理而直接發往控制器，那么無論其到達順序如何，對于數據包X而言，其最終只能執行一條流表項的動作。如果請求A優先到達，那么計數動作會被忽略；如果請求B優先到達，那么轉發動作會被忽略。由此可見，數據包X的行為不能同時滿足路由應用和監控應用的意圖，并且可以看到只要請求中包含重疊域，則最終行為必不能滿足原始意圖。我們稱這個由重疊域帶來的問題為重疊問題，這也是被大多數基于流表項粒度的沖突解決方案所忽略的問題。

為了解決上述三個問題，我們提出了TS檢查器。

3 架構設計

在本節中，我們將詳細介紹TS檢查器。SDN架構把網絡抽象成三層，從北到南依次為：應用層、控制層、基礎設備層。和位于控制層與基礎設備層之間進行攔截的VeriFlow不同[12]，我們把TS檢查器定位于應用層與控制層之間。如圖1所示，在應用層有多個部署于Docker的獨立應用向控制器發出請求，這些應用包括負載均衡應用、監控應用、路由應用等。在這些請求發往控制器之前，需要經過包括四個模塊的檢查層的處理，在檢查層處理時，會根據策略判斷當前請求被接受或被拒絕。被接受的請求將進一步發往控制器進行后續操作，而對于被拒絕的請求，會發送反饋給相應的應用。

圖1 總體架構

與Athens和Pyretic方案不同，我們的檢查層方案僅需對現有應用進行微小改動——添加反饋處理模塊，而這可以通過補丁或擴展的方式實現。

整個檢查層包括四個模塊，其中進行了兩次檢查，由沖突檢查模塊和重疊檢查模塊分別負責不同的檢查任務。為了便于闡述，我們把北向應用發起的請求抽象成帶有負載的POST請求，并用如下所示的JSON對象進行描述。

“requests”: [{

“id”: “00070”,

“idle_time”: “3600”,

“hard_time”: “3600”,

“priority”: “20”,

“match”: {

“src_ip”: “192.168.1.1/32”

“eth_type”: “0x800”

},

“actions”: “drop”

},]

下面將分別描述四個模塊的主要功能。

3.1 沖突檢查模塊

這是第一個檢查步驟，負責檢查到來的請求是否與交換機中現有流表項(表示了當前網絡狀態)之間是否存在沖突。和當前網絡狀態一致的請求將被轉發到下一步驟(請求隊列)進行后續處理，而與當前網絡狀態沖突的請求則會被丟棄并發送相應反饋。

3.2 請求隊列

請求隊列是一個基于環形隊列實現的先進先出的隊列，用于存放被沖突檢查模塊過濾后的請求。

3.3 重疊檢查模塊

在此模塊中執行第二次檢查，負責檢查隊列中的請求之間是否存在重疊域，若有重疊域存在，則請求被發往下一個模塊，否則會被標志為有效請求并跳過整合模塊被直接發往SDN控制器。上述三個模塊共同構成了消費者- 生產者模式，沖突檢查模塊負責向請求隊列中輸入數據，而重疊檢查模塊負責批量消費請求隊列中的數據。

3.4 整合模塊

嘗試整合帶有重疊域的請求。如果這些帶重疊域請求的動作域指令是相互沖突的，則被丟棄并發送相應反饋，否則就通過策略去整合請求，將整合之后的請求發給SDN控制器。

四個步驟的處理流程可以用圖2概括。

圖2 TS檢查器處理流程

4 系統實現

4.1 沖突檢測算法

在檢查層對請求進行的第一步處理是進行沖突檢測。沖突檢測用于檢測一個新到來的請求是否與交換機中現有流表項規則有沖突。因為交換機中現有流表項規則表示了當前網絡狀態，這個步驟對于消除與網絡狀態沖突的請求從而維護網絡狀態一致性必不可少。

文獻[10-13]各自使用了不同的方法去完成沖突檢測的任務，它們全部基于檢查新插入請求或流表項與交換機中所有流表項之間的沖突。這些方法很完善但在某些場景下并非必要且是低效的。根據網絡局部性理論[15]可知，近期內被命中的流表項短時間內很可能被再次命中。所以對于某些對時延性要求較高而對網絡狀態一致性并不具有嚴格要求的場景而言，我們提出了用戶可配置的基于最近最多匹配的部分檢查這一折衷算法，使用者可以根據場景需求選擇部分檢查的覆蓋率，當覆蓋率為100%時退化為全部檢查。

部分檢查算法基于網絡局部性，如果交換機中的某條流表項被一個數據包命中過，那么短期內它有很大的概率會被再次匹配。基于此，我們在沖突檢查器中設計了最近最多匹配的緩存數據結構(LRM)，它用于保存每個交換機最近最頻繁被匹配到的流表項。為找到最近最多匹配的流表項，可使用流表項中的idle字段。根據OpenFlow規范，idle字段表示距離上一次被匹配的時間間隔，這反映了此條流表項的活躍度。

在沖突檢測算法中，我們使用Trie字典樹數據結構存儲匹配域中的IP地址，以保證在O(n)時間內完成檢測。具體的沖突檢測算法如算法1所示。沖突檢測器的輸出結果為接受或拒絕某個請求，對于被接受的請求將會發往請求隊列模塊。

算法1 沖突檢測算法input：acomingrequest，flowentries’idstoredinLRMforfidinLRM： flow=get＿flow(fid) trie=build＿trie(flow->match)ifrequest．matchisintrie： request＿queue．push(request)else： reject(request)

4.2 使用請求隊列解決不公平競爭問題

經過沖突檢測器過濾的請求被發往請求隊列。請求隊列在檢查層的作用是存儲請求便于后續的重疊檢查器進行處理。請求隊列的上游是沖突檢測器，下游是重疊檢測器，上游的處理時間是O(n)，并且在實際實現中可以將沖突檢測器實現為多線程并行處理，而下游處理時間是O(n2)。一方面請求隊列可以作為緩沖隊列去緩解消費速度落后于生產速度的情況，另一方面，正如在第3節中提到的，請求隊列可以通過緩存極短時間內到達的多個請求，在滿足實時性要求的同時便于下游進行批處理從而消除部分不公平競爭的問題。即對于被處理的同一批請求，在其優先級相同的情況下，不會因為其到達時間先后的微小差距而被區別對待。當請求隊列中有數據時，便會通過信號量方式通知下游重疊檢查器，重疊檢查器會取出當前請求隊列中所有請求，進行后續處理。

Corybantic和Athens解決方案對于何時進行一次策略整合沒有給出明確的說明[8-9]，它們的重點在于整合的決策算法。而請求隊列可以解決這個問題。

為實現請求隊列，我們底層使用了RingBuffer環形隊列結構，配合鎖和信號量以保證線程安全和對下游線程的喚醒。

4.3 重疊檢測算法

在沖突檢查步驟中，僅僅篩選出了與當前網絡狀態不沖突的應用請求，而面對在短時間內收到的一批應用請求時，其匹配域中很可能存在重疊從而導致需要進行進一步整合。重疊檢測器就是為了解決這個問題。

在實現算法上，重疊檢測算法與沖突檢測算法相似，不同的是，沖突檢測算法是比較單個輸入請求與交換機流表項，而重疊檢測算法的輸入是一批請求，重疊檢測器需要從這些請求中過濾掉其動作指令相互矛盾的請求，將可整合的請求發往之后的整合步驟進行進一步處理。

因為大多數重疊域是由于IP地址的交集造成的，我們這里以源IP地址為例進行說明。IPv4地址為32位，而在OpenFlow協議中可以使用通配符匹配，故在字典樹中我們使用高度最多為32位的字典樹即可存儲IP地址。

起初，字典樹數據結構為空，當收到請求隊列的喚醒信號時，它去獲取請求隊列中的全部請求，假設此時共有k個請求，重疊檢查器會去遍歷這k個請求，嘗試向字典樹中插入每個請求的源IP地址，并用tag位記錄其優先級。在插入前，檢查器會檢測當前字典樹中是否有其前綴IP地址。若沒有，則直接插入；若已有前綴IP地址發現，當前請求則會被記錄到由其前綴IP地址的請求構成的集合中。即當k個請求遍歷結束之后，會有多個集合生成，每個集合中至少有一條或多條應用請求，同一集合中的應用請求之間具有重疊域關系，稱之為重疊集。若重疊集中只有一條請求，說明不存在與之重疊的請求。

經過重疊檢測器之后，內部數量大于1的重疊集會被送到整合器進行整合，內部數量等于1的重疊集即只有一條請求的集合將被直接發到SDN控制器，提前結束了整個檢查流程。重疊檢測算法見算法2。

算法2 重疊檢測算法input：queuedrequestsfromRequestQueuetrie=Noneoverlap＿sets=Noneforrequestinqueued＿requests： node=in＿trie(trie，request) ifnode： overlap＿sets．set＿of＿(node)．append(request) else： overlap＿sets．add({request}) trie=insert＿trie(trie，request)forr＿setinoverlap＿sets： iflen(r＿set)is1： transfer＿to＿controller(r＿set) else： transfer＿to＿next＿stage(r＿set)

4.4 整合算法

重疊檢查器挑選出了需要被整合的重疊集，其中的應用請求需要接受整合器的進一步處理。整合器會嘗試去整合每個重疊集中的應用請求，它與重疊檢查器一起可以解決第2節提到的重疊問題。

在整合含有重疊域的請求時，需要分析每個請求的action字段以判斷請求之間是否存在相互矛盾的動作。根據OpenFlow規范，有drop、forward、set等顯式的動作，如表3所示[4]。如果我們把count動作也視為顯式動作，那么這四種動作之間的動作域關系表可以用表4展示。

表3 OpenFlow協議動作域

續表3

表4 動作域關系表

正如表4所示，對任意兩個請求的動作關系存在三種可能情況。No表示不存在矛盾，所以請求可以被整合。Yes表示存在矛盾，所以相關請求要么被丟棄要么按照預先約定的策略進行處理。Maybe表示需要根據具體的動作目標來進一步判斷是否存在矛盾沖突。例如forward動作，它可能有多個目標端口，當其目標端口不同時，則相互沖突，否則就視為一致。

實際環境中在一個重疊集中可能會存在超過兩條的應用請求，但在本文中，我們的目標是先解決兩個含重疊域的請求的整合，后續的工作將會將重點放在對三條及以上的請求的整合處理。因此在整合器這一步中我們暫時只處理包含兩條請求的重疊集。

假設重疊集中含有A、B兩個請求，直接將A和B請求發往SDN控制器會引起問題，正如第2節所描述的。整合器會按照策略生成一條新的請求C，請求C通過計算A和B的匹配域交集作為C的匹配域，A和B的動作域并集作為C的動作域，A和B中較高的優先級作為C的優先級。然后將請求三元組發給SDN控制器。至此，TS檢查器結束。

為了更清楚地解釋整合算法，我們以表5中的請求A和B為例，首先forward動作和set動作可以共存，所以兩個請求可以被整合。根據整合算法，請求A和請求B的匹配域交集為{src_ip=192.0.0.1/32, dst_ip=192.0.0.0/16}，其動作域的并集為{set_field:401->vlan_id, forward:1}。于是新生成的請求C和原請求A和B如表6所示。整合算法見算法3。

表5 原始請求

表6 整合后的請求

算法3 整合算法input：overlappingsetswhichhavetworequestsaccepted＿requests={}forrequestsinoverlappingsets： a，b=request ifcontradict(a．actions，b．actions)： reject(a，b) sendfeedbacktoapplicationsofa，b else： c=newrequest common＿match=intersection(a．match，b．match) c．match=common＿match c．actions=Union(a．actions，b．actions) c．priority=max(a．priority，b．priority) accepted＿requests．append([c，a，b])transfer＿to＿controller(accepted＿requests)

到目前為止，TS檢查器結束所有檢查步驟。新到來的請求必須經過沖突檢查器以保證其行為和當前流表項一致，然后經過重疊檢查器進行請求間的重疊檢測。經過這兩個步驟的檢查，被接受的請求會被發往SDN控制器，而帶有重疊域的請求被送往整合器，其會選擇具有可合并動作域的請求進行整合，隨即將整合結果發往SDN控制器，對于不可進行整合的請求將會被拒絕并且發送反饋給相應應用。

5 實驗驗證

在本節中，我們使用Ryu控制器[3]和Mininet評估TS檢查器的性能。Ryu控制器是提供RESTFul接口的輕量級控制器。Mininet提供了生成OpenFlow虛擬交換機、虛擬主機和網絡拓撲的環境。在實驗環境中，為了模擬北向應用發出的請求，我們構建了軟件請求生成器去模擬應用發出的POST請求，這些請求先經過解析器解析后可以映射成多條即將插入到交換機中的流表項，之后經過TS檢查器層過濾，將過濾結果發給SDN控制器。在實驗環境中，我們使用的服務器為Dell R730，搭配了2個主頻為2.4 GHz的Intel Xeon CPU，并劃分成24個邏輯CPU。

5.1 正確性驗證

在正確性驗證中，我們主要驗證了基于最近最多匹配的部分檢查算法。因為對匹配百分比的設定取決于實際場景，在實驗中，用圖3所示的拓撲環境，分別模擬了以下場景。

圖3 拓撲結構

場景1：數據包流量平均分布于6臺主機之間。

場景2：50%的流量集中于主機A與主機D之間，50%的數據包流量平均分布于其他主機通信。

場景3：90%的流量集中于主機A與D之間，10%的流量平均分布于其他主機間。

在三種場景中，我們先后設置沖突檢測器的匹配百分比為60%和100%，并對比了三種場景下沖突檢測器的過濾結果，如圖4所示，縱坐標為檢測出有沖突的請求數。

圖4 過濾結果對比

可以看出，在場景3中60%和100%的匹配百分比過濾結果相差無幾，而在場景1和場景2中，卻存在明顯差距。由此可以看到基于最近最多匹配的部分檢查算法適用于流量集中于部分鏈路的情況。

5.2 性能驗證

在性能驗證中，我們對TS檢查器層的沖突檢測器和重疊檢測器及整合器分別進行了不同流表項和請求數量時的測試。我們構建了一個SDN控制器、三個ovs交換機，每個交換機分別連接2個主機的拓撲環境。

首先，我們評估了沖突檢測器的計算時間。因為沖突檢測器中使用了基于最近最多匹配的部分檢查算法，所以其處理時間取決于不同場景下指定的匹配百分比。我們分別測試了100%匹配、66%匹配、33%匹配和20%匹配。從圖5可以看出，隨著流表項數量的增加，所耗費的檢查時間呈線性增長。并且隨著匹配百分比的升高，耗費的檢查時間也逐漸增長。

圖5 流表項數量與沖突檢測時間的關系

之后我們驗證了重疊檢測器和整合器這兩個步驟共同耗費的處理時間。如圖6所示，隨著重疊集數量的增加，處理時間線性增加。這其中大部分時間用于構建和更新字典樹，也就是在重疊檢測器這一步驟中，而整合器步驟耗時很短。

圖6 請求數量和重疊檢測與整合時間的關系

最后我們測試了一個完整的處理流程，使用三個請求生成器分別模擬三個應用先后生成了1 000個請求，三個交換機中的流表項數量分別為6 000，并且設置沖突檢測器的匹配百分比為30%。如表7所示，在此環境中，對于每個請求而言沖突檢測器處理耗時小于1 ms，重疊檢測器和整合器耗時略多，但仍然小于1 ms。

表7 檢查步驟與耗費時間

6 結 語

我們設計、實現并評估了TS檢查器——一個用于在SDN架構中檢測沖突并進行整合以保證網絡狀態一致性的機制。TS檢查器作為檢查層位于應用層與控制層之間，為高效完成沖突檢測，使用字典樹數據結構和基于最近最多匹配的部分檢查算法來減少某些場景下的平均檢查時間。設計了請求隊列以輔助下游實現請求間的重疊檢查和整合。在整合階段，我們提出了整合兩個含重疊域請求的方法。最后使用Mininet驗證了設計，并進行了性能評估。

下一步我們計劃探索用于三條及以上請求之間的整合機制，并且將TS檢查器擴展到多控制器環境中。

[1] OpenFlow: a southbound protocol[OL]. https://www.opennetworking.org/sdn-resources/openflow.

[2] Docker: an app engine[OL]. https://www.docker.com/.

[3] Ryu controller: an open source SDN controller[OL]. https://osrg.github.io/ryu/.

[4] OpenFlow switch specification[OL]. https://www.opennetworking.org/images/stories/downloads/sdn-resources/onf-specifications/openflow/openflow-spec-v1.4.0.pdf.

[5] Mininet[OL]. http://mininet.org/.

[6] Anderson C J, Foster N, Guha A, et al. NetKAT: semantic foundations for networks[C]// ACM Sigplan-Sigact Symposium on Principles of Programming Languages. ACM, 2014:113- 126.

[7] Monsanto C, Reich J, Foster N, et al. Composing software-defined networks[C]// Usenix Conference on Networked Systems Design and Implementation. USENIX Association, 2013:1- 14.

[8] Mogul J C, AuYoung A, Banerjee S, et al. Corybantic: towards the modular composition of SDN control programs[C]//Proceedings of the Twelfth ACM Workshop on Hot Topics in Networks. ACM, 2013: 1- 7.

[9] AuYoung A, Ma Y, Banerjee S, et al. Democratic resolution of resource conflicts between sdn control programs[C]//Proceedings of the 10th ACM International on Conference on emerging Networking Experiments and Technologies. ACM, 2014: 391- 402.

[10] Al-Shaer E, Al-Haj S. FlowChecker: Configuration analysis and verification of federated OpenFlow infrastructures[C]//Proceedings of the 3rd ACM workshop on Assurable and usable security configuration. ACM, 2010: 37- 44.

[11] Porras P, Shin S, Yegneswaran V, et al. A security enforcement kernel for OpenFlow networks[C]//Proceedings of the first workshop on Hot topics in software defined networks. ACM, 2012: 121- 126.

[12] Khurshid A, Zhou W, Caesar M, et al. Veriflow: Verifying network-wide invariants in real time[J]. ACM SIGCOMM Computer Communication Review, 2012, 42(4): 467- 472.

[13] Son S, Shin S, Yegneswaran V, et al. Model checking invariant security properties in OpenFlow[C]//Communications (ICC), 2013 IEEE International Conference on. IEEE, 2013: 1974- 1979.

[14] Prakash C, Lee J, Turner Y, et al. Pga: Using graphs to express and automatically reconcile network policies[J]. ACM SIGCOMM Computer Communication Review, 2015, 45(4): 29- 42.

[15] Jain R. Characteristics of destination address locality in computer networks: a comparison of caching schemes[J]. Computer networks and ISDN systems, 1990, 18(4): 243- 254.