引 言

隨著網(wǎng)絡(luò)變得復(fù)雜和龐大，網(wǎng)絡(luò)管理也變得更加困難，網(wǎng)絡(luò)升級(jí)或改造過程中的細(xì)小失誤可能會(huì)對(duì)網(wǎng)絡(luò)的正常運(yùn)行造成嚴(yán)重影響。根據(jù)Veriflow公司于2016年對(duì)315名IT專業(yè)人員進(jìn)行的調(diào)查得出的結(jié)果，59%的受訪者表示網(wǎng)絡(luò)復(fù)雜性的增加導(dǎo)致了更頻繁的中斷，74%的人表示網(wǎng)絡(luò)變化每年或多次對(duì)企業(yè)產(chǎn)生重大影響[1]。2019年7月3日，Cloudflare公司在新的Web應(yīng)用層防火墻中部署了一個(gè)配置錯(cuò)誤的規(guī)則，導(dǎo)致了全球大面積宕機(jī)[2]。配置錯(cuò)誤、硬軟件實(shí)現(xiàn)錯(cuò)誤、網(wǎng)絡(luò)攻擊或協(xié)議交互的意外錯(cuò)誤都會(huì)影響網(wǎng)絡(luò)的可用性和安全性。那么，關(guān)鍵問題在于我們?nèi)绾尾拍艽_保業(yè)務(wù)的意圖在復(fù)雜的網(wǎng)絡(luò)環(huán)境中正確的實(shí)施運(yùn)行?

[[332104]]

過去幾年，已經(jīng)出現(xiàn)了一個(gè)新的研究領(lǐng)域，即網(wǎng)絡(luò)驗(yàn)證，旨在嚴(yán)格確保網(wǎng)絡(luò)按期望的業(yè)務(wù)意圖運(yùn)行。網(wǎng)絡(luò)驗(yàn)證的技術(shù)靈感來源于形式化方法，一種廣義上基于數(shù)學(xué)方法，通過對(duì)復(fù)雜系統(tǒng)建立嚴(yán)格的數(shù)學(xué)模型，驗(yàn)證系統(tǒng)的性能與行為正確性的方法，主要有模型檢測、定理證明、符號(hào)執(zhí)行及SMT/SAT(可滿足性理論)求解器四種技術(shù)[3]。形式化驗(yàn)證已經(jīng)在硬軟件領(lǐng)域得到的成功的應(yīng)用。例如，NASA(美國航空航天局)成功使用形式化驗(yàn)證技術(shù)在火星探測器飛行軟件中發(fā)現(xiàn)了并發(fā)錯(cuò)誤[4]。如果我們可以驗(yàn)證硬軟件，為什么不驗(yàn)證網(wǎng)絡(luò)?最近，網(wǎng)絡(luò)驗(yàn)證在驗(yàn)證和程序語言社區(qū)變得逐漸流行起來，學(xué)術(shù)界和產(chǎn)業(yè)界都開展了網(wǎng)絡(luò)驗(yàn)證的相關(guān)研究。在學(xué)術(shù)界，主要有斯坦福大學(xué)、伊利諾伊大學(xué)香檳分校、加州大學(xué)洛杉磯分校、卡內(nèi)基梅隆大學(xué)以及清華大學(xué)等高校。在工業(yè)界，主要有微軟研究院和AT&T實(shí)驗(yàn)室。目前，該領(lǐng)域已經(jīng)出現(xiàn)了一些初創(chuàng)公司，如Forward Networks、Veriflow、Intentionet。

本文將首先介紹一些相關(guān)背景知識(shí)，然后分別介紹網(wǎng)絡(luò)驗(yàn)證中的控制平面驗(yàn)證和數(shù)據(jù)平面驗(yàn)證兩個(gè)研究方向，最后進(jìn)行總結(jié)。

背景知識(shí)

