基于MapReduce的OpenFlow網絡屬性驗證技術

劉 藝 雷 程 張紅旗 楊英杰

(解放軍信息工程大學 鄭州 450001) (河南省信息安全重點實驗室(解放軍信息工程大學) 鄭州 450001)(liuyi9582@126.com)

?

基于MapReduce的OpenFlow網絡屬性驗證技術

劉 藝 雷 程 張紅旗 楊英杰

(解放軍信息工程大學 鄭州 450001) (河南省信息安全重點實驗室(解放軍信息工程大學) 鄭州 450001)(liuyi9582@126.com)

針對OpenFlow網絡中由程序自動改變數據平面狀態方式引起的流表配置錯誤問題，提出1種基于MapReduce的OpenFlow網絡屬性驗證技術.首先，利用OpenFlow網絡控制轉發分離的特點，設計支持實時與非實時2種驗證方式的技術架構.其次，提出基于MapReduce模型的非實時驗證算法，在Map階段劃分規則等價類，在Reduce階段構建基于交換機端口謂詞的網絡轉發圖并分析可達性，以實現對網絡屬性的并行驗證.與此同時，利用原子謂詞消除謂詞集合冗余項和規則匹配域轉換的方法，提高可達性分析效率.此外，在非實時驗證算法的基礎上，結合網絡更新事件提出實時驗證算法，實現網絡狀態改變時的增量式網絡屬性驗證.最后，理論分析和仿真實驗驗證了該技術的運行效率和存儲開銷，并分析了其對TCP連接建立時間的影響.

流表配置；網絡可達性分析；網絡屬性驗證；MapReduce模型；OpenFlow網絡

軟件定義網絡[1](software-defined networking， SDN)是美國斯坦福大學CleanSlate項目組提出的1種邏輯控制和數據轉發分離的網絡架構，基于OpenFlow[2]實現SDN已成為主流趨勢[3].在OpenFlow網絡中，研究人員通過在中央控制器上開發應用程序，驅動其生成、維護和下發流表，并由OpenFlow交換機簡單地按照流表匹配執行，從而靈活控制管理網絡.然而，這種自動化的軟件管控網絡方式存在安全問題.單個程序的高復雜性和多個程序間的競爭關系導致流表配置易出錯，網絡數據平面狀態屬性與預期不符，如存在轉發回路、出現路由黑洞、訪問控制規則失效等，造成交換機無法正確轉發數據包，這不僅降低了網絡性能，而且違反安全策略危害網絡安全[4].

針對這一問題，一種解決方法是從控制平面角度，在應用程序部署前結合網絡拓撲驗證程序的正確性，如NICE[5]采用模型檢查和符號執行2種技術測試控制器程序是否出現缺陷，但由于程序代碼通常是不可訪問的[6]，該方法實用性不高，此外由于它可擴展性較差，不適用于大型程序.另一種解決方法是從數據平面角度，基于數據平面信息進行網絡屬性驗證[7]，即通過分析全網流表規則驗證網絡的全局狀態是否滿足期望的網絡屬性.一般地，OpenFlow網絡屬性驗證是指驗證與功能正確性相關的網絡屬性[4]，如轉發回路、路由黑洞、可達性和數據包目的地控制等.已有的網絡屬性驗證技術如FlowChecker[8]，Anteater[9]，Hassel[10]等普遍耗時長，每次驗證至少需要幾秒，對于現代數據中心網絡等數據平面狀態改變頻率能達到每秒上千次[11]的網絡，不能在網絡運行時實時驗證流表配置是否出錯.

因此，針對現有技術存在驗證耗時長、難以滿足實時性需求的問題，本文提出了基于MapReduce的OpenFlow網絡屬性驗證技術(MapReduce-based network property verification technique for OpenFlow network， MRVeri)，支持實時和非實時2種驗證工作模式.通過引入MapReduce模型實現并行驗證和網絡狀態改變時增量驗證，分別加快非實時與實時驗證速度；通過將規則謂詞聚合為交換機端口謂詞和采用原子謂詞將規則匹配域的多維集合運算轉換為整數集合運算進一步提高驗證效率；此外，通過基于原子謂詞的謂詞表示方式消除冗余項降低存儲開銷.

1 相關工作

OpenFlow網絡采用集中式控制方式，中央控制器能提供統一的、確定的網絡數據平面信息[4]，為基于數據平面信息的網絡屬性驗證提供了良好的基礎.目前，OpenFlow網絡屬性驗證研究主要集中在3個方面：

1) 基于有限狀態自動機的驗證.此類研究將數據包看作有限狀態自動機，當前狀態由數據包頭和所處設備定義，下一個狀態由包頭和當前設備的規則決定，驗證網絡屬性等同于檢測終態集合是否存在不期望的狀態.FlowChecker將用2元決策圖(binary decision diagram， BDD)描述的規則和用計算樹邏輯(computation tree logic， CTL)編寫的網絡屬性輸入到SMV中進行驗證.FLOVER[12]將規則和網絡屬性翻譯為Yices斷言，利用Yices SMT進行驗證.Hassel將數據包定義為幾何空間中的點，規則對數據包的動作定義為該幾何空間中的轉換函數，設計了多種算法驗證不同的網絡屬性.

