基于布爾函數的網絡可達性驗證方法

收稿日期：2022-01-16；修回日期：2022-03-09

作者簡介：張立群（1996-），男，山東青州人，碩士，主要研究方向為軟件定義網絡、網絡安全；林海濤（1974-），男，山東濰坊人，副教授，博士，主要研究方向為信息網絡管理與規劃；沈釗（1980-），男（通信作者），講師，碩士，主要研究方向為通信與信息系統（shenzhao_0@163.com）．

摘 要：針對SDN中由于不同應用的轉發路徑交疊等導致的數據平面配置問題，提出一種基于布爾函數的網絡可達性驗證方法。首先，將網絡拓撲抽象為端口拓撲并計算端口鄰接矩陣；之后，生成網絡的路徑空間和各端口的轉發函數并計算每條路徑的路徑函數；最后通過判斷路徑函數的可滿足性來確定路徑的可達性。通過仿真實驗，對網絡拓撲和流規則規模等因素對算法驗證效率的影響進行研究，并將所提方法與APV和DASDA進行性能比較。實驗結果表明，所提方法能夠有效檢測SDN中的流規則配置問題。隨著網絡中環路的增加和流規則規模的增長，驗證網絡所需的時間開銷逐漸增加。其中，網絡拓撲對路徑生成時間影響較大，而轉發函數的生成時間則主要受流規則規模的影響。方法的驗證時間相較于APV和DASDA分別平均縮短約53.76%和27.74%。

關鍵詞：軟件定義網絡；規則配置；可達性驗證；布爾函數

中圖分類號：TP393.08"" 文獻標志碼：A

文章編號：1001-3695（2022）09-039-2812-06

doi：10.19734/j.issn.1001-3695.2022.01.0049

Network reachability verification method based on Boolean functions

Zhang Liqun，Lin Haitao，Shen Zhao

（College of Electronics Engineering，Naval University of Engineering，Wuhan 430000，China）

Abstract：Aiming at the data plane configuration problem caused by overlapping forwarding paths of different applications in SDN，this paper proposed a Boolean function-based network reachability verification method.Firstly，it abstracted the network topology into port topology and calculated the port adjacency matrix，then it generated the path space of the network and the forwarding function of each port，and calculated the path function of each path.Finally，it judged the accessibility of path from the satisfiability of path function.Through simulation experiments，this paper studied the influence of factors such as network topo-logy and flow rule scale on the algorithm verification efficiency，and the performance of the proposed method was compared with APV and DASDA.Experimental results show that the proposed method can effectively detect flow rule configuration problems in SDN.As the number of loops in the network increases and the size of the flow rules grows，the time overhead required to verify the network gradually increases.Among them，the network topology has a great influence on the path generation time，and the generation time of the forwarding function is mainly affected by the scale of the flow rule.Compared with APV and DASDA，the time to verify is shortened by an average of about 53.76% and 27.74%，respectively.

Key words：software defined network；rule configuration；reachability verification；Boolean functions

0 引言

為了適應新的網絡需求，傳統網絡體系架構經過幾十年的發展增加了大量的網絡協議，這使得整個網絡變得臃腫不堪［1］。為重新定義網絡架構，斯坦福大學在Clean Slate項目中提出了軟件定義網絡［2］（software defined network，SDN）。SDN 的基本理念是構建一個網絡操作系統，使得僅在控制器軟件上進行網絡編程就能管控所有網絡流量。相較于傳統網絡架構，SDN架構具有較好的擴展性、強大的靈活性和快速響應性等特點，被廣泛應用于物聯網和5G開發等大規模網絡應用［3，4］。

但SDN還存在著一些問題，可能導致嚴重的網絡安全事故［5］。首先，部署在控制器中的多個應用對同一轉發平面進行操作，使得不同應用的轉發路徑相互交疊，可能出現多應用的不當依賴。這種不當依賴使得真實的轉發平面與管理員的預期不符，出現轉發環路、非法可達路徑以及數據阻塞等網絡問題，影響網絡的安全和轉發性能［6］，如圖1（a）所示。其次，在主流的南向協議OpenFlow中定義了基于傳輸層安全性協議（transport layer security，TLS）的OpenFlow通道，用于實現控制器對交換機的管理。但由于TLS協議的復雜性，管理員一般使用明文對交換機進行配置管理［7］，這使得在SDN中發生中間人攻擊的概率要大于傳統網絡［8］。攻擊者會利用OpenFlow協議實現欺騙攔截，阻止正常的流量傳輸，或者在交換機中添加新的流規則，控制數據包轉發，使網絡平面脫離管理員控制［9］，如圖1（b）所示。目前，SDN中缺乏有效的網絡驗證機制，難以應對這些控制平面的配置錯誤和網絡攻擊［10］。為此，對網絡可達性驗證的研究具有重要的應用價值。

