劉 藝 雷 程 張紅旗 楊英杰

(解放軍信息工程大學(xué) 鄭州 450001) (河南省信息安全重點(diǎn)實(shí)驗(yàn)室(解放軍信息工程大學(xué)) 鄭州 450001)(liuyi9582@126.com)

?

基于MapReduce的OpenFlow網(wǎng)絡(luò)屬性驗(yàn)證技術(shù)

劉 藝 雷 程 張紅旗 楊英杰

(解放軍信息工程大學(xué) 鄭州 450001) (河南省信息安全重點(diǎn)實(shí)驗(yàn)室(解放軍信息工程大學(xué)) 鄭州 450001)(liuyi9582@126.com)

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

流表配置；網(wǎng)絡(luò)可達(dá)性分析；網(wǎng)絡(luò)屬性驗(yàn)證；MapReduce模型；OpenFlow網(wǎng)絡(luò)

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

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

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

1 相關(guān)工作

OpenFlow網(wǎng)絡(luò)采用集中式控制方式，中央控制器能提供統(tǒng)一的、確定的網(wǎng)絡(luò)數(shù)據(jù)平面信息[4]，為基于數(shù)據(jù)平面信息的網(wǎng)絡(luò)屬性驗(yàn)證提供了良好的基礎(chǔ).目前，OpenFlow網(wǎng)絡(luò)屬性驗(yàn)證研究主要集中在3個(gè)方面：

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

2) 基于布爾可滿足問(wèn)題的驗(yàn)證.此類研究將網(wǎng)絡(luò)屬性驗(yàn)證問(wèn)題轉(zhuǎn)換為邏輯網(wǎng)絡(luò)的可滿足性問(wèn)題.Anteater將規(guī)則轉(zhuǎn)換為布爾表達(dá)式，和網(wǎng)絡(luò)屬性聯(lián)合起來(lái)組成SAT實(shí)例，輸入到SAT解決器中執(zhí)行分析.

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

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

2 基于MapReduce的OpenFlow網(wǎng)絡(luò)屬性驗(yàn)證技術(shù)

Fig. 1 Technical framework of network property verification technique for OpenFlow network.圖1 OpenFlow網(wǎng)絡(luò)屬性驗(yàn)證技術(shù)架構(gòu)

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

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

2.1 規(guī)則鏈路信息預(yù)處理

依據(jù)OpenFlow標(biāo)準(zhǔn)[15]，規(guī)則r(inport,C,pri,a).其中，inport具有全網(wǎng)唯一性，表示規(guī)則對(duì)從特定端口進(jìn)入其所在交換機(jī)的數(shù)據(jù)包起作用；C為匹配域，包括源/目的IP、端口等匹配字段；pri是規(guī)則優(yōu)先級(jí)；a為動(dòng)作.a主要包括3種：fwd(port)表示將數(shù)據(jù)包從端口port轉(zhuǎn)發(fā)出去；setm→n(port)表示將數(shù)據(jù)包頭由m改為n后從端口port轉(zhuǎn)發(fā)出去；drop表示丟棄數(shù)據(jù)包，為統(tǒng)一起見(jiàn)，可看作從特殊端口port*轉(zhuǎn)發(fā)出去.

2)inport和outport分別為數(shù)據(jù)包進(jìn)入和離開(kāi)交換機(jī)的端口號(hào).

3)flag_r是規(guī)則狀態(tài)標(biāo)識(shí)，僅在實(shí)時(shí)驗(yàn)證時(shí)使用，flag_r=1表示增加規(guī)則，flag_r=0表示刪除規(guī)則.

2.2 基于MapReduce的非實(shí)時(shí)網(wǎng)絡(luò)屬性驗(yàn)證

基于MapReduce的非實(shí)時(shí)網(wǎng)絡(luò)屬性驗(yàn)證流程如圖2所示，Map階段劃分規(guī)則等價(jià)類，Reduce階段基于構(gòu)建的網(wǎng)絡(luò)轉(zhuǎn)發(fā)圖進(jìn)行屬性驗(yàn)證.