網(wǎng)絡(luò)從路由轉(zhuǎn)發(fā)的角度可以被分為三層，即策略、控制平面和數(shù)據(jù)平面，如圖1所示[3]。策略是控制平面和數(shù)據(jù)平面的參考，體現(xiàn)了網(wǎng)絡(luò)管理人員的意圖，如主機(jī)A是否允許和主機(jī)B通信?？刂破矫媸怯糜趯?shí)現(xiàn)策略的，在傳統(tǒng)網(wǎng)絡(luò)中是指分散于各處的網(wǎng)絡(luò)設(shè)備中的配置文件，在SDN(軟件定義網(wǎng)絡(luò))中是指各種應(yīng)用。數(shù)據(jù)平面是網(wǎng)絡(luò)中根據(jù)控制平面生成的轉(zhuǎn)發(fā)信息與拓?fù)浣Y(jié)構(gòu)，其中轉(zhuǎn)發(fā)信息在傳統(tǒng)網(wǎng)絡(luò)中是指轉(zhuǎn)發(fā)表，在SDN中是指流表。根據(jù)控制平面和數(shù)據(jù)平面兩個(gè)層次，網(wǎng)絡(luò)驗(yàn)證有控制平面驗(yàn)證和數(shù)據(jù)平面驗(yàn)證兩個(gè)研究方向，其通過分析對(duì)應(yīng)平面信息，然后驗(yàn)證網(wǎng)絡(luò)策略的不變式完成檢查。其中，不變式是一種屬性，在網(wǎng)絡(luò)中特指路由轉(zhuǎn)發(fā)行為的正確屬性，如無轉(zhuǎn)發(fā)循環(huán)不變式，斷言了數(shù)據(jù)包在網(wǎng)絡(luò)中不會(huì)出現(xiàn)轉(zhuǎn)發(fā)循環(huán)。在對(duì)一個(gè)特定網(wǎng)絡(luò)如企業(yè)網(wǎng)、校園網(wǎng)進(jìn)行驗(yàn)證時(shí)，除了需要考慮該網(wǎng)絡(luò)的控制平面或數(shù)據(jù)平面信息，還需要考慮網(wǎng)絡(luò)環(huán)境的因素，如網(wǎng)絡(luò)外部發(fā)送給網(wǎng)絡(luò)的路由通告。

圖1 網(wǎng)絡(luò)層次劃分情況

控制平面驗(yàn)證

控制平面驗(yàn)證通過輸入控制平面信息，驗(yàn)證網(wǎng)絡(luò)策略的不變式以確?？刂破矫媾c策略要求的一致。其優(yōu)點(diǎn)是可以在配置部署到網(wǎng)絡(luò)之前完成驗(yàn)證，能夠方便的定位到錯(cuò)誤的配置位置;缺點(diǎn)是需要分析配置文件與網(wǎng)絡(luò)行為之間的復(fù)雜關(guān)系，以及考慮形式各異的配置語言。

目前，傳統(tǒng)網(wǎng)絡(luò)目前仍占據(jù)主導(dǎo)地位，其控制平面的配置文件分散在各處的網(wǎng)絡(luò)設(shè)備中，驗(yàn)證面臨狀態(tài)爆炸問題。相關(guān)研究方面，F(xiàn)eamster等人于2005年提出了rcc工具[5]，是第一個(gè)能在真實(shí)網(wǎng)絡(luò)中檢測BGP(邊界網(wǎng)關(guān)協(xié)議)故障的靜態(tài)分析工具，但其檢查的范圍僅限于BGP協(xié)議。rcc采用的是靜態(tài)分析的方法，其將控制平面信息標(biāo)準(zhǔn)化成SQL數(shù)據(jù)，然后驗(yàn)證根據(jù)策略轉(zhuǎn)換成的SQL上的約束條件判斷BGP配置的正確性。為了提高驗(yàn)證范圍，不再局限于特定的協(xié)議，F(xiàn)ogel等人提出了Batfish工具[6]。