2) 基于布爾可滿足問題的驗證.此類研究將網絡屬性驗證問題轉換為邏輯網絡的可滿足性問題.Anteater將規則轉換為布爾表達式，和網絡屬性聯合起來組成SAT實例，輸入到SAT解決器中執行分析.

3) 基于圖的驗證.此類研究以圖的形式組織全網規則，借助圖搜索算法計算網絡可達性，從而驗證網絡屬性.VeriFlow[13]通過劃分規則等價類和建立轉發圖高速緩存實現實時驗證，但當規則有多個匹配字段時規則等價類的數目可能相當大，會影響驗證速率.NetPlumber[11]通過設計管道圖(plumbing graph)及其增量更新算法實現實時驗證，并提出規則聚類技術使得當規則更新時多個規則類能獨立驗證，但在鏈路狀態變化時耗時長.Libra[14]首次引入MapReduce實現并行驗證，但它建立在數據包只基于目的IP地址前綴進行轉發的基礎上，不適用于OpenFlow網絡.

經分析可知，從時間開銷來看，基于有限狀態自動機和基于布爾可滿足問題的驗證技術普遍速度慢，適合以非實時方式驗證網絡屬性；基于圖的驗證技術速度有所提高，但仍有提升空間，而且在鏈路狀態改變情況下耗時長.從存儲開銷來看，已有研究普遍未考慮壓縮規則信息，降低存儲開銷.因此，亟需1種支持實時和非實時2種方式、速度快且存儲開銷小的OpenFlow網絡屬性驗證技術，以解決規則和鏈路更新造成網絡數據平面狀態出錯的問題.

2 基于MapReduce的OpenFlow網絡屬性驗證技術

Fig. 1 Technical framework of network property verification technique for OpenFlow network.圖1 OpenFlow網絡屬性驗證技術架構

OpenFlow網絡的集中控制特性為自動化網絡屬性驗證提供了契機[11].結合OpenFlow網絡控制轉發分離特點，本文提出了支持實時和非實時驗證功能的OpenFlow網絡屬性驗證技術，其技術架構如圖1所示，主要包括位于中央控制器和交換機之間的驗證代理和驗證器2部分.非實時驗證指在規則下發到交換機后對網絡數據平面快照(即全網規則和鏈路信息)進行整體驗證，是實時驗證的基礎，一般用于狀態改變不頻繁的網絡，可以減少網絡通信資源消耗，主要實現步驟如圖1中①②③④所示，驗證器在收到網絡管理員發送的網絡屬性驗證請求后，通知驗證代理獲取數據平面快照，隨后對返回的快照進行驗證，將結果反饋給管理員，管理員可依此調整網絡.實時驗證指驗證過程發生在規則下發到交換機前或網絡數據平面發生鏈路更新等狀態改變事件時，為了不影響網絡運行通常是基于非實時驗證結果進行增量式驗證，一般用于狀態頻繁改變的網絡，主要實現步驟如圖1中⑤⑥⑦所示，驗證代理從控制器與交換機的通信報文中提取有用信息發送給驗證器進行驗證，并根據收到的驗證結果執行既定操作，如拒絕規則更新或發出警報等.

由此可知，OpenFlow網絡屬性驗證技術的核心在于驗證器上運行的驗證算法.由于網絡規模大、規則數目多，為了提高驗證速率，在進行非實時驗證時，需要分解驗證任務實現并行驗證；在進行實時驗證時，需要只分析受規則或鏈路更新影響的部分網絡實現增量驗證，因此驗證算法引入MapReduce模型.首先進行規則鏈路信息預處理，之后，在非實時驗證時，Map階段按照規則匹配域劃分規則等價類，Reduce階段按規則等價類將規則組織成若干子圖，獨立、并行地進行分析；在實時驗證時，Map階段由規則或鏈路更新信息確定受影響的規則等價類，Reduce階段對相應子圖進行增量更新及分析.

2.1 規則鏈路信息預處理

依據OpenFlow標準[15]，規則r(inport,C,pri,a).其中，inport具有全網唯一性，表示規則對從特定端口進入其所在交換機的數據包起作用；C為匹配域，包括源/目的IP、端口等匹配字段；pri是規則優先級；a為動作.a主要包括3種：fwd(port)表示將數據包從端口port轉發出去；setm→n(port)表示將數據包頭由m改為n后從端口port轉發出去；drop表示丟棄數據包，為統一起見，可看作從特殊端口port*轉發出去.

2)inport和outport分別為數據包進入和離開交換機的端口號.

