引 言

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

[[332104]]

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

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

背景知識

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

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

控制平面驗證

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

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

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

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

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

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

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

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

數(shù)據(jù)平面驗證

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

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

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

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

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

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

總 結(jié)

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

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

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

參考文獻

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