1 相關工作

文獻［11］提出一種NetPlumber工具，NetPlumber基于頭空間分析［12］（header space analysis，HSA）創建并維護流規則之間的依賴關系圖，該圖將流規則使用管道連接，兩流規則的匹配域交集作為管道的過濾器，以增量的方式動態檢查狀態的合法性變化。文獻［13］提出的NetV同樣是基于HAS的網絡分析工具。與NetPlumber相比，NetV使用二元決策圖解決了通配符表達式在多次并集和差分操作后的爆炸問題，減少了使用不同通配符篩選器執行相同行為規則的冗余。

文獻［14］提出一種高效的流規則沖突檢測方法，通過對全網規則的匹配域進行編碼，實現對流規則的壓縮，進而實現對全網規則沖突的檢測。但由于對規則進行壓縮，所以可能在檢測過程中出現虛報。文獻［15］提出了一種基于原子謂詞驗證（atomic predicates verifier，APV）的方法，該方法通過將訪問控制列表（access control lists，ACL）和轉發表（forward information database，FIB）構造成端口謂詞，并計算謂詞集合的原子謂詞集；然后使用整數集合來表示各個轉發謂詞，構建轉發圖驗證網絡可達性。但當其網絡數目較多時，需要計算大量的原子謂詞；并且當原子謂詞集合進行更新時，表示端口謂詞的整數集合也需要進行調整，驗證效率較低。文獻［16］提出了一種輕量級的包轉發驗證方案（lightweight packet forwarding verification，LPV），通過對交換機出口和入口的隨機采樣，比對采樣包中的相關信息判斷網絡中的異常轉發。但由于需要不斷采樣和上傳，增加了轉發延遲和通信開銷。文獻［17］提出一種基于形式化驗證的沖突檢測解決方案DASDA。DASDA通過底層配置和轉發平面快照驗證SDN拓撲中所有網絡設備的行為。交換機中的流規則被抽象為流規則決策圖（flow entries decision diagram，FeDD），FeDD中的路徑節點代表數據包的各個匹配字段，路徑終點記錄著數據包在網絡中的所有動作。當交換機數目較少時，算法檢測速度相對較快。文獻［18］提出一種方法來驗證請求的路徑集合會不會發生配置錯誤，但該方法只對路徑集合進行了分析，并沒有結合具體的流規則。

針對上述研究存在的虛假預警、驗證效率低以及通信開銷增加等問題，本文提出一種基于布爾函數的網絡可達性驗證（reachability verification based on Boolean functions，RVBBF）方法。RVBBF使用控制器中已有的網絡拓撲和流規則信息，無須與轉發平面進行頻繁通信，減小了通信開銷，并且該方法使用布爾函數對未壓縮的流規則匹配域進行描述，結合物理路徑對數據平面中的可達性和轉發環路進行檢測，消除了虛假預警，提高了驗證效率，增強了SDN的安全性。

2 網絡模型

對于每一個數據包，其都有著確定的源IP地址（記做IPS）和目的IP地址（記做IPD）。在IPv4網絡中，網絡地址由32 bit比特序列表示，本文將數據包抽象為一個64 bit的比特序列（該方法同樣可拓展應用于IPv6），其中前32 bit表示IPS，后32 bit表示IPD。整個數據包空間Ω可以表示為

Ω={（a0，…，a63）|ai∈{0，1}}（1）

當數據包到達交換機時，會將數據包的包頭信息與流規則進行匹配，并根據規則定義的動作處理數據包。流規則一般包含匹配域、動作域、優先級以及計數器等字段。為簡化問題，使得僅通過布爾運算就能判斷數據包與流規則的匹配關系以及求解流規則所能匹配的數據包集合，作出如下定義。

定義1 流規則格式定義，如式（2）所示。

R：〈sw，pri，M，action〉（2）