Fig. 2 Workflow of non-real-time network property verification.圖2 非實(shí)時(shí)網(wǎng)絡(luò)屬性驗(yàn)證流程

2.2.1 Map階段

Map階段的主要任務(wù)是依據(jù)代理提供的規(guī)則信息劃分規(guī)則等價(jià)類.通常規(guī)則分類有2種方案：

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

2) 基于子網(wǎng)，每個(gè)mapper根據(jù)規(guī)則目的IP地址所屬的子網(wǎng)將規(guī)則劃分入不同等價(jià)類，此種方法能構(gòu)造相對(duì)完整的轉(zhuǎn)發(fā)路徑，reducer之間無(wú)需或者少量通信就能完成驗(yàn)證任務(wù).因此，本文方案以后者為依據(jù)，提出基于子網(wǎng)trie樹(shù)的規(guī)則等價(jià)類劃分.

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

由此，規(guī)則等價(jià)類定義如下：

定義1.規(guī)則等價(jià)類Rw={r1,r2,…,rn}，若網(wǎng)絡(luò)中存在子網(wǎng)w，對(duì)于ri(1≤i≤n)，或者ri匹配w，或者w匹配ri.

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

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

因?yàn)榫W(wǎng)絡(luò)中規(guī)則數(shù)目往往遠(yuǎn)大于子網(wǎng)數(shù)目，所以mapper構(gòu)建子網(wǎng)trie樹(shù)，1個(gè)子網(wǎng)地址對(duì)應(yīng)1個(gè)trie樹(shù)節(jié)點(diǎn)，稱為實(shí)心節(jié)點(diǎn)，空心節(jié)點(diǎn)意味著沒(méi)有對(duì)應(yīng)的子網(wǎng)，但為了構(gòu)建trie樹(shù)必須生成.假設(shè)mapper數(shù)目為N，規(guī)則總數(shù)為S，每個(gè)mapper被分配S/N條規(guī)則，每次讀入1條規(guī)則，提取其目的IP地址，轉(zhuǎn)換為二進(jìn)制數(shù)形式，從子網(wǎng)trie樹(shù)根結(jié)點(diǎn)出發(fā)遍歷，遍歷過(guò)程與傳統(tǒng)路由器進(jìn)行數(shù)據(jù)包轉(zhuǎn)發(fā)時(shí)采用的二進(jìn)制trie樹(shù)查找算法類似，即在每個(gè)內(nèi)部節(jié)點(diǎn)，遇到0遍歷左子樹(shù)，遇到1遍歷右子樹(shù)，但本文的目的是找到與規(guī)則r滿足關(guān)系——r匹配w或者w匹配r——的所有子網(wǎng)w，因此往往無(wú)需遍歷整棵樹(shù).遍歷過(guò)程分2種情況：

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

2)dst(r)≤n，因?yàn)樽泳W(wǎng)trie樹(shù)中任一節(jié)點(diǎn)小于其子孫節(jié)點(diǎn)，所以有dst(r)≤n

直至當(dāng)前節(jié)點(diǎn)無(wú)子孫節(jié)點(diǎn)或出現(xiàn)上述情況2時(shí)，結(jié)束搜索.

對(duì)于wj∈W，mapper輸出wj，規(guī)則信息對(duì)，其中規(guī)則信息為，由子網(wǎng)地址(即wj)標(biāo)識(shí)不同的規(guī)則等價(jià)類.

子網(wǎng)trie樹(shù)的構(gòu)建也可以采用傳統(tǒng)網(wǎng)絡(luò)中的路由表壓縮算法，減小存儲(chǔ)空間，實(shí)現(xiàn)快速更新.

2.2.2 Reduce階段