Batfish并沒有選擇在控制平面上進(jìn)行建模，而是選擇通過控制平面生成數(shù)據(jù)平面，然后調(diào)用數(shù)據(jù)平面驗(yàn)證工具進(jìn)行驗(yàn)證。這種方式結(jié)合了控制平面驗(yàn)證和數(shù)據(jù)平面驗(yàn)證的優(yōu)點(diǎn)，既能提前檢測錯(cuò)誤也不需考慮協(xié)議的復(fù)雜交互。但是，Batfish面臨著一個(gè)難題，即如何根據(jù)配置和環(huán)境生成一個(gè)可靠的數(shù)據(jù)平面，其通過使用DataLog(一種數(shù)據(jù)查詢語言)的一種變式LogiQL建立了一個(gè)陳述式模型以解決此挑戰(zhàn)。由于Batfish需要對(duì)整個(gè)數(shù)據(jù)平面進(jìn)行模擬，速度很慢。Gemberjacobson等人發(fā)現(xiàn)，生成詳細(xì)的數(shù)據(jù)平面是不必要的，提出了ARC，可以直接在控制平面進(jìn)行快速分析[7]。

ARC使用加權(quán)有向圖對(duì)控制平面建模，使用圖算法進(jìn)行分析完成驗(yàn)證。對(duì)于特定的屬性不變式，可以比Batfish快出了三個(gè)數(shù)量級(jí)。但是，ARC只對(duì)一些特定的協(xié)議組合進(jìn)行了分析，如OSPF，RIP，eBGP。為提高驗(yàn)證的協(xié)議范圍，F(xiàn)ayaz等人提出了ERA工具[8]。

ERA使用二元決策圖(BDD)對(duì)控制平面建模，通過探索BDD模型完成驗(yàn)證。相比ARC可以驗(yàn)證更多協(xié)議，相比Batfish驗(yàn)證速度快了2.5到17倍，且可以擴(kuò)展到大型網(wǎng)絡(luò)中。Beckett等人指出，控制平面驗(yàn)證的主要難點(diǎn)在于構(gòu)建一個(gè)具有高度的網(wǎng)絡(luò)設(shè)計(jì)覆蓋范圍與高度數(shù)據(jù)平面覆蓋范圍的驗(yàn)證工具，同時(shí)保持足夠高的可擴(kuò)展性[9]。

其中，網(wǎng)絡(luò)設(shè)計(jì)覆蓋范圍是指工具能夠支持網(wǎng)絡(luò)的拓?fù)漕愋汀⒙酚蓞f(xié)議和其他一些特點(diǎn)的范圍;數(shù)據(jù)平面覆蓋范圍是指工具能夠支持的數(shù)據(jù)平面的范圍。為解決該挑戰(zhàn)，Beckett等人提出了Minesweeper工具。Minesweeper使用SMT公式對(duì)控制平面建模，將公式放入SMT Solver中完成驗(yàn)證。相比之前的控制平面驗(yàn)證工具，可以驗(yàn)證更多的協(xié)議，覆蓋更大的數(shù)據(jù)平面，且可以擴(kuò)展到大型網(wǎng)絡(luò)。值得說明的是，ARC、ERA和Minesweeper都使用了Batfish的配置解析器將不同廠商的配置轉(zhuǎn)換為無關(guān)廠商的統(tǒng)一格式。表1從網(wǎng)絡(luò)設(shè)計(jì)覆蓋范圍、擴(kuò)展性、主要基于的技術(shù)3個(gè)方面對(duì)上述工具進(jìn)行了總結(jié)。其中，擴(kuò)展性是指工具擴(kuò)展到大型網(wǎng)絡(luò)的能力。

表1 傳統(tǒng)網(wǎng)絡(luò)控制平面驗(yàn)證工具總結(jié)