其中：sw記錄規則所在的交換機；pri表示規則的優先級，其取值為［0，65535］的整數，數值越大則優先級越高；匹配域M=（NetS，NetD），NetS和NetD分別表示規則匹配的源地址網絡和目的地址網絡，兩者皆為前綴匹配字段；action為動作域，表示交換機對數據包的操作。當該數據包到達sw時，將按照所匹配規則的action進行操作。

定義2 交換機對數據包的操作包含轉發和丟棄兩種，對動作域action使用式（3）描述。

action=fwd（Eth）（3）

對于轉發動作，使用本地端口Eth描述，表示將數據包從對應端口轉發；對于丟棄動作，可認為交換機將數據包從特殊的端口Ethd轉發，即action=fwd（Ethd）。

定義3 對于任意流規則R，其可匹配的數據包空間為ΩR，則一定存在一個64元的布爾函數B，使得

B（ω）=trueω∈ΩR

ξ∈ΩRξ∈{ξ|B（ξ）=true}（4）

稱B為流規則R的匹配函數，形式為

B=v0∧v1∧…∧v63（5）

對于匹配函數存在下列性質：

性質1 對于數據包ω0和匹配函數B，若B（ω0）=true，則ω0匹配流規則；否則數據包與該流規則不匹配。

性質2 若B為某一流規則的匹配函數，則B（ω）=true的解空間即為該規則所有可匹配的數據包。

性質3 存在兩個特殊的匹配函數BT和BF，分別有

BT（ω）=true ω∈Ω（6）

BF（ω）=1 ω∈Ω（7）

值得注意的是，并非所有匹配函數都具有全部的64 bit變量。例如，存在流規則R，其匹配域M=（192.168.0.0/16，10.0.0.0/8），則BR如下所示。

BR=v0∧v1∧v2∧v3∧v4∧v5∧v6∧v7∧

v8∧v9∧v10∧v11∧v12∧v13∧v14∧v15∧

v32∧v33∧v34∧v35∧v36∧v37∧v38∧v39

在BR中只包含24 bit變量，這是由于NetS和NetD的網絡前綴分別為16和8。對于NetS來說，需要從v0～v15的16 bit變量即可表示；同理對于NetD，則只需從v32～v39的8 bit變量。

本文使用二元決策圖［19］（binary decision diagram，BDD）來對布爾函數進行表示。BDD是用于表示布爾函數的有向無環圖，可以極大地減小驗證布爾函數滿足性需要的時間開銷，其結構如圖2所示。

3 基于布爾函數的網絡可達性驗證

為解決SDN中缺乏可達性驗證機制的問題，基于第2章網絡模型提出一種基于布爾函數的網絡可達性驗證方法。RVBBF的工作流程包括抽象端口拓撲、計算轉發函數、生成路徑空間和路徑驗證四部分，其流程結構如圖3所示。

RVBBF對流規則和數據包的匹配關系用布爾函數進行描述，并使用路徑搜索算法對轉發平面的拓撲結構進行搜索，生成路徑空間，將網絡可達性問題轉換為布爾可滿足性問題（Boolean satisfiability problem，SAT），使得僅通過簡單的邏輯運算就能夠驗證網絡端到端的可達性。為提高驗證效率，RVBBF對生成路徑空間和計算轉發函數兩階段進行并行處理，使兩者同時進行，并且使用BDD結構表示方法中的布爾函數，有效縮短路徑驗證時間。下面將對RVBBF的各階段工作進行詳細描述。

3.1 抽象端口拓撲

對網絡的物理拓撲進行抽象，可得網絡的端口拓撲，如圖4所示。在端口拓撲中，節點表示設備端口，分為交換機節點和主機節點；邊表示端口之間的連接關系，實線為外部連接，即端口位于不同交換機且存在物理鏈路，虛線為內部連接，即端口位于同一交換機。

為方便后續研究，將〈sw，eth〉映射為全局端口P，映射規則記為D。例如在上述拓撲中有

D［〈Sw 1，Eth-0〉］→P1

D［〈Sw 1，Eth-1〉］→P0

由D和各端口的連接關系，可得網絡拓撲的鄰接矩陣E，其中eij∈{-1，0，1}表示端口Pi和Pj的連接關系。若eij=-1，表示兩節點為內部連接；若eij=0，表示兩節點無連接；若eij=1，則表示兩節點為外部連接。上述拓撲的鄰接矩陣如下所示：

E=0-1-110000000000

-10-100000000010

-1-1000000000100

Euclid ExtraOAp

00000010000000

3.2 計算轉發函數

