前 言

如今網絡變得越來越復雜，在運營商對網絡進行配置時，一些不經意間違規配置可能會釀成大錯，因此需要最大程度上保證網絡的配置正確，但人工檢查又太過繁瑣，所以一種新的研究領域——網絡驗證進入了研究者的視野。網絡驗證指使用數學中的形式化方法對網絡配置進行檢查。網絡驗證可以分為數據平面驗證和控制平面驗證，如圖1[1]所示，數據平面是指網絡設備中指定數據包的轉發行為的功能，比如轉發表、流表;控制平面是指結合網絡拓撲、環境信息等生成數據平面的功能，如網絡設備的配置文件。本文主要對目前數據平面驗證工具進行介紹，主要參考了Li[1]等在2019年發表的綜述。

圖1 網絡層次結構和常見錯誤

ConfigChecker

早在2009年由Al-Shaer[2]首先提出ConfigChecker數據平面驗證工具，ConfigChecker是基于模型檢查的，是形式化驗證中十分常見且重要的驗證方法。ConfigChecker使用狀態機建模網絡，狀態機的狀態是由數據包的頭部信息和位置確定的，將由轉發表等數據平面信息建模為狀態轉移關系，不同設備的行為都可以用一組規則來表示，每一個規則都有一個條件和一個動作，條件可以用狀態中的參數來表示一個布爾公式，如果設備上的報文滿足該公式，則觸發相應動作，此過程使用了BDD(二元決策圖)對訪問控制策略編碼，然后使用CTL(計算樹邏輯)表示網絡驗證屬性，如可達性檢查、環路檢測以及發現安全性問題，最后檢查所有狀態是否滿足各屬性。雖然模型檢查存在狀態爆炸的問題，以模型檢查為基礎的驗證工具很難應用在大型網絡上，但是ConfigChecker的提出證明了使用形式化方法驗證網絡的可行性，通過對該篇文章的閱讀我也對模型檢測有了更好的認識。

Mai[3]等在2011年提出了首次在真實網絡中進行網絡驗證的數據平面驗證工具Anteater，核心思想是將網絡驗證問題轉化為SAT問題，然后通過SAT求解器進行求解。Anteater驗證的主要流程較簡單：通過分析網絡中的轉發表獲得數據平面信息，將網絡建模成有向圖，圖中的節點是網絡中各設備可能到達的目的地，圖中的邊是允許在兩節點通過的數據包需要滿足的條件(通過策略函數來表示，也就是多個布爾公式);再將所需驗證的屬性使用一些聲明式語言(如Ruby)來表示，并轉換成SAT公式(該過程是需要通過各邊上策略函數的組合來得到一個SAT公式)，最后通過SAT求解器計算驗證屬性所轉化的SAT公式是否可滿足(參考了可達性驗證算法思想，計算節點之間各路徑允許通過的數據包集合)。我認為該文章中對系統建模的方法是比較容易理解的，基于有向圖，節點為地點，邊為條件，在節點之間流動的數據包用一種稱為符號包(symbolic packet)的變量表示(其中包含了數據包的IP地址、MAC地址、端口號等信息)。本文的網絡屬性驗證方面基本都是圍繞著可達性驗證算法展開的，可達性算法思想是若判定s、t兩點的可達性就是判定是否存在symbolic packet滿足從s到t的路徑上所有邊上的約束條件，將這些條件合并成一個SAT公式，然后求解。轉發循環驗證是為每一個頂點v加一個虛擬節點v’，再分別驗證v-v’的可達性。丟包驗證是網絡中添加一個匯聚節點d，假設它可以到達任意目的地，然后分別測試個節點v的v-d可達性。一致性驗證是分別驗證這兩個節點與其它節點的可達性、丟包情況，然后求異或(即看結果是否一樣)。雖然Anteater不能進行實時驗證，擴展性、時間效率都不夠好，但是我認為這種將可達性驗證算法用于對數據包的計算上是十分有意義的，之后的工具中也有應用該思想的。

HSA