在SDN中，網(wǎng)絡(luò)行為是集中由控制器決定的，這使得驗(yàn)證網(wǎng)絡(luò)變得簡單。目前SDN控制平面驗(yàn)證主要集中在兩方面，一是對(duì)SDN程序的驗(yàn)證，二是開發(fā)驗(yàn)證控制器[3]。SDN使用應(yīng)用程序制定策略管理網(wǎng)絡(luò)設(shè)備，如路由或訪問控制。如普通的軟件程序一樣，SDN程序會(huì)出現(xiàn)設(shè)計(jì)或?qū)崿F(xiàn)錯(cuò)誤，如果盲目的部署在網(wǎng)絡(luò)中，很容易引起故障的發(fā)生。驗(yàn)證控制器用于檢查控制器是否按照策略正確安裝規(guī)則，因?yàn)槠涮囟ǖ木幊陶Z言支持不變式驗(yàn)證，可以在編譯時(shí)與規(guī)則安裝到交換機(jī)之前進(jìn)行驗(yàn)證，防止錯(cuò)誤的規(guī)則下發(fā)。目前，SDN程序驗(yàn)證方向有Verificare、VeriCon等工具，驗(yàn)證控制器方向有NetCore、NDLog、NetKAT等工具。

數(shù)據(jù)平面驗(yàn)證

數(shù)據(jù)平面驗(yàn)證通過輸入數(shù)據(jù)平面信息，驗(yàn)證網(wǎng)絡(luò)策略的不變式以確保數(shù)據(jù)平面與策略要求的一致。其優(yōu)點(diǎn)是數(shù)據(jù)平面直接體現(xiàn)了配置的影響，分析起來更加簡單。但是，其不能在配置部署前完成驗(yàn)證，而且需要重復(fù)采集數(shù)據(jù)以應(yīng)對(duì)網(wǎng)絡(luò)波動(dòng)帶來的數(shù)據(jù)平面變化。此外，數(shù)據(jù)平面驗(yàn)證不能提供錯(cuò)誤配置的出處，需要人員自行關(guān)聯(lián)發(fā)現(xiàn)，由于網(wǎng)絡(luò)行為與配置文件之間的復(fù)雜關(guān)系，這是十分困難的。數(shù)據(jù)平面驗(yàn)證方面，傳統(tǒng)網(wǎng)絡(luò)與SDN網(wǎng)絡(luò)的唯一區(qū)別在于數(shù)據(jù)采集過程，傳統(tǒng)網(wǎng)絡(luò)可以通過SNMP(簡單網(wǎng)絡(luò)管理協(xié)議)，終端或者控制會(huì)話來收集轉(zhuǎn)發(fā)表，而SDN網(wǎng)絡(luò)可以監(jiān)視控制器獲得。

由于控制平面驗(yàn)證不能發(fā)現(xiàn)網(wǎng)絡(luò)設(shè)備將控制平面轉(zhuǎn)換成數(shù)據(jù)平面的實(shí)現(xiàn)錯(cuò)誤，以及存在分析復(fù)雜的問題，Mai等人于2011年提出了第一個(gè)在真實(shí)網(wǎng)絡(luò)中發(fā)現(xiàn)錯(cuò)誤的數(shù)據(jù)平面分析工具Anteater[10]。Anteater首先根據(jù)數(shù)據(jù)平面信息將網(wǎng)絡(luò)建模成為一個(gè)圖，然后將不變式建模為圖上的函數(shù)，最后將函數(shù)轉(zhuǎn)換為SAT公式放入SAT Solver進(jìn)行求解。Anteater通過實(shí)驗(yàn)證明，分析數(shù)據(jù)平面是一種可行方法，相比于控制平面驗(yàn)證速度不一定更快，但實(shí)現(xiàn)方法上相比更容易。