匹配函數B可以求得流規則所匹配的數據包，但在交換機內部存在大量的流規則，并且優先級和轉發端口各異，難以用其表征交換機的轉發動作。為此類比匹配函數，對轉發函數進行如下定義。

定義4 對于任意的交換機端口P，通過其轉發的數據包空間為ΩP，則一定存在一個64元的布爾函數FP，使得

FP（ω）=trueω∈ΩP

ξ∈ΩPξ∈{ξ|FP（ξ）=true}（8）

稱布爾函數FP為端口P的轉發函數。

根據流規則集合和D可計算任意端口的轉發函數FP，其步驟如下：

首先，通過算法1，對獲取的流規則進行預處理，計算其匹配函數，并將端口映射為全局端口，得到使用匹配函數表示的流規則〈sw，pri，B，P〉。

算法1 流規則預處理

輸入： 〈sw，pri，M，action〉 ，D。

輸出： 〈sw，pri，B，P〉。

1M′←tran（M）

2B←BT；

3for i←1 to len（M′） do

4" switch（M′［i］）

5" case 0：

6"" B←B∧vi；

7" case 1：

8"" B←B∧vi；

9" case *：

10" skip；

11 end switch

12end for

13Eth←get_Eth（action）

14P←D［〈sw，Eth〉］

15return 〈sw，pri，B，P〉

在算法1中，函數tran（）將M轉換為三元序列M′。

M′∈{（m0，…，m63）|mi∈{0，1，*}}

其中：（m0，…，m31）表示NetS；（m32，…，m63）表示NetD，*為通配符。若M′的第i位為1或0，取位變量vi或vi；若第i位為*，則跳過位變量vi。所有位變量的析取即為該流規則的匹配函數。get_Eth（）則根據action獲取本地轉發端口Eth，之后根據D將〈sw，Eth〉映射為P。

數據包在交換機內進行規則匹配時，是按照優先級進行的，數值越大，優先級越高。為實現對同一交換機中高優先級的流規則優先處理，將規則以（sw，pri）為關鍵字進行排序，其中sw為主關鍵字，進行升序排列，pri為次關鍵字，進行降序排列。可得到有序的流規則列表，如下所示。

〈sw1，pri1，B1，P1〉

〈swj，prij，Bj，Pj〉

〈swm，prim，Bm，Pm〉

其中：對于相同sw的規則，若jlt;k，有prij≥prik。

最后通過算法2，根據有序的規則列表和端口集合，計算各個端口的轉發函數。

算法2 計算轉發函數

輸入：有序的流規則列表，端口集合{1，2，…，n}。

輸出：轉發函數集合{F1，…，Fn}。

1 for j←1 to n do

2"" Fj←BF；

3 end for

4 fd←BF；

5 s←sw1；

6 i←1；

7 while i≤m do

8""" if swi=s then

9"""" FPi←FPi∨（Bi∧fd）

10""" fd←fd∨Bi

11""" i←i+1

12"" else

13""" fd←BF

14""" s←swi

15""" i←i

16"" end if

17end while

18return {F1，F2，…，Fn}

3.3 生成路徑空間

按照真實網絡中的轉發模式，數據包一般是從交換機的某一端口PM進入，通過內部連接到轉發端口PN，然后從PN通過外部連接轉發至另一交換機的端口PX進入交換機，不斷重復，如圖5所示。為此，根據鄰接矩陣E和起始端口P，可生成P的路徑空間SetP。

路徑空間中的基本元素是物理可達路徑path，并具有以下特點：a）path以某一主機節點作為起始節點，通過外部連接與交換機節點相連，而后通過內部連接與同一交換機的節點相連，交替進行；b）當訪問到已訪問過交換機的節點時，path結束；c）當訪問到已訪問過的節點時，path結束；d）當訪問到主機節點時，path結束。

通過基于深度優先搜索（depth first search，DFS）的算法3，可由拓撲的鄰接矩陣和起始節點生成路徑空間SetP。

算法3 生成路徑空間

輸入：鄰接矩陣E，起始節點P。

輸出：路徑空間SetP={path1，…，pathk}。

1 now=P；SetP←；

2 path←［now］；

3 while true do

4""" while true do

5"""""" if find_next（now） then

6"""""""" now←find_next（now）；

7"""""" else

8"""""""" break；

9"""""" end if

10""""" path.append（now）

11""""" if now or （now.Sw is visited） then

12"""""" break；

13""""" end if

14""" end while