3)flag_r是規則狀態標識，僅在實時驗證時使用，flag_r=1表示增加規則，flag_r=0表示刪除規則.

2.2 基于MapReduce的非實時網絡屬性驗證

基于MapReduce的非實時網絡屬性驗證流程如圖2所示，Map階段劃分規則等價類，Reduce階段基于構建的網絡轉發圖進行屬性驗證.

Fig. 2 Workflow of non-real-time network property verification.圖2 非實時網絡屬性驗證流程

2.2.1 Map階段

Map階段的主要任務是依據代理提供的規則信息劃分規則等價類.通常規則分類有2種方案：

1) 基于交換機，每個mapper根據規則所屬交換機的標識將其交付給不同reducer，但由于規則存在復雜的依賴關系，reducer在驗證過程中需要頻繁通信，即使是1條規則發生改變也可能需要多個reducer重新執行驗證，而且不同交換機上的規則數目差異大；

2) 基于子網，每個mapper根據規則目的IP地址所屬的子網將規則劃分入不同等價類，此種方法能構造相對完整的轉發路徑，reducer之間無需或者少量通信就能完成驗證任務.因此，本文方案以后者為依據，提出基于子網trie樹的規則等價類劃分.

記wspa,dst(r)spa分別表示子網w的地址空間范圍和規則r的目的IP地址空間范圍，若wspa?dst(r)spa，則稱規則r匹配子網w；若dst(r)spa?wspa，則稱子網w匹配規則r.

由此，規則等價類定義如下：

定義1.規則等價類Rw={r1,r2,…,rn}，若網絡中存在子網w，對于ri(1≤i≤n)，或者ri匹配w，或者w匹配ri.

將規則r分入不同的規則等價類，即找到子網集合W={w1,w2,…,wm}，對于wj(1≤j≤m)，或者r匹配wj，或者wj匹配r.

為快速找到W，將規則目的IP地址和子網地址轉化為二進制數形式，dst(r)={0,1,x}λ(可從Pr中獲得)，w={0,1,x}λ，其中λ表示地址長度.假設x<0<1，則按從高位到低位的順序比較，2個地址具有大小關系.據此，規則r匹配子網w意味著dst(r)≤w，子網w匹配規則r意味著dst(r)≥w.

因為網絡中規則數目往往遠大于子網數目，所以mapper構建子網trie樹，1個子網地址對應1個trie樹節點，稱為實心節點，空心節點意味著沒有對應的子網，但為了構建trie樹必須生成.假設mapper數目為N，規則總數為S，每個mapper被分配S/N條規則，每次讀入1條規則，提取其目的IP地址，轉換為二進制數形式，從子網trie樹根結點出發遍歷，遍歷過程與傳統路由器進行數據包轉發時采用的二進制trie樹查找算法類似，即在每個內部節點，遇到0遍歷左子樹，遇到1遍歷右子樹，但本文的目的是找到與規則r滿足關系——r匹配w或者w匹配r——的所有子網w，因此往往無需遍歷整棵樹.遍歷過程分2種情況：

1)dst(r)>n，若n為實心節點，則W=W∪{n}(假設最初W=?)；若n為空心節點，則W=W.

2)dst(r)≤n，因為子網trie樹中任一節點小于其子孫節點，所以有dst(r)≤n

直至當前節點無子孫節點或出現上述情況2時，結束搜索.

對于wj∈W，mapper輸出wj，規則信息對，其中規則信息為，由子網地址(即wj)標識不同的規則等價類.

子網trie樹的構建也可以采用傳統網絡中的路由表壓縮算法，減小存儲空間，實現快速更新.

2.2.2 Reduce階段

Reduce階段的主要任務是根據收到的同一子網對應的規則信息r,outport,pri和所有鏈路信息構建網絡轉發圖進行可達性分析，從而驗證網絡屬性.為了降低網絡轉發圖規模、加快可達性分析效率，本文提出基于交換機端口謂詞(SP)的網絡轉發圖構建算法和基于原子謂詞(AP)的網絡可達性分析算法.

1) 基于SP的網絡轉發圖構建算法

為計算SP，首先以(inport,pri)為關鍵字采用最高位優先法(most significant digit first, MSD)對規則進行排序，其中inport是主位關鍵字，pri為次位關鍵字，排序結果如下：

之后，利用RP_to_SP算法將已排序規則轉換為SP，其中Set(Pr)函數表示將Pr按照相應規則的“setm→n(port)”動作要求進行改變.RP_to_SP算法如下：

算法1. RP_to_SP算法.

輸入: 有序的轉發表、端口集合{1,2,…,k};

forj=1 tokdo

end for

f←false；

g←inport1；

i←1；

whilei≤m

ifinporti=gthen

else

end if

f←f∨Pri；

i←i+1；

else

{f←false,g←inporti,i←i}；

end if

end while