Kazemian[4]等在2012年提出了HSA(Header Space Analysis 頭空間分析技術)，基于符號執行技術，與之前的Anteater完全不同，HSA更加抽象，不易理解。HSA的系統建模過程較復雜：有七個需要注意的部分。(1)文章提出了頭空間(Header Space)H的概念，將報頭看作是一組由0、1組成的序列，在{0,1}L(L表示序列長度)頭空間中，一個報頭是一個點，一個流是一片區域。(2)將各個網絡設備的各輸入端口所可能輸入的所有報頭組成為網絡空間N(即頭空間H×{所有設備入端口})。(3)將各網絡設備根據其功能定義出不同網絡轉移函數，函數有兩個參數，分別是報頭header和端口port，函數定義了頭空間中不同區域通過某一網絡設備后的轉換情況。(4)定義拓撲轉移函數，函數參數與網絡轉移函數的參數相同(header，port)，該函數用于描述網絡中各鏈路，一般一組(header，port)經歷過網絡傳遞函數轉換后，其鏈路狀況也會改變，需要拓撲轉移函數來計算新的拓撲狀況。(5)定義了Slice三元組(網絡空間N的一個子集，讀寫操作，對于該Slice的所有轉移函數)，我認為Slice的主要功能就是描述數據包集合，與Anteater中符號包(symbolic packet)功能類似。(6)定義了頭空間的代數，因為每個數據包(或流)在頭空間是一組0、1組合，定義了交、并、補、差、T(轉移函數能夠輸出的(header，port)集合)和T-1等操作，用于對頭空間中的子空間進行操作，得到最后的空間(即剩余的數據包)。(7)網絡設備建模，將不同網絡設備根據其功能，將多個傳遞函數組合，得到一個總的函數，比如路由器處理數據包的過程為重寫源、目的地址(T1)、減少TTL(T2)、更新校驗和(T3)、轉發到出端口(T4)，則該路由器可通過符合以上四個轉移函數得到Trouter=T1(T2(T3(T4(header，port))))。

網絡驗證是將網絡屬性建模成頭空間的相關斷言，驗證過程是先根據斷言構造特定的符號數據包幾何，輸入到網絡中的轉移函數進行分析，然后通過分析轉移函數對符號數據包集合的處理過程確定斷言的滿足性以完成屬性驗證。由于使用了基于函數的分析方法，能夠找到違反驗證屬性的全部反例。可達性分析如圖2[4]所示，是考慮離開源地址的所有報頭空間，在到達目的地址的過程中，跟蹤這個空間(中間會經歷很多傳遞函數，空間會減少)，到達目的地址時，若頭空間還有剩余，則可達，再根據之前提到的T-1(轉移函數的逆)函數找到源地址發送的可以到達目的地址的報頭集合。循環檢測是通過給每個端口輸入一個全是x(通配符)的測試報頭，追蹤數據包，如果數據包返回源端口，則說明有循環。

圖2 計算從a到b的可達性示意圖

我認為HAS相較于Anteater更難理解一些，但是提出的頭空間是十分巧妙的，以數據包為點，以網絡設備為點與點之間的線(與Anteater剛好相反：以設備地址為點，以數據包為線)，這種抽象在一定程度上能讓復雜的網絡空間變得更簡單。

于2013年被提出的VeriFlow[5]是首個的對數據平面進行實時驗證的工具。VeriFlow在某種程度上是在Anteater的基礎上增加了增量計算，實現實時驗證，因為VeriFlow也是基于可達性算法，對數據包進行計算。VeriFlow的大致思想是：實時監控SDN網絡中所有的網絡更新時事件，VeriFlow處于控制器與網絡設備的夾層中;然后VeriFlow旨在受網絡更新影響的小范圍內進行網絡驗證，驗證過程使用自定義算法。VeriFlow實現只在小范圍內進行驗證的方法是：通過分析SDN控制器下發的新規則，基于新規則和與新規則有重疊部分的老規則，將網絡劃分為一組等價類，每次網絡更新只會影響一小部分等價類，然后為每個被修改的等價類構建各自的轉發圖，轉發圖用于表示網絡的轉發行為，最后通過遍歷轉發圖來檢查網絡屬性。由于VeriFlow只進行小范圍驗證，所以驗證速度很快，從而基于等價類實現了實時驗證的目的。其中等價類的劃分是將網絡中具有相同轉發行為的數據包集合劃為一個等價類，為了加速等價類的劃分和找到受更新影響的等價類，文中使用多維前綴樹(trie)這種適用于包分類算法的數據結構。trie中的每一層對應于轉發規則中的特定位，trie的每個節點存在1，0，x三個分支，一個trie可以看作是幾個trie或幾個維度的組合，每個維度對應數據包頭中的一個字段，從trie的根到葉子節點的路徑表示與該規則匹配的包集，每個葉子節點存儲了匹配數據包集的規則和它們所處的位置，由此完成了等價類的劃分，如圖3[5]所示。等價類劃分后是為每個等價類都生成一個轉發圖，轉發圖是用于表示等價類中的數據包是如何被轉發的，圖中節點表示特定網絡設備的等價類，有向邊表示對于該(等價類，設備)對的轉發規則，若圖中兩節點X，Y相連表示根據節點X所在設備的轉發表，該等價類中的數據包可以發送到Y所在的設備中。構建轉發圖的過程為了找到與等價類匹配的包和規則，需要再次遍歷trie。網絡屬性的檢查是建立在轉發圖上的，將檢查的屬性設定為一個驗證函數，將轉發圖作為輸入，執行函數，得到結果。VeriFlow開發了一個可編程接口，用于編寫和插入新的屬性檢查函數。在VeriFlow中可達性驗證、循環驗證、一致性驗證等都是通過編寫特定函數完成的。