15""" SetP←SetP∪{path}

16""" while continue_back（） do

17""""" path.pop（）

18""""" if len（path）=0 then

19"""""" break；

20""""" end if

21""""" now←path［-1］

22""" end while

23""" if find_over（） then

24"""" break

25"" end if

26 end while

27 return SetP

其中，函數find_next（）可以返回當前正在訪問節點now可達但尚未訪問的下一跳節點；當now的所有可達節點都被訪問過后，continue_back（）返回true，路徑回溯；若now=P且now的所有可達節點都已訪問，則所有路徑都已經找到，函數check_over（）返回為true，算法結束并返回路徑空間SetP。

3.4 路徑驗證

SetP中的path只是物理可達并不一定邏輯可達，即交換機不一定存在相應的流規則來轉發數據包。通過算法4對所有的物理可達路徑進行驗證，在這個過程中，可以檢測路徑包含的環路以及可達性。

算法4 路徑可達性驗證

輸入：路徑空間SetP，轉發函數集{F1，…，Fn}。

輸出：循環路徑空間Cir、可達路徑空間Rea。

1 for path in SetP do

2"" Bpt←BT；

3"" for P in path do

4"""" if P is Output then

5""""" Bpt←Bpt∧FP；

6"""" end if

7"" end for

8"" if SAT（Bpt） then

9"""" if path.tail in path-path.tail then

10""""" Cir←Cir∪{path}；

11""" else

12""""" Rea←Rea∪{path}；