Kazemian等人之后提出了一種數(shù)據(jù)平面驗(yàn)證框架HSA [11]。HSA框架是基于幾何模型的，其將數(shù)據(jù)包建模成幾何空間中的點(diǎn)，用頭空間(Header Space)即最大長度為L的{0,1}字符串表示，網(wǎng)絡(luò)設(shè)備建模成該幾何空間上的轉(zhuǎn)移函數(shù)，通過分析特定數(shù)據(jù)包頭部在幾何空間的變化，進(jìn)行不變式的驗(yàn)證。相比于其他基于形式化驗(yàn)證方法的工具，HSA可以提供所有反例，使分析錯(cuò)誤變得高效。Veriflow和NetPlumber使用等價(jià)類與增量技術(shù)分別改進(jìn)了Anteater和HSA，有足夠的速度和擴(kuò)展性。

Lopes等人認(rèn)為，Veriflow和NetPlumber是定制化的代碼，難以擴(kuò)展到新的數(shù)據(jù)包格式和協(xié)議。而網(wǎng)絡(luò)驗(yàn)證若要發(fā)展成為一個(gè)網(wǎng)絡(luò)CAD行業(yè)，必須要發(fā)展成一個(gè)更標(biāo)準(zhǔn)化、更加可擴(kuò)展的技術(shù)。為解決該挑戰(zhàn)，Lopes等人基于Datalog技術(shù)，提出了NOD工具[12,13]。NOD使用Datalog對(duì)策略和協(xié)議行為編碼，能夠進(jìn)行通用的擴(kuò)展，最后使用基于SMT Solver技術(shù)的Z3 Datalog框架進(jìn)行驗(yàn)證。實(shí)驗(yàn)表明，NOD的Datalog模型計(jì)算可達(dá)數(shù)據(jù)集合比模型檢測和SMT計(jì)算單個(gè)可達(dá)數(shù)據(jù)都快，相比于基于HSA的Hassel工具，雖然速度相比較慢，但更易于通用化。為專注于驗(yàn)證訪問控制策略的正確實(shí)施，Jayaraman等人提出了SecGuru工具，是NOD的早期版本, 已經(jīng)被部署在Azure中以檢查數(shù)以百計(jì)的路由器和防火墻的正確性[14]。

SecGuru使用位向量對(duì)數(shù)據(jù)平面和策略進(jìn)行編碼，然后將這種位向量邏輯放入Z3 SMT Solver完成驗(yàn)證。表2從表達(dá)性、擴(kuò)展性、主要基于的技術(shù)3個(gè)方面對(duì)上述工具進(jìn)行了總結(jié)，其中，表達(dá)性是指分析網(wǎng)絡(luò)功能的能力，如路由、NAT(網(wǎng)絡(luò)地址轉(zhuǎn)換)、IP分片等，擴(kuò)展性是指工具擴(kuò)展到大型網(wǎng)絡(luò)的能力。

表2 數(shù)據(jù)平面驗(yàn)證工具總結(jié)

總 結(jié)

網(wǎng)絡(luò)驗(yàn)證的目的是保證網(wǎng)絡(luò)按照高級(jí)策略意圖忠實(shí)的運(yùn)行，即網(wǎng)絡(luò)真實(shí)行為與策略一致。本文主要對(duì)網(wǎng)絡(luò)驗(yàn)證中的控制平面驗(yàn)證和數(shù)據(jù)平面驗(yàn)證兩個(gè)方向中的現(xiàn)有研究進(jìn)行了簡單概述。整體上來看，工具大多是基于形式化方法實(shí)現(xiàn)的，如基于SMT/SAT求解器的Minesweeper、Batfish、Anteater、NOD、SecGuru;基于符號(hào)執(zhí)行的HSA。其他工具如rcc、ARC、ERA通過不同的建模方法實(shí)現(xiàn)了驗(yàn)證。上述工具的特點(diǎn)是基于模型的形式化驗(yàn)證，本質(zhì)上是一種狀態(tài)機(jī)驗(yàn)證技術(shù)。其大致框架如圖2所示，首先將平面信息進(jìn)行建模，然后使用與建模方法對(duì)應(yīng)的算法或工具，驗(yàn)證對(duì)應(yīng)模型下的策略不變式，以檢測出不符合策略的錯(cuò)誤，保證網(wǎng)絡(luò)的真實(shí)行為與該策略一致。