圖3 VeriFlow計算等價類的過程

數據平面實時驗證工具NetPlumber[6]同樣出現于2013年，主要是應用在SDN網絡中。SDN網絡中主要是通過控制器向各網絡設備發送各種規則，而NetPlumber就是處于控制器和設備之間，對這些規則進行檢查。它首先是繼承了HSA的思想，借助了頭空間的思想(header space)，將一個報文看作頭空間的一個點，將一組報文看作一片區域，將網絡設備定義為不同轉移函數，完成數據包在頭空間的流動。該文中更清楚地介紹了轉移函數：每個轉移函數由一些列規則構成，一個規則包括一組輸入端口、一個通配符表達式(用于過濾數據包)和一組對符合表達式的數據包的操作，操作包括轉發、刪除、重寫、封裝等。NetPlumber對于HSA的改進主要體現在實現了實時增量檢查和提出了一種新的屬性檢查方式。所以HSA中可以檢查的屬性NetPlumber都可以完成。

NetPlumber

NetPlumber的核心是首先通過各轉發表構建了一種依賴圖，叫做plumbing graph，如圖4[6]所示，然后再通過分析SDN控制器下發的規則對該圖進行調整，其中圖的節點對應規則，圖的有向邊稱為pipes，對應了規則之間的依賴關系，代表了匹配數據包的可能路徑。定義每個pipe邊包含一個pipe fliter，用于過濾數據包。文中對規則(節點的定義也是非常巧妙的，定義為一個二元組，match字段用于標識出可以受該規則處理的數據包，action字段表示對這些數據包的操作。在plumbing graph中若兩規則節點相連，一是可能這兩個規則所屬的網絡設備之間存在物理鏈路，二是可能被第一個規則節點處理后的數據包能夠被第二個規則節點識別并再進行處理。對于規則的增加、刪除和鏈路的增加、刪除文中都介紹了如何對plumbing graph進行更新，該內容也是NetPlumber能夠進行實時驗證的基礎，每一次網絡發生變化時，不會重新建立plumbing graph，而只是小范圍的更新，計算速度較快，以實現實時更新。文中提到的還有助于實時網絡更新的一個思想是分布式NetPlumber，將plumbing graph分成多個集群，一個集群內的節點交互更多，集群間的共用節點復制出一個劃入另一個集群，然后各集群之間可以同時計算，速度更快。

圖4 由4個交換機組成的簡單網絡的plumbing graph

NetPlumber中的所有屬性驗證也是基于對plumbing graph進行檢測的，通過向圖中指定位置增加probe nodes收集數據包，進行驗證，定義每個probe node、具有一個過濾表達式和一個測試表達式，過濾表達式用于過濾數據包，測試表達式用于驗證屬性。比如計算端口s到端口d的可達性，向s注入一個全是x通配符的一組數據包，使其沿著所有的有向邊傳播，在每一個規則節點上，flow由match過濾，由action轉換后得到一個新的flow，繼續傳到下一個節點，如果在d處存在來自s的數據包，則說明s和d可達。我認為NetPlumber的整體構思可以分為兩部分，一是將整個網絡都表示在頭空間中，二是由頭空間得到plumbing graph，通過對plumbing graph中節點的驗證以完成屬性驗證。借助plumbing graph這個巧妙的設計首先實現了實時驗證數據平面，還可以檢測一切由網絡狀態更新相關的網絡屬性驗證，同時可以對graph進行聚類的劃分實現并行計算。

小 結

目前已經完成了幾個比較常見的數據平面驗證工具的介紹，包括ConfigChecker、Anteater、HSA、VeriFlow、NetPlumber。數據平面驗證基本都是基于Xie[7]提出的可達性算法，通過對一條路徑中的數據包進行計算，結果不為空則表明可達。不同工具也有各自的特點和有價值的思想，下面進行簡要的總結：(1)ConfigChecker基于符號模型檢測技術，根據數據包頭信息和所處位置建模為狀態，使用BDD表達的布爾公式表示狀態轉移關系，使用CTL表達驗證屬性，通過遍歷所有的狀態來驗證屬性。(2)Anteater基于SAT問題，根據數據平面信息將網絡構建成一個有向圖，節點表示位置，有向邊表示數據包通過的條件(策略)，將網絡用布爾公式編碼。用一組表示數據包頭字段的變量的符號包示數據包，再將驗證屬性表示成一個個SAT實例，通過SAT求解器進行驗證。(3)HSA基于符號執行技術，提出頭空間的概念，一個數據包為頭空間中的一個點，對頭空間中區域的過濾就是對數據包的過濾。將不同設備的功能定義為轉移函數，用于對頭空間的區域進行操作。屬性驗證過程是將不同屬性寫成頭空間內的不同斷言，通過判定斷言的真假來驗證屬性。(4)VeriFlow基于等價類思想實現了實時驗證，它通過監控SDN網絡中控制器與網絡設備間的通信，將具有相同轉發行為的數據包劃為一個等價類，再為每一個等價類建立一個轉發圖，節點代表網絡設備，邊代表該設備的轉發規則。屬性檢查是在各個等價類的轉發圖上基于圖算法進行驗證。(5)NetPlumber基于增量計算的思想，在完成HSA中將數據包映射到頭空間后，把網絡建成了一種叫作plumbing graph的依賴圖，節點表示規則，邊表示規則間的依賴關系，通過在plumbing graph中增加探測節點，然后根據探測節點(帶有過濾表達式和測試表達式)完成相應屬性驗證。

數據平面能夠完成網絡當前這一時刻的網絡驗證，并且只能在網絡配置完成后真正運行網絡出現錯誤時才能檢查出來，不能對錯誤進行提前檢查，所以今后網絡驗證的發展方向還是需要集中在控制平面上，但本文數據平面驗證工具也很都起著重要的作用，因為有很大一部分控制平面驗證工具是先通過一些方法根據網絡設備控制平面信息生成數據平面后，再對生成的數據平面進行驗證，這個驗證過程也是需要數據平面驗證工具的。綜上可以看出網絡驗證領域的數據平面驗證出現了很多巧妙的驗證思想和工具，為網絡驗證更好的發展奠定了基礎。

參考文獻

[1]Li Y H, Yin X,Wang Z L, et al. A Survey on Network Verification and Testing With FormalMethods: Approaches and Challenges.IEEE Communications Surveys & Tutorials,2019, 21(1): 940-969.

[2]Al-Shaer E,Marrero W, El-Atawy A, et al. Network configuration in a box: towardsend-to-end verification of network reachability and security. In: 2009 17thIEEE International Conference on Network Protocols, 2009: 123-132.

[3]Mai H, KhurshidA, Agarwal R, et al. Debugging the data plane with anteater. In: Proceedings ofthe ACM SIGCOMM 2011 conference, 2011: 290-301.

[4]Kazemian P,Varghese G, Mckeown N. Header space analysis: Static checking for networks. In:Proceedings of the 9th USENIX conference on Networked Systems Design andImplementation, 2012: 9.

[5]Khurshid A, ZouX, Zhou W, et al. VeriFlow: Verifying Network-Wide Invariants in Real Time. In:10th {USENIX} Symposium on Networked Systems Design and Implementation ({NSDI}13), 2013: 15-27.

[6]Kazemian P,Chang M, Zeng H, et al. Real time network policy checking using header spaceanalysis. In: Proceedings of the 10th USENIX conference on Networked SystemsDesign and Implementation, 2013: 99–112.

[7]Xie G G, JibinZ, Maltz D A, et al. On static reachability analysis of IP networks. In:Proceedings IEEE 24th Annual Joint Conference of the IEEE Computer andCommunications Societies., 2005: 2170-2183 vol. 3.

本文轉載自微信公眾號「中國保密協會科學技術分會」，可以通過以下二維碼關注。轉載本文請聯系中國保密協會科學技術分會公眾號。