Fig. 3 Network topology and its forwarding graph.圖3 網絡拓撲及其網絡轉發圖

以圖3(a)(b)中的網絡拓撲及其網絡轉發圖為例，圖3中節點以端口號標識，以SP為節點值，若端口i是j的內部(外部)上游端口，則有1條從節點i到j的以虛線(實線)標識的有向邊，p*是為“drop”動作規則設置的特殊端口.比如，p6和p7之間無虛線連接，表示從p6進入交換機的數據包不會從p7轉發出去.

與文獻[14]中以單個交換機為節點、以物理鏈路為邊的轉發圖相比，基于SP的網絡轉發圖表達了更加細粒度的規則信息，更加符合OpenFlow規則特點.并且與文獻[11]中以規則為節點、以規則關系為邊的轉發圖相比，它將規則信息聚合到端口，降低了圖的規模，減少了存儲開銷的同時也壓縮了之后需要進行的圖搜索空間，在時間和存儲開銷方面都更優.

2) 基于AP的網絡可達性分析算法

已有的網絡屬性驗證技術的核心算法是計算網絡可達性.本文基于網絡轉發圖建立端口可達樹，并將網絡屬性等價轉換為端口可達性，通過遍歷端口可達樹進行驗證，同時得到具體的違反信息.然而在計算可達性的過程中，由于規則匹配域的每一維上有許多允許的區間和任意的覆蓋，在最壞情況下，多維集合交并運算的計算復雜度為O(2n)(n是包頭位數).因此，為了提高可達性分析速度，本文引入原子謂詞[16].AP是從給定謂詞集合Ψ中提取的若干謂詞，記AP集合為B(Ψ)={b1,b2,…,bm}，它滿足5個條件：

① ?i∈{1,2,…,m},bi≠false；

③ 若i≠j，則bi∧bj=false；

⑤m是所有滿足條件①～④的謂詞集合的元素數目最小值.

若以整數{1,2,…,m}標識每個AP，可得謂詞p對應的整數集合S(p)?{1,2,…,m}，由此謂詞在多維空間上的合取(析取)轉化為更加快速的整數集合交(并)運算，而且AP集合遠小于Ψ[16]，消除了冗余項，減少了謂詞存儲開銷.

算法2. ReTree_path_Build算法.

輸入: 圖G、端口s;

輸出: 端口s可達樹的一條路徑.

if (s是輸入端口) then

/*t和temp分別暫時存儲節點標識和節點值*/

while(1)

/*尋找數據包能到達的內部下游端口*/

(t,temp)=Inner_relate(G,(t,temp));

if (IsEmpty((t,temp))) then break;

/*在可達樹中增加節點*/

else

ReTree.add(t,temp);

/*尋找數據包能到達的外部下游端口*/

(t,temp)=External_relate(G,(t,temp));

if (IsEmpty((t,temp))) then break;

elseReTree.add(t,temp);

end if

end if

end while

else

/*S(P)滿足?p,(S(P),p)∈

(t,temp)←(s,∪S(P));

while(1)

(t,temp)=External_relate(G,(t,temp));

if (IsEmpty((t,temp))) then break;

else

ReTree.add(t,temp);

(t,temp)=Inner_relate(G,(t,temp));

if (IsEmpty((t,temp))) then break;

elseReTree.add(t,temp);

end if

end if

end while

end if

Inner_relate(G,(t,temp))

{ /*尋找數據包能到達的內部下游端口*/

if (?v,v=in_next(G,t)) then

temp∩S(P)≠?) then

S(v)=temp∩S(P);

end if

temp∩S(P)≠?) then

S(v)=S(v)∪Set(temp∩S(P));

(t,temp)←(v,S(v));

else (t,temp)←?;

end if

else

路由黑洞報告; /*發現路由黑洞*/

(t,temp)←?;

end if

return (t,temp).

}

External_relate(G,(t,temp))

{ /*尋找數據包能到達的外部下游端口*/

if (?v,v=out_next(G,t)) then

if (!visisted(v)) then

(t,temp)←(v,S(v));

else (t,temp)←?;

end if

else

轉發回路報告; /*發現轉發回路*/

(t,temp)←?;

end if

else (t,temp)←?;

end if

return (t,temp).

}

以圖3所示網絡為例，表1和表2分別是用AP集合表達的網絡轉發圖中各節點輸入和輸出謂詞.

Table 1 Input Predicates of Nodes

Table 2 Output Predicates of Nodes

圖4是端口p1的可達樹，它涵蓋了經過和未經過“setm→n(port)”操作的數據包轉發路徑信息，假設驗證策略“p1和p11所連主機不能通信”，由可達樹可知，存在數據包b3∨b4經過端口序列p1→p2→p4→p5→p7→p8→p10→p11后變為b6∨b8到達p11，故網絡不滿足該策略.

Fig. 4 Reachability Tree of p1.圖4 端口p1可達樹