圖2 控制平面驗(yàn)證與數(shù)據(jù)平面驗(yàn)證大致框架

除了控制平面驗(yàn)證與數(shù)據(jù)平面驗(yàn)證，網(wǎng)絡(luò)驗(yàn)證還有很多其他方向。例如，網(wǎng)絡(luò)測試通過生成測試數(shù)據(jù)包以確保網(wǎng)絡(luò)設(shè)備忠實(shí)的按照控制平面建立了轉(zhuǎn)發(fā)信息，而且忠實(shí)的按照轉(zhuǎn)發(fā)信息完成轉(zhuǎn)發(fā);網(wǎng)絡(luò)規(guī)范的自動(dòng)綜合旨在開發(fā)一種綜合工具從高級(jí)的策略中自動(dòng)生成正確的配置;網(wǎng)絡(luò)調(diào)試旨在網(wǎng)絡(luò)領(lǐng)域中找到逐步調(diào)試、監(jiān)視、斷點(diǎn)、掛起或恢復(fù)等功能的等效實(shí)現(xiàn)方法。未來，網(wǎng)絡(luò)驗(yàn)證仍需要解決一些面臨的問題，如有狀態(tài)網(wǎng)絡(luò)(如包含有狀態(tài)防火墻等中間件的網(wǎng)絡(luò))下的驗(yàn)證、復(fù)雜路由場景下的控制平面驗(yàn)證以及定量屬性(延遲、帶寬)不變式的驗(yàn)證等。

參考文獻(xiàn)

[1] Veriflow. Network Complexity, Change, and Human Factors are Failing the Business. https://www.veriflow.net/survey/.

[2] John Graham-Cumming. Cloudflare outage caused by bad software deploy [EB/OL]. https://blog.cloudflare.com/cloudflare-outage/,2019–07–02.

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

[4] Brat G, Drusinsky D, Giannakopoulou D, et al. Experimental evaluation of verification and validation tools on martian rover software[J]. Formal Methods in System Design, 2004, 25(2-3): 167-198.

[5] Feamster N, Balakrishnan H. Detecting BGP configuration faults with static analysis[C]. networked systems design and implementation, 2005: 43-56.

[6] Fogel A, Fung S, Pedrosa L, et al. A general approach to network configuration analysis[C]. networked systems design and implementation, 2015: 469-483.

[7] Gemberjacobson A, Viswanathan R, Akella A, et al. Fast Control Plane Analysis Using an Abstract Representation[C]. acm special interest group on data communication, 2016: 300-313.

[8] Fayaz S K, Sharma T, Fogel A, et al. Efficient network reachability analysis using a succinct control plane representation[C]. operating systems design and implementation, 2016: 217-232.

[9] Beckett R, Gupta A, Mahajan R, et al. A General Approach to Network Configuration Verification[C]. acm special interest group on data communication, 2017: 155-168.

[10] Mai H, Khurshid A, Agarwal R, et al. Debugging the data plane with anteater[C]. acm special interest group on data communication, 2011, 41(4): 290-301.

[11] Kazemian P, Varghese G, Mckeown N, et al. Header space analysis: static checking for networks[C]. networked systems design and implementation, 2012: 9-9

[12] Lopes N P, Bjorner N, Godefroid P, et al. Checking beliefs in dynamic networks[C]. networked systems design and implementation, 2015: 499-512.

[13] Lopes N P, Bjørner N, Godefroid P, et al. Network verification in the light of program verification[J]. MSR, Rep, 2013.

[14] Jayaraman K, Bjørner N, Outhred G, et al. Automated analysis and debugging of network connectivity policies[J]. Microsoft Research, 2014: 1-11.