13""" end if

14"" end if

15end for

16return Cir，Rea

算法4通過遍歷路徑空間，對路徑中輸出端口的轉發函數F進行合取得到路徑函數Bpt，然后對Bpt進行SAT驗證。若存在可滿足的解，則存在數據包能夠同時通過路徑上所有的轉發端口，其解空間就是可通過該路徑的數據包集合，路徑存在邏輯通路。之后再對路徑屬性進行判斷，若路徑的終端節點在路徑中重復出現，則表明該路徑是循環路徑，否則為單向可達路徑。若解不存在，說明不存在數據包可以通過該條路徑上所有轉發端口，即路徑邏輯不可達。

4 實驗分析

4.1 實驗條件

本文實驗計算機的配置如下：Intel Core i7-9750H CPU 2.6 GHz處理器，16 GB內存，Windows 10操作系統。在Visual Studio Code平臺上基于Python語言對該方法進行實現。在性能分析實驗中，不同規模的流規則集合為通過使用Classbench工具隨機生成。

4.2 實驗結果與分析

4.2.1 有效性分析

為驗證RVBBF的有效性，對引言中所提的網絡場景進行分析驗證，其端口拓撲（省略內部連接）及映射關系如圖6所示。以H1（在兩圖中均為節點9）為起始節點生成路徑空間，兩場景的路徑空間如表1所示（加粗路徑表示邏輯可達）。

結合轉發函數對表1路徑進行驗證，發現場景1中存在一條轉發環路［9，0，3，4，5，6，7，2］和一條非法可達路徑［9，0，1，10］；在場景2中則只有一條數據通路［9，0，4］，其中節點4為〈Sw0，Ethd〉，表明Sw1可能受到攻擊或規則設置錯誤，造成數據阻塞。結果表明，RVBBF能夠有效檢測網絡中由于應用的不當依賴和網絡攻擊導致的流規則沖突。

4.2.2 性能分析

為驗證RVBBF的性能，本節通過改變網絡拓撲和流規則數目等參數，對算法各部分驗證效率進行分析。為提高準確性，本節數據均為多次實驗取平均值。

1） 網絡拓撲對生成路徑空間的影響

在實驗中設置五臺交換機，分別組成線型、環型和網狀三種典型的基本網絡拓撲，如圖7所示。通過改變不同拓撲下的終端主機數量，研究網絡拓撲對路徑空間生成時間的影響，實驗結果如圖8所示。各個拓撲的路徑空間（由于終端主機地位對等，任取其一作為起始節點）大小如表2所示。

由表2和圖8可以看出，在相同拓撲下，隨著主機數量的增多，路徑數量和生成時間也逐漸增加，且不同拓撲之間的差距逐漸增大。網狀拓撲的路徑空間生成時間要明顯高于線型拓撲和環型拓撲。這是由于在網狀拓撲中具有較多可達環路，增加相同數目的主機使得增加的物理可達路徑會更多，在生成路徑空間時需要消耗較多的時間。在相同交換機數目的情況下，環型拓撲和網狀拓撲的路徑生成時間平均約為線型拓撲的3.02倍和10.83倍。

2）流規則規模對轉發函數生成的影響

隨機生成不同數量的流規則集合，研究流規則規模對轉發函數生成的影響，結果如圖9所示。

由圖9可以看出，三種拓撲的轉發函數生成時間在相同規則規模下幾乎相等，且隨著規模的增加而增加。這是由于該階段需要對預處理后流規則的匹配函數進行析取、合取和求反等操作。每一條規則進行的操作相似。為此，端口函數的生成時間會隨著流規則的規模逐漸增加，且基本成線型關系。

3）流規則數目對路徑驗證的影響

為避免路徑空間大小對路徑驗證時間的影響，實驗設置具有68臺終端的線型拓撲、37臺終端的環型拓撲和4臺終端的網狀拓撲，其路徑空間中都包含67條路徑。實驗結果如圖10所示。

圖9 流規則規模對轉發函數生成時間的影響

Fig.9 Influence of flow rule size on forwarding function generation time圖10 流規則規模對路徑驗證時間的影響

Fig.10 Influence of flow rule size on path verification time

由圖10可看出，總體上來說網狀拓撲的路徑驗證時間最長，其次是環型拓撲，線型拓撲的路徑驗證時間最短。這是因為網狀拓撲中的路徑相對較長，生成路徑函數時需要對更多的轉發函數進行析取操作，為此驗證時間更長。而且由于使用了BDD對布爾函數進行存儲，極大縮短了對路徑的驗證時間。在上述實驗中，路徑驗證時間均不超過20 ms。

4.2.3 與APV算法的性能比較

本節將對RVBBF與APV［15］和DASDA［17］進行性能比較。實驗在如圖11所示的復雜拓撲下進行，通過改變流規則的集合規模，分析其驗證效率，實驗結果如圖12所示。

由圖11可以發現，三種算法的檢測時間都隨著流規則規模的增加而增加，但RVBBF在驗證效率上要優于APV和DASDA，驗證時間分別平均縮短約53.76%和27.74%。這是由于隨著流規則數目的增加，尤其是當流規則集合包含的網段較多時，APV中的原子謂詞數量會顯著增加，DASDA則會導致FeDD過于龐大，使得在對其進行維護和查詢時需要更多的時間。并且在APV中，新謂詞的出現可能會對當前的原子謂詞集合造成影響，導致其需要重新計算原子謂詞集合，增加了驗證的時間消耗。相對于APV，DASDA沒有復雜的原子謂詞計算過程，檢測效率相對較高。而RVBBF則只需計算交換機各端口的轉發函數，再據此對路徑空間中的路徑進行驗證即可。同時由于使用BDD對布爾函數進行表示，大大提高了RVBBF的路徑驗證效率。

5 結束語

針對SDN中由于不同應用的轉發路徑交疊等導致的數據平面配置問題，本文提出了一種基于布爾函數的網絡可達性驗證方法。該方法根據流規則生成轉發函數，結合路徑生成算法產生的路徑空間可實現SDN數據轉發平面的可達性驗證。實驗結果表明，RVBBF能夠有效驗證網絡可達性，并且相比于APV，其驗證效率有明顯提高。

在當今網絡中，轉發平面中的配置錯誤非常普遍，新技術也帶來了新的安全挑戰。在經典的SDN南向接口協議OpenFlow中，定義的動作中存在能夠修改數據包IP地址的SET動作，該動作可以對數據包的包頭信息進行修改，使得網絡管理員方便、靈活地實現數據牽引、路由重定向等功能。但如果對SET動作使用不當，則會造成防火墻失效，引發嚴重的網絡安全事故［20］。因此下一步將就如何快速高效地檢測由SET動作導致的轉發平面威脅展開研究，進一步提高網絡安全。

參考文獻：

［1］楊澤衛，李呈.重構網絡：SDN架構與實現［M］.北京：電子工業出版社，2017：1-16.（Yang Zewei，Li Cheng.Refactoring networks：SDN architecture and implementation［M］.Beijing：Publishing House of Electronics Industry，2017：1-16.）

［2］Greenberg A，Hjalmtysson G，Maltz D A，et al.A clean slate 4D approach to network control and management［J］.ACM SIGCOMM Computer Communication Review，2005，35（5）：41-54.

［3］Maity I，Mondal A，Misra S，et al.Tensor-based rule-space management system in SDN［J］.IEEE Systems Journal，2018，13（4）：3921-3928.

［4］Barakabitze A A，Ahmad A，Mijumbi R，et al.5G network slicing using SDN and NFV：a survey of taxonomy，architectures and future challenges［J］.Computer Networks，2020，167：106984.

［5］劉藝，雷程，張紅旗，等.基于MapReduce的OpenFlow網絡屬性驗證技術［J］.計算機研究與發展，2016，53（11）：2500-2511.（Liu Yi，Lei Cheng，Zhang Hongqi，et al.MapReduce-based network pro-perty verification technique for OpenFlow network［J］.Journal of Computer Research and Development，2016，53（11）：2500-2511.）

［6］王軍.SDN下的策略沖突檢測研究［D］.成都：電子科技大學，2020.（Wang Jun.Research on strategy conflict detection under SDN［D］.Chengdu：University of Electronic Science and Technology of China，2020.）

［7］Benton K，Camp L J，Small C.OpenFlow vulnerability assessment［C］//Proc of the 2nd ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking.New York：ACM Press，2013：151-152.

［8］董仕.軟件定義網絡安全問題研究綜述［J］.計算機科學，2021，48（3）：295-306.（Dong Shi.Survey on software defined networks security［J］.Computer Science，2021，48（3）：295-306.）

［9］郭中孚，張興明，趙博，等.軟件定義網絡數據平面安全綜述［J］.網絡與信息安全學報，2018，4（11）：1-12.（Guo Zhongfu，Zhang Xingming，Zhao Bo，et al.Survey of software-defined networking data plane security［J］.Chinese Journal of Network and Information Security，2018，4（11）：1-12.）

［10］陳浩宇，鄒德清，金海.面向SDN/NFV環境的網絡功能策略驗證［J］.網絡與信息安全學報，2021，7（3）：59-71.（Chen Haoyu，Zou Deqing，Jin Hai.Verification on policies for network functions in SDN/NFV-based environment［J］.Chinese Journal of Network and Information Security，2021，7（3）：59-71.）

［11］Kazemian P，Chang M，Zeng H，et al.Real time network policy checking using header space analysis［C］//Proc of the 10th USENIX Symposium on Networked Systems Design and Implementation.New York：ACM Press，2013：99-111.

［12］Kazemian P，Varghese G，McKeown N.Header space analysis：static checking for networks［C］//Proc of the 9th USENIX Symposium on Networked Systems Design and Implementation.New York：ACM Press，2012：113-126.

［13］Fang Yang，Lu Yiqin.Real-time verification of network properties based on header space［J］.IEEE Access，2020，8：36789-36806.

［14］郝巍，伊鵬，江逸茗.一種快速的SDN規則沖突檢測機制［J］.計算機工程，2019，45（2）：139-143.（Hao Wei，Yi Peng，Jiang Yi-ming.A fast SDN rule conflict detection mechanism［J］.Computer Engineering，2019，45（2）：139-143.）

［15］Yang Hongkun，Lam S S.Real-time verification of network properties using atomic predicates［J］.IEEE/ACM Trans on Networking，2015，24（2）：887-900.

［16］王首一，李琦，張云.輕量級的軟件定義網絡數據包轉發驗證［J］.計算機學報，2019，42（1）：176-189.（Wang Shouyi，Li Qi，Zhang Yun.LPV：lightweight packet forwarding verification in SDN［J］.Chinese Journal of Computers，2019，42（1）：176-189.）

［17］Saied W，Souayeh N B Y B，Saadaoui A，et al.Deep and automated SDN data plane analysis［C］//Proc of International Conference on Software，Telecommunications and Computer Networks.Piscataway，NJ：IEEE Press，2019：1-6.

［18］Burdonov I，Kossachev A，Yevtushenko N，et al.Preventive model-based verification and repairing for SDN requests［EB/OL］.（2020-09-21）.http：//doi.org/10.48550/arxiv.1906.03101.

［19］Bryant R E.Graph-based algorithms for boolean function manipulation［J］.IEEE Trans on Computers，1986，100（8）：677-691.

［20］Saadaoui A，Souayeh N B Y B，Bouhoula A.Automated and optimized formal approach to verify SDN access-control misconfigurations［C］//Proc of International Conference on Testbeds and Research Infrastructures.Cham：Springer，2018：96-112.