Reduce階段的主要任務(wù)是根據(jù)收到的同一子網(wǎng)對(duì)應(yīng)的規(guī)則信息r,outport,pri和所有鏈路信息構(gòu)建網(wǎng)絡(luò)轉(zhuǎn)發(fā)圖進(jìn)行可達(dá)性分析，從而驗(yàn)證網(wǎng)絡(luò)屬性.為了降低網(wǎng)絡(luò)轉(zhuǎn)發(fā)圖規(guī)模、加快可達(dá)性分析效率，本文提出基于交換機(jī)端口謂詞(SP)的網(wǎng)絡(luò)轉(zhuǎn)發(fā)圖構(gòu)建算法和基于原子謂詞(AP)的網(wǎng)絡(luò)可達(dá)性分析算法.

1) 基于SP的網(wǎng)絡(luò)轉(zhuǎn)發(fā)圖構(gòu)建算法

為計(jì)算SP，首先以(inport,pri)為關(guān)鍵字采用最高位優(yōu)先法(most significant digit first, MSD)對(duì)規(guī)則進(jìn)行排序，其中inport是主位關(guān)鍵字，pri為次位關(guān)鍵字，排序結(jié)果如下：

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

算法1. RP_to_SP算法.

輸入: 有序的轉(zhuǎn)發(fā)表、端口集合{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 網(wǎng)絡(luò)拓?fù)浼捌渚W(wǎng)絡(luò)轉(zhuǎn)發(fā)圖

以圖3(a)(b)中的網(wǎng)絡(luò)拓?fù)浼捌渚W(wǎng)絡(luò)轉(zhuǎn)發(fā)圖為例，圖3中節(jié)點(diǎn)以端口號(hào)標(biāo)識(shí)，以SP為節(jié)點(diǎn)值，若端口i是j的內(nèi)部(外部)上游端口，則有1條從節(jié)點(diǎn)i到j(luò)的以虛線(實(shí)線)標(biāo)識(shí)的有向邊，p*是為“drop”動(dòng)作規(guī)則設(shè)置的特殊端口.比如，p6和p7之間無(wú)虛線連接，表示從p6進(jìn)入交換機(jī)的數(shù)據(jù)包不會(huì)從p7轉(zhuǎn)發(fā)出去.

與文獻(xiàn)[14]中以單個(gè)交換機(jī)為節(jié)點(diǎn)、以物理鏈路為邊的轉(zhuǎn)發(fā)圖相比，基于SP的網(wǎng)絡(luò)轉(zhuǎn)發(fā)圖表達(dá)了更加細(xì)粒度的規(guī)則信息，更加符合OpenFlow規(guī)則特點(diǎn).并且與文獻(xiàn)[11]中以規(guī)則為節(jié)點(diǎn)、以規(guī)則關(guān)系為邊的轉(zhuǎn)發(fā)圖相比，它將規(guī)則信息聚合到端口，降低了圖的規(guī)模，減少了存儲(chǔ)開(kāi)銷的同時(shí)也壓縮了之后需要進(jìn)行的圖搜索空間，在時(shí)間和存儲(chǔ)開(kāi)銷方面都更優(yōu).

2) 基于AP的網(wǎng)絡(luò)可達(dá)性分析算法

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

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

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

⑤m是所有滿足條件①～④的謂詞集合的元素?cái)?shù)目最小值.

若以整數(shù){1,2,…,m}標(biāo)識(shí)每個(gè)AP，可得謂詞p對(duì)應(yīng)的整數(shù)集合S(p)?{1,2,…,m}，由此謂詞在多維空間上的合取(析取)轉(zhuǎn)化為更加快速的整數(shù)集合交(并)運(yùn)算，而且AP集合遠(yuǎn)小于Ψ[16]，消除了冗余項(xiàng)，減少了謂詞存儲(chǔ)開(kāi)銷.

算法2. ReTree_path_Build算法.