此外，為了加快驗證速度，可在樹節點中存儲從根節點到該節點的路徑上的端口序列，并為每棵可達樹維護1張Hash表(HT)，它由一系列關鍵字，值對組成，其中“關鍵字”是端口號v，“值”是樹中標識為v的節點集合，則由HT(v)可得v在可達樹中對應的節點，節點值為從端口s到v的數據包集合，存儲的端口序列為具體路徑信息.比如在驗證路徑點(waypoint)策略時，如從端口s到d的數據包必須經過某個路徑點，如端口m，可由HT(d)得到d對應的節點，通過檢查該節點中存儲的端口序列是否存在m進行驗證.采用相似的方法可以驗證更加復雜的路徑點策略，如所有來自端口s的數據包應該經過某個路徑點集合，或者所有從端口s到d的數據包應該按序經過指定的路徑點序列.

2.3 基于MapReduce的實時網絡屬性驗證

基于MapReduce的實時網絡屬性驗證建立在非實時驗證的基礎上，通過增量更新網絡轉發圖和端口可達樹實現實時網絡屬性驗證，主要分6種情況:

1) 增加規則rnew.如圖5所示，mapper將規則的目的IP地址與子網trie樹進行匹配，輸出w，規則信息對，發送至不同reducer上.reducer需要：①根據rnew的規則信息更新相應SP；②更新AP集合；③使用更新后的SP和AP集合更新網絡轉發圖和端口可達樹.為提高處理速度，步驟②③可并行進行.

Fig. 5 Real-time verification workflow for adding rules.圖5 規則增加時實時網絡屬性驗證流程

在步驟①中，由于rnew的RP可能與已有規則的RP存在交集，為了加快更新速度，規則列表中增設字段Ri表示實際能被規則ri處理的數據包集合，如式(1)所示：

Ri=Pri∧(∨inportj=inporti,Prj∩Pri≠?,prij>prii

(1)

則對于端口x，SP中各元素如式(2)～(4)所示：

(2)

(3)

(4)

在步驟②中，SP的改變可能導致AP集合變化.假設原有AP集合為B({p1,p2,…pn})，當增加謂詞pnew時，按照式(5)計算新的AP集合.

Β({p1,p2,…,pn}∪{pnew})={bk=ak1∧ck2|

ak1∈B({p1,p2,…pn}),

(5)

當刪除謂詞pold時，原有AP集合可能不滿足2.2.2節中條件⑤，需要最小化.基本思路是以prt(bi)={pj|i∈S(pj),1≤j≤n}衡量AP的表達能力，對于2個不同的b,b′∈B({p1,p2,…，pn})，若prt(b)=prt(b′)，則將它們融合，采用文獻[16]中最小化AP集合算法可得B({p1,p2,…,pn}-pold).

在步驟③中，若端口x的SP在步驟①中被改變，則需要更新含有x的可達樹.利用每棵可達樹的Hash表計算x所在節點(即HT(x))，對該節點及其子孫節點的節點值進行更新.單個節點的更新如圖6所示：

Fig. 6 Updating a single node.圖6 單個節點更新示意圖

(6)

由此可得到帶有臨時謂詞集合的臨時可達樹.在完成AP集合更新后，需要將臨時可達樹“轉正”，分2種情況：①若AP集合未發生改變，則只需將Φ中的謂詞轉換為相應的整數集合；②若AP集合發生改變，則基于新的AP集合重新遍歷可達樹，計算相應的節點值.

2) 刪除規則r.與情況1類似，首先由mapper將r發送至相應的reducer上，reducer根據r更新SP、AP集合和可達樹.

3) 增加子網.mapper向子網trie樹中插入新的子網，并計算其規則等價類，reducer為新增等價類構建網絡轉發圖.

4) 刪除子網.mapper將子網從子網trie樹中刪除，并通知相應的reducer刪除與該子網有關的信息.

5) 啟用新鏈路.網絡的鏈路狀態對SP和AP集合沒有影響，假設新鏈路連接2個端口p1和p2，由HT(p1)(HT(p2))在可達樹中定位它們對應的節點，并以p1(p2)為起點對增加新鏈路后的網絡轉發圖進行DFS搜索，擴展可達樹，同時修改Hash表.

6) 中斷舊鏈路.與情況5類似，由HT(p1)(HT(p2))在可達樹中定位節點，刪除這些節點及其子孫節點，并修改Hash表.

2.4 時間復雜度分析

