前 言

如今網(wǎng)絡(luò)變得越來越復(fù)雜，在運(yùn)營商對網(wǎng)絡(luò)進(jìn)行配置時，一些不經(jīng)意間違規(guī)配置可能會釀成大錯，因此需要最大程度上保證網(wǎng)絡(luò)的配置正確，但人工檢查又太過繁瑣，所以一種新的研究領(lǐng)域——網(wǎng)絡(luò)驗(yàn)證進(jìn)入了研究者的視野。網(wǎng)絡(luò)驗(yàn)證指使用數(shù)學(xué)中的形式化方法對網(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ù)洹h(huán)境信息等生成數(shù)據(jù)平面的功能，如網(wǎng)絡(luò)設(shè)備的配置文件。本文主要對目前數(shù)據(jù)平面驗(yàn)證工具進(jìn)行介紹，主要參考了Li[1]等在2019年發(fā)表的綜述。

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

ConfigChecker

早在2009年由Al-Shaer[2]首先提出ConfigChecker數(shù)據(jù)平面驗(yàn)證工具，ConfigChecker是基于模型檢查的，是形式化驗(yà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ī)則來表示，每一個規(guī)則都有一個條件和一個動作，條件可以用狀態(tài)中的參數(shù)來表示一個布爾公式，如果設(shè)備上的報文滿足該公式，則觸發(fā)相應(yīng)動作，此過程使用了BDD(二元決策圖)對訪問控制策略編碼，然后使用CTL(計算樹邏輯)表示網(wǎng)絡(luò)驗(yàn)證屬性，如可達(dá)性檢查、環(huán)路檢測以及發(fā)現(xiàn)安全性問題，最后檢查所有狀態(tài)是否滿足各屬性。雖然模型檢查存在狀態(tài)爆炸的問題，以模型檢查為基礎(chǔ)的驗(yàn)證工具很難應(yīng)用在大型網(wǎng)絡(luò)上，但是ConfigChecker的提出證明了使用形式化方法驗(yàn)證網(wǎng)絡(luò)的可行性，通過對該篇文章的閱讀我也對模型檢測有了更好的認(rèn)識。

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

HSA

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

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

圖2 計算從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ò)空間變得更簡單。

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

圖3 VeriFlow計算等價類的過程

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

NetPlumber

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

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

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

小 結(jié)

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

數(shù)據(jù)平面能夠完成網(wǎng)絡(luò)當(dāng)前這一時刻的網(wǎng)絡(luò)驗(yàn)證，并且只能在網(wǎng)絡(luò)配置完成后真正運(yùn)行網(wǎng)絡(luò)出現(xiàn)錯誤時才能檢查出來，不能對錯誤進(jìn)行提前檢查，所以今后網(wǎng)絡(luò)驗(yàn)證的發(fā)展方向還是需要集中在控制平面上，但本文數(shù)據(jù)平面驗(yàn)證工具也很都起著重要的作用，因?yàn)橛泻艽笠徊糠挚刂破矫骝?yàn)證工具是先通過一些方法根據(jù)網(wǎng)絡(luò)設(shè)備控制平面信息生成數(shù)據(jù)平面后，再對生成的數(shù)據(jù)平面進(jìn)行驗(yàn)證，這個驗(yàn)證過程也是需要數(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)載自微信公眾號「中國保密協(xié)會科學(xué)技術(shù)分會」，可以通過以下二維碼關(guān)注。轉(zhuǎn)載本文請聯(lián)系中國保密協(xié)會科學(xué)技術(shù)分會公眾號。