輸入: 圖G、端口s;

輸出: 端口s可達(dá)樹(shù)的一條路徑.

if (s是輸入端口) then

/*t和temp分別暫時(shí)存儲(chǔ)節(jié)點(diǎn)標(biāo)識(shí)和節(jié)點(diǎn)值*/

while(1)

/*尋找數(shù)據(jù)包能到達(dá)的內(nèi)部下游端口*/

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

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

/*在可達(dá)樹(shù)中增加節(jié)點(diǎn)*/

else

ReTree.add(t,temp);

/*尋找數(shù)據(jù)包能到達(dá)的外部下游端口*/

(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))

{ /*尋找數(shù)據(jù)包能到達(dá)的內(nèi)部下游端口*/

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

路由黑洞報(bào)告; /*發(fā)現(xiàn)路由黑洞*/

(t,temp)←?;

end if

return (t,temp).

}

External_relate(G,(t,temp))

{ /*尋找數(shù)據(jù)包能到達(dá)的外部下游端口*/

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

if (!visisted(v)) then

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

else (t,temp)←?;

end if

else

轉(zhuǎn)發(fā)回路報(bào)告; /*發(fā)現(xiàn)轉(zhuǎn)發(fā)回路*/

(t,temp)←?;

end if

else (t,temp)←?;

end if

return (t,temp).

}

以圖3所示網(wǎng)絡(luò)為例，表1和表2分別是用AP集合表達(dá)的網(wǎng)絡(luò)轉(zhuǎn)發(fā)圖中各節(jié)點(diǎn)輸入和輸出謂詞.

Table 1 Input Predicates of Nodes

Table 2 Output Predicates of Nodes

圖4是端口p1的可達(dá)樹(shù)，它涵蓋了經(jīng)過(guò)和未經(jīng)過(guò)“setm→n(port)”操作的數(shù)據(jù)包轉(zhuǎn)發(fā)路徑信息，假設(shè)驗(yàn)證策略“p1和p11所連主機(jī)不能通信”，由可達(dá)樹(shù)可知，存在數(shù)據(jù)包b3∨b4經(jīng)過(guò)端口序列p1→p2→p4→p5→p7→p8→p10→p11后變?yōu)閎6∨b8到達(dá)p11，故網(wǎng)絡(luò)不滿足該策略.

Fig. 4 Reachability Tree of p1.圖4 端口p1可達(dá)樹(shù)

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

2.3 基于MapReduce的實(shí)時(shí)網(wǎng)絡(luò)屬性驗(yàn)證

基于MapReduce的實(shí)時(shí)網(wǎng)絡(luò)屬性驗(yàn)證建立在非實(shí)時(shí)驗(yàn)證的基礎(chǔ)上，通過(guò)增量更新網(wǎng)絡(luò)轉(zhuǎn)發(fā)圖和端口可達(dá)樹(shù)實(shí)現(xiàn)實(shí)時(shí)網(wǎng)絡(luò)屬性驗(yàn)證，主要分6種情況:

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

Fig. 5 Real-time verification workflow for adding rules.圖5 規(guī)則增加時(shí)實(shí)時(shí)網(wǎng)絡(luò)屬性驗(yàn)證流程

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

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

(1)

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

(2)

(3)

(4)

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

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

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

(5)

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

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

Fig. 6 Updating a single node.圖6 單個(gè)節(jié)點(diǎn)更新示意圖

(6)

由此可得到帶有臨時(shí)謂詞集合的臨時(shí)可達(dá)樹(shù).在完成AP集合更新后，需要將臨時(shí)可達(dá)樹(shù)“轉(zhuǎn)正”，分2種情況：①若AP集合未發(fā)生改變，則只需將Φ中的謂詞轉(zhuǎn)換為相應(yīng)的整數(shù)集合；②若AP集合發(fā)生改變，則基于新的AP集合重新遍歷可達(dá)樹(shù)，計(jì)算相應(yīng)的節(jié)點(diǎn)值.