由于實時網絡屬性驗證是對非實時驗證中的SP，AP集合和端口可達樹進行增量式更新，在最壞情況下退化為非實時驗證，故本文只分析非實時網絡屬性驗證的時間復雜度.Map階段的時間開銷分為構建子網trie樹和遍歷子網trie樹2部分.因為向trie樹插入IP地址前綴相當于對trie樹進行查找，其時間是小于或等于IP地址長度的常量，所以構建子網trie樹的時間復雜度為O(w)，其中w是子網數目.同時，若m個mapper共同對r條規則進行等價類劃分，需要O(rm)時間遍歷trie樹，故總的時間復雜度為O(w+rm).Reduce階段的時間開銷分為基于SP構建網絡轉發圖和基于AP分析網絡可達性2部分.以1個reducer為例計算時間復雜度.假設網絡中有e條鏈路和n個交換機，平均每個交換機含有k個端口和1張含m條規則的流表.基于SP構建網絡轉發圖階段，計算SP包括規則排序和執行RP_to_SP算法2項操作，時間復雜度為O(2m+n(k+m))；構建網絡轉發圖主要是尋找內部關聯和外部關聯關系，時間復雜度為O(nk2+e).基于AP分析網絡可達性階段，計算AP集合的時間復雜度取決于給定謂詞集合大小[16]，在最壞情況下每條規則含2個互不重疊的謂詞，給定謂詞集合大小為2mn，時間復雜度為O(mn)；網絡可達性分析的時間開銷與待驗證的網絡屬性有關，在此只分析構建1棵可達樹，主要操作是遍歷轉發圖的邊，在最壞情況下同一交換機上任2個端口之間都存在內部關聯關系，時間復雜度為O(nk2+e).故在最壞情況下總的時間復雜度為O(nk2+nk+mn+e).

3 實驗結果與分析

3.1 實驗條件

本文在Hadoop 2.2.0平臺上開發MapReduce程序進行仿真實驗，硬件選取情況如表3所示，節點之間以100 Mbps帶寬互聯，操作系統為Ubuntu 12.04.

Table3 Information of Hadoop Platform Hardware

為與Hassel和NetPlumber等工具進行性能對比，數據集采用Stanford大學主干網[17]數據和Internet2[18]數據，如表4所示：

Table4 Information of Experimental Datasets

3.2 實驗結果分析

為驗證MRVeri的實時與非實時驗證效率，實驗分為3部分：1)基于整體實驗數據集進行非實時網絡屬性驗證；2)通過隨機改變實驗數據集中的規則和鏈路信息模擬動態網絡進行實時網絡屬性驗證；3)基于Mininet仿真平臺評估MRVeri對TCP連接建立時間的影響.

1) 非實時網絡屬性驗證實驗

采用MRVeri和Hassel驗證Stanford大學主干網和Internet2中是否存在轉發回路，若存在則返回具體的路徑.其中，對于Stanford大學主干網，為與文獻[10]中的結果進行比較，選取30個端口檢測轉發回路.實驗結果顯示，MRVeri和Hassel都在Stanford大學主干網和Internet2中分別發現12條和2條回路路徑，時間開銷如表5所示:

Table5 Time Overhead of MRVeri and Hassel

由表5可看出，MRVeri的速率比Hassel分別快約37倍和45倍.原因有3點：1)引入了MapReduce，可以實現并行驗證；2)構造端口可達樹的速度快，為證明這一點，在MRVeri(只采用1個reducer)和Hassel都完成規則預處理后，隨機選取端口計算可達樹，每個端口可達樹的時間開銷CDF圖如圖7所示，可知MRVeri最大耗時不足1ms，明顯快于Hassel；3)AP集合可以壓縮真實網絡中規則的大量冗余，如Stanford大學主干網和Internet2的AP集合大小分別為509和216，遠小于其規則數目.

Fig. 7 CDF of constructing time for each port reachability tree.圖7 每個端口可達樹的時間開銷CDF圖

2) 實時網絡屬性驗證實驗

為評估MRVeri在實時驗證方面的性能，分別在規則增加、規則刪除、鏈路啟用和鏈路失效這4種情況下測算更新端口可達樹時間.

為模擬規則增加場景，先隨機選取實驗數據集中90%規則構造端口可達樹，之后將剩下的10%規則逐條插入.類似地，在規則刪除實驗中，先對實驗數據集中所有規則計算端口可達樹，再隨機選取10%規則逐條刪除.為模擬鏈路啟用場景，先隨機選取實驗網絡拓撲中10%的鏈路，標識其為不可用，并構造端口可達樹，之后逐條將這些鏈路的標識修改為可用.鏈路失效場景則是先對整網計算端口可達樹，再隨機選取10%的鏈路，逐條標識其為不可用.圖8和圖9分別表示在Stanford主干網和Internet2中端口可達樹更新時間的分布情況.

Fig. 8 CDF of update time of port reachability trees in Stanford.圖8 Stanford主干網端口可達樹更新時間CDF圖

Fig. 9 CDF of update time of port reachability trees in Internet2.圖9 Internet2端口可達樹更新時間CDF圖

