前 言

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

圖1 網(wǎng)絡(luò)層次結(jié)構(gòu)和常見(jiàn)錯(cuò)誤

ConfigChecker

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

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

HSA

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

網(wǎng)絡(luò)驗(yàn)證是將網(wǎng)絡(luò)屬性建模成頭空間的相關(guān)斷言，驗(yàn)證過(guò)程是先根據(jù)斷言構(gòu)造特定的符號(hào)數(shù)據(jù)包幾何，輸入到網(wǎng)絡(luò)中的轉(zhuǎn)移函數(shù)進(jìn)行分析，然后通過(guò)分析轉(zhuǎn)移函數(shù)對(duì)符號(hào)數(shù)據(jù)包集合的處理過(guò)程確定斷言的滿足性以完成屬性驗(yàn)證。由于使用了基于函數(shù)的分析方法，能夠找到違反驗(yàn)證屬性的全部反例?？蛇_(dá)性分析如圖2[4]所示，是考慮離開(kāi)源地址的所有報(bào)頭空間，在到達(dá)目的地址的過(guò)程中，跟蹤這個(gè)空間(中間會(huì)經(jīng)歷很多傳遞函數(shù)，空間會(huì)減少)，到達(dá)目的地址時(shí)，若頭空間還有剩余，則可達(dá)，再根據(jù)之前提到的T-1(轉(zhuǎn)移函數(shù)的逆)函數(shù)找到源地址發(fā)送的可以到達(dá)目的地址的報(bào)頭集合。循環(huán)檢測(cè)是通過(guò)給每個(gè)端口輸入一個(gè)全是x(通配符)的測(cè)試報(bào)頭，追蹤數(shù)據(jù)包，如果數(shù)據(jù)包返回源端口，則說(shuō)明有循環(huán)。

圖2 計(jì)算從a到b的可達(dá)性示意圖

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

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

圖3 VeriFlow計(jì)算等價(jià)類的過(guò)程

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

NetPlumber

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

圖4 由4個(gè)交換機(jī)組成的簡(jiǎn)單網(wǎng)絡(luò)的plumbing graph

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

小 結(jié)

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

數(shù)據(jù)平面能夠完成網(wǎng)絡(luò)當(dāng)前這一時(shí)刻的網(wǎng)絡(luò)驗(yàn)證，并且只能在網(wǎng)絡(luò)配置完成后真正運(yùn)行網(wǎng)絡(luò)出現(xiàn)錯(cuò)誤時(shí)才能檢查出來(lái)，不能對(duì)錯(cuò)誤進(jìn)行提前檢查，所以今后網(wǎng)絡(luò)驗(yàn)證的發(fā)展方向還是需要集中在控制平面上，但本文數(shù)據(jù)平面驗(yàn)證工具也很都起著重要的作用，因?yàn)橛泻艽笠徊糠挚刂破矫骝?yàn)證工具是先通過(guò)一些方法根據(jù)網(wǎng)絡(luò)設(shè)備控制平面信息生成數(shù)據(jù)平面后，再對(duì)生成的數(shù)據(jù)平面進(jìn)行驗(yàn)證，這個(gè)驗(yàn)證過(guò)程也是需要數(shù)據(jù)平面驗(yàn)證工具的。綜上可以看出網(wǎng)絡(luò)驗(yàn)證領(lǐng)域的數(shù)據(jù)平面驗(yàn)證出現(xiàn)了很多巧妙的驗(yàn)證思想和工具，為網(wǎng)絡(luò)驗(yàn)證更好的發(fā)展奠定了基礎(chǔ)。

參考文獻(xiàn)

[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.

本文轉(zhuǎn)載自微信公眾號(hào)「中國(guó)保密協(xié)會(huì)科學(xué)技術(shù)分會(huì)」，可以通過(guò)以下二維碼關(guān)注。轉(zhuǎn)載本文請(qǐng)聯(lián)系中國(guó)保密協(xié)會(huì)科學(xué)技術(shù)分會(huì)公眾號(hào)。