2) 刪除規(guī)則r.與情況1類似，首先由mapper將r發(fā)送至相應(yīng)的reducer上，reducer根據(jù)r更新SP、AP集合和可達(dá)樹(shù).

3) 增加子網(wǎng).mapper向子網(wǎng)trie樹(shù)中插入新的子網(wǎng)，并計(jì)算其規(guī)則等價(jià)類，reducer為新增等價(jià)類構(gòu)建網(wǎng)絡(luò)轉(zhuǎn)發(fā)圖.

4) 刪除子網(wǎng).mapper將子網(wǎng)從子網(wǎng)trie樹(shù)中刪除，并通知相應(yīng)的reducer刪除與該子網(wǎng)有關(guān)的信息.

5) 啟用新鏈路.網(wǎng)絡(luò)的鏈路狀態(tài)對(duì)SP和AP集合沒(méi)有影響，假設(shè)新鏈路連接2個(gè)端口p1和p2，由HT(p1)(HT(p2))在可達(dá)樹(shù)中定位它們對(duì)應(yīng)的節(jié)點(diǎn)，并以p1(p2)為起點(diǎn)對(duì)增加新鏈路后的網(wǎng)絡(luò)轉(zhuǎn)發(fā)圖進(jìn)行DFS搜索，擴(kuò)展可達(dá)樹(shù)，同時(shí)修改Hash表.

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

2.4 時(shí)間復(fù)雜度分析

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

3 實(shí)驗(yàn)結(jié)果與分析

3.1 實(shí)驗(yàn)條件

本文在Hadoop 2.2.0平臺(tái)上開(kāi)發(fā)MapReduce程序進(jìn)行仿真實(shí)驗(yàn)，硬件選取情況如表3所示，節(jié)點(diǎn)之間以100 Mbps帶寬互聯(lián)，操作系統(tǒng)為Ubuntu 12.04.

Table3 Information of Hadoop Platform Hardware

為與Hassel和NetPlumber等工具進(jìn)行性能對(duì)比，數(shù)據(jù)集采用Stanford大學(xué)主干網(wǎng)[17]數(shù)據(jù)和Internet2[18]數(shù)據(jù)，如表4所示：

Table4 Information of Experimental Datasets

3.2 實(shí)驗(yàn)結(jié)果分析

為驗(yàn)證MRVeri的實(shí)時(shí)與非實(shí)時(shí)驗(yàn)證效率，實(shí)驗(yàn)分為3部分：1)基于整體實(shí)驗(yàn)數(shù)據(jù)集進(jìn)行非實(shí)時(shí)網(wǎng)絡(luò)屬性驗(yàn)證；2)通過(guò)隨機(jī)改變實(shí)驗(yàn)數(shù)據(jù)集中的規(guī)則和鏈路信息模擬動(dòng)態(tài)網(wǎng)絡(luò)進(jìn)行實(shí)時(shí)網(wǎng)絡(luò)屬性驗(yàn)證；3)基于Mininet仿真平臺(tái)評(píng)估MRVeri對(duì)TCP連接建立時(shí)間的影響.

1) 非實(shí)時(shí)網(wǎng)絡(luò)屬性驗(yàn)證實(shí)驗(yàn)

采用MRVeri和Hassel驗(yàn)證Stanford大學(xué)主干網(wǎng)和Internet2中是否存在轉(zhuǎn)發(fā)回路，若存在則返回具體的路徑.其中，對(duì)于Stanford大學(xué)主干網(wǎng)，為與文獻(xiàn)[10]中的結(jié)果進(jìn)行比較，選取30個(gè)端口檢測(cè)轉(zhuǎn)發(fā)回路.實(shí)驗(yàn)結(jié)果顯示，MRVeri和Hassel都在Stanford大學(xué)主干網(wǎng)和Internet2中分別發(fā)現(xiàn)12條和2條回路路徑，時(shí)間開(kāi)銷如表5所示:

Table5 Time Overhead of MRVeri and Hassel

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

Fig. 7 CDF of constructing time for each port reachability tree.圖7 每個(gè)端口可達(dá)樹(shù)的時(shí)間開(kāi)銷CDF圖

2) 實(shí)時(shí)網(wǎng)絡(luò)屬性驗(yàn)證實(shí)驗(yàn)

為評(píng)估MRVeri在實(shí)時(shí)驗(yàn)證方面的性能，分別在規(guī)則增加、規(guī)則刪除、鏈路啟用和鏈路失效這4種情況下測(cè)算更新端口可達(dá)樹(shù)時(shí)間.

為模擬規(guī)則增加場(chǎng)景，先隨機(jī)選取實(shí)驗(yàn)數(shù)據(jù)集中90%規(guī)則構(gòu)造端口可達(dá)樹(shù)，之后將剩下的10%規(guī)則逐條插入.類似地，在規(guī)則刪除實(shí)驗(yàn)中，先對(duì)實(shí)驗(yàn)數(shù)據(jù)集中所有規(guī)則計(jì)算端口可達(dá)樹(shù)，再隨機(jī)選取10%規(guī)則逐條刪除.為模擬鏈路啟用場(chǎng)景，先隨機(jī)選取實(shí)驗(yàn)網(wǎng)絡(luò)拓?fù)渲?0%的鏈路，標(biāo)識(shí)其為不可用，并構(gòu)造端口可達(dá)樹(shù)，之后逐條將這些鏈路的標(biāo)識(shí)修改為可用.鏈路失效場(chǎng)景則是先對(duì)整網(wǎng)計(jì)算端口可達(dá)樹(shù)，再隨機(jī)選取10%的鏈路，逐條標(biāo)識(shí)其為不可用.圖8和圖9分別表示在Stanford主干網(wǎng)和Internet2中端口可達(dá)樹(shù)更新時(shí)間的分布情況.

Fig. 8 CDF of update time of port reachability trees in Stanford.圖8 Stanford主干網(wǎng)端口可達(dá)樹(shù)更新時(shí)間CDF圖

Fig. 9 CDF of update time of port reachability trees in Internet2.圖9 Internet2端口可達(dá)樹(shù)更新時(shí)間CDF圖

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

在規(guī)則增加情況下，MRVeri在Stanford中與NetPlumber相當(dāng)，在Internet2中略優(yōu)于NetPlumber;但在鏈路啟用時(shí)，遠(yuǎn)優(yōu)于NetPlumber，主要因?yàn)榫W(wǎng)絡(luò)鏈路狀態(tài)對(duì)SP和AP集合沒(méi)有影響，只需從受影響的端口出發(fā)進(jìn)行DFS搜索更新可達(dá)樹(shù)，而NetPlumber需要進(jìn)行更多的操作來(lái)更新其所維護(hù)的管道圖.此外在鏈路失效時(shí)Veriflow平均需要1.15 s驗(yàn)證網(wǎng)絡(luò)屬性，相較MRVeri更慢.

Fig. 10 Update time in rule adding case.圖10 規(guī)則增加情況下更新時(shí)間圖

DataSourceNetPlumberMRVeriMeanMedianMeanMedianStanford302021200.10.037Internet2476023200.0240.0052

3) TCP連接建立時(shí)間實(shí)驗(yàn)

Fig. 11 Time of building TCP connection.圖11 TCP連接建立時(shí)間圖

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

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

4 結(jié)束語(yǔ)

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

[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 技術(shù)研究[J]. 軟件學(xué)報(bào), 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

國(guó)家“八六三”高技術(shù)研究發(fā)展計(jì)劃基金項(xiàng)目(2012AA012704)；鄭州市科技領(lǐng)軍人才項(xiàng)目(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).