由圖8和圖9可知，當規則增加時，MRVeri對Stanford主干網和Internet2中絕大部分可達樹進行更新的時間分別小于0.37 ms和0.7 ms；當規則刪除時，分別小于0.5 ms和1 ms；當鏈路啟用時，分別小于1.01 ms和0.28 ms；當鏈路失效時，更新時間最快，分別小于0.007 ms和0.002 ms.與文獻[11]中NetPlumber在規則增加和鏈路啟用情況下的更新時間對比分別如圖10和表6所示.

在規則增加情況下，MRVeri在Stanford中與NetPlumber相當，在Internet2中略優于NetPlumber;但在鏈路啟用時，遠優于NetPlumber，主要因為網絡鏈路狀態對SP和AP集合沒有影響，只需從受影響的端口出發進行DFS搜索更新可達樹，而NetPlumber需要進行更多的操作來更新其所維護的管道圖.此外在鏈路失效時Veriflow平均需要1.15 s驗證網絡屬性，相較MRVeri更慢.

Fig. 10 Update time in rule adding case.圖10 規則增加情況下更新時間圖

DataSourceNetPlumberMRVeriMeanMedianMeanMedianStanford302021200.10.037Internet2476023200.0240.0052

3) TCP連接建立時間實驗

Fig. 11 Time of building TCP connection.圖11 TCP連接建立時間圖

在Mininet仿真平臺上模擬OpenFlow網絡，它以Floodlight為控制器，具有50個OVS交換機，每個交換機上連接1個主機.運行TCP客戶程序的主機每隔5s隨機向某個運行TCP服務器程序的主機發起連接，并在連接建立后立即釋放，同時，為使Floodlight盡可能多地下發新規則到OVS交換機上，設置規則超時時間為1 s.由于MRVeri包括驗證代理和驗證器2部分，故實驗分別在不運行MRVeri、僅運行驗證代理和完整運行MRVeri的情況下，測試不同數目主機對建立TCP連接的平均時間，結果如圖11所示:

當MRVeri執行實時網絡屬性驗證時，TCP連接建立平均時間增加了約41%，其中驗證代理使其增加約35.4%(驗證算法僅約5.6%)，這是由于驗證代理處于控制器與交換機之間，需要緩存大量通信報文、提取和預處理有用的規則鏈路信息、與底層交換機通信等，可通過將驗證代理納入控制器中減少開銷，從而使屬性驗證過程對終端用戶透明.此外，隨著主機數目的增多，TCP連接建立平均時間的增加幅度未顯著增大.

4 結束語

針對OpenFlow網絡流表配置易出錯問題，本文從數據平面角度出發，提出了基于MapReduce的網絡屬性驗證技術.它通過提供實時和非實時驗證，方便代理或管理員及時調整網絡，減少錯誤配置帶來的損失.針對網絡規模大、規則數目多的特點，通過引入MapReduce實現并行非實時驗證和增量實時驗證.此外，由于網絡屬性驗證是以對網絡轉發圖的可達性分析為基礎，針對已有可達性分析算法速度慢的問題，通過提出RP_to_SP算法聚合規則謂詞，以構建表達信息更細粒度、規模更小的網絡轉發圖；通過采用原子謂詞，將可達性計算過程中規則匹配域的多維集合運算轉換為整數集合運算，以提高效率、消除冗余項和優化驗證存儲開銷.仿真實驗選取了2個實際網絡拓撲和數據，并模擬了OpenFlow網絡中TCP連接建立場景.結果表明,在非實時工作模式下，MRVeri比Hassel分別快約37倍和45倍，存儲開銷分別少約33倍和24倍；在實時工作模式下，當網絡鏈路改變時，MRVeri驗證速度遠優于NetPlumber，Veriflow等現有實時驗證技術，并且其實時驗證算法對TCP連接建立時間影響小.

[1]McKeown N. Software-defined networking[C] //Proc of the 28th IEEE INFOCOM. New York: IEEE Communications Society, 2009: 30-32

[2]McKeown N, Anderson T, Balakrishnan H, et al. OpenFlow: Enabling innovation in campus networks[J]. ACM SIGCOMM Computer Communication Review, 2008, 38(2): 69-74

[3]Zuo Qingyun, Chen Ming, Zhao Guangsong, et al. Research on OpenFlow-Based SDN technologies[J]. Journal of Software, 2013, 24(5): 1078-1097 (in Chinese)

(左青云, 陳鳴, 趙廣松, 等. 基于 Open Flow 的 SDN 技術研究[J]. 軟件學報, 2013, 24(5): 1078-1097)

[4]Zhang S, Malik S, McGeer R. Verification of Computer Switching Networks: An Overview[M]. Berlin: Springer, 2012: 1-16

[5]Canini M, Venzano D, Peresini P, et al. A NICE way to test OpenFlow applications[C] //Proc of the 9th USENIX Symp on Networked System Design and Implementation. Berkeley, CA: USENIX Association, 2012: 127-140

[6]Sherwood R, Gibb G, Yap K K, et al. Can the production network be the testbed?[C] //Proc of the 9th USENIX Symp on Operating Systems Design and Implementation. Berkeley, CA: USENIX Association, 2010: 1-6

[7]McGeer R. Verification of switching network properties using satisfiability[C] //Proc of IEEE ICC’12. Piscataway, NJ: IEEE, 2012: 6638-6644

[8]Al-Shaer E, Al-Haj S. FlowChecker: Configuration analysis and verification of federated OpenFlow infrastructures[C] //Proc of the 3rd ACM Workshop on Assurable and Usable Security Configuration. New York: ACM, 2010: 37-44

[9]Mai H, Khurshid A, Agarwal R, et al. Debugging the data plane with anteater[J]. ACM SIGCOMM Computer Communication Review, 2011, 41(4): 290-301

[10]Kazemian P, Varghese G, McKeown N. Header space analysis: Static checking for networks[C] //Proc of the 9th USENIX Symp on Networked System Design and Implementation. Berkeley, CA: USENIX Association, 2012: 113-126

[11]Kazemian P, Chan M, Zeng H, et al. Real time network policy checking using header space analysis[C] //Proc of the 10th USENIX Symp on Networked System Design and Implementation. Berkeley, CA: USENIX Association, 2013: 99-111

[12]Son S, Shin S, Yegneswaran V, et al. Model checking invariant security properties in OpenFlow[C] //Proc of IEEE ICC’13. Piscataway, NJ: IEEE, 2013: 1974-1979

[13]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

[14]Zeng H, Zhang S, Ye F, et al. Libra: Divide and conquer to verify forwarding tables in huge networks[C] //Proc of the 11th USENIX Symp on Networked System Design and

Implementation. Berkeley, CA: USENIX Association, 2014, 14: 87-99

[15]Openflow Switch Consortium. Openflow switch specification, version 1.0.0[OL]. [2015-03-09]. https://www.open networking.org/images/stories/downloads/sdn-resources/onf-specifications/openflow/openflow-spec-v1.0.0.pdf

[16]Yang H, Lam S S. Real-time verification of network properties using atomic predicates[C] //Proc of IEEE ICNP’13. Piscataway, NJ: IEEE, 2013: 1-11

[17]Atlassian. Header Space Library and NetPlumber[CP/OL]. [2015-04-15]. https://bitbucket.org/peymank/hassel-public

[18]Internet2 Community. The Internet2 Observatory Data Collections[CP/OL]. [2015-04-15]. http://www.internet2.edu/research-solutions/research-support/observatory

Liu Yi, born in 1991. PhD candidate. Her main research interests include SDN security and security policy management.

Lei Cheng, born in 1989. PhD candidate. His main research interests include network security and MTD (leicheng12150@gmail.com).

Zhang Hongqi, born in 1962. Professor and PhD supervisor. His main research interests include network security and classification protection (zhq37922@126. com).

Yang Yingjie, born in 1971. PhD and associate professor. His main research interests include security management and situation awareness (yang-yj1002@263. net).

MapReduce-Based Network Property Verification Technique for OpenFlow Network

Liu Yi, Lei Cheng, Zhang Hongqi, and Yang Yingjie

(PLAInformationEngineeringUniversity,Zhengzhou450001) (HenanKeyLaboratoryofInformationSecurity(PLAInformationEngineeringUniversity),Zhengzhou450001)

Aimed at the problem of configuration errors of flow tables resulting from automatic change of data-plane state by software in OpenFlow network, a MapReduce-based network property verification technique is proposed. Firstly, by exploiting the separation of logic control from data forwarding in OpenFlow network, a novel technical framework providing non-real-time and real-time verification is designed. Further, on the basis of the advantage of parallel computing in MapReduce, a non-real-time verification algorithm is presented, which can verify network properties in parallel in two phases. In Map phase, it slices network into equivalence classes. In Reduce phase, it builds network forwarding graph with switch port predicates and conducts network reachability analysis. Meanwhile, with the help of atomic predicates, it can not only eliminate the redundancy of the set of switch port predicates, but also convert highly computation-intensive operations on predicates to those on sets of integers, speeding up computation of network reachability further. Based on it, a real-time verification algorithm is proposed. According to different network update events, it applies different changes to the results of non-real-time verification in order to incrementally verify properties. Finally, theoretical analysis and experimental results show the low time and storage overhead of the proposed technique. Additionally, its effect on the time of building TCP connection is also analyzed.

flow table configuration; network reachability analysis; network property verification; MapReduce model; OpenFlow network

2015-06-14；

2015-09-06

國家“八六三”高技術研究發展計劃基金項目(2012AA012704)；鄭州市科技領軍人才項目(131PLJRC644)

TP393.08

This work was supported by the National High Technology Research and Development Program of China (863 Program) (2012AA012704) and Zhengzhou Science and Technology Talents Project (131PLJRC644).