確保業務意圖在網絡中的正確實施——網絡驗證
引 言
隨著網絡變得復雜和龐大，網絡管理也變得更加困難，網絡升級或改造過程中的細小失誤可能會對網絡的正常運行造成嚴重影響。根據Veriflow公司于2016年對315名IT專業人員進行的調查得出的結果，59%的受訪者表示網絡復雜性的增加導致了更頻繁的中斷，74%的人表示網絡變化每年或多次對企業產生重大影響[1]。2019年7月3日，Cloudflare公司在新的Web應用層防火墻中部署了一個配置錯誤的規則，導致了全球大面積宕機[2]。配置錯誤、硬軟件實現錯誤、網絡攻擊或協議交互的意外錯誤都會影響網絡的可用性和安全性。那么，關鍵問題在于我們如何才能確保業務的意圖在復雜的網絡環境中正確的實施運行?
過去幾年，已經出現了一個新的研究領域，即網絡驗證，旨在嚴格確保網絡按期望的業務意圖運行。網絡驗證的技術靈感來源于形式化方法，一種廣義上基于數學方法，通過對復雜系統建立嚴格的數學模型，驗證系統的性能與行為正確性的方法，主要有模型檢測、定理證明、符號執行及SMT/SAT(可滿足性理論)求解器四種技術[3]。形式化驗證已經在硬軟件領域得到的成功的應用。例如，NASA(美國航空航天局)成功使用形式化驗證技術在火星探測器飛行軟件中發現了并發錯誤[4]。如果我們可以驗證硬軟件，為什么不驗證網絡?最近，網絡驗證在驗證和程序語言社區變得逐漸流行起來，學術界和產業界都開展了網絡驗證的相關研究。在學術界，主要有斯坦福大學、伊利諾伊大學香檳分校、加州大學洛杉磯分校、卡內基梅隆大學以及清華大學等高校。在工業界，主要有微軟研究院和AT&T實驗室。目前，該領域已經出現了一些初創公司，如Forward Networks、Veriflow、Intentionet。
本文將首先介紹一些相關背景知識，然后分別介紹網絡驗證中的控制平面驗證和數據平面驗證兩個研究方向，最后進行總結。
背景知識
網絡從路由轉發的角度可以被分為三層，即策略、控制平面和數據平面，如圖1所示[3]。策略是控制平面和數據平面的參考，體現了網絡管理人員的意圖，如主機A是否允許和主機B通信?？刂破矫媸怯糜趯崿F策略的，在傳統網絡中是指分散于各處的網絡設備中的配置文件，在SDN(軟件定義網絡)中是指各種應用。數據平面是網絡中根據控制平面生成的轉發信息與拓撲結構，其中轉發信息在傳統網絡中是指轉發表，在SDN中是指流表。根據控制平面和數據平面兩個層次，網絡驗證有控制平面驗證和數據平面驗證兩個研究方向，其通過分析對應平面信息，然后驗證網絡策略的不變式完成檢查。其中，不變式是一種屬性，在網絡中特指路由轉發行為的正確屬性，如無轉發循環不變式，斷言了數據包在網絡中不會出現轉發循環。在對一個特定網絡如企業網、校園網進行驗證時，除了需要考慮該網絡的控制平面或數據平面信息，還需要考慮網絡環境的因素，如網絡外部發送給網絡的路由通告。
圖1 網絡層次劃分情況
控制平面驗證
控制平面驗證通過輸入控制平面信息，驗證網絡策略的不變式以確保控制平面與策略要求的一致。其優點是可以在配置部署到網絡之前完成驗證，能夠方便的定位到錯誤的配置位置;缺點是需要分析配置文件與網絡行為之間的復雜關系，以及考慮形式各異的配置語言。
目前，傳統網絡目前仍占據主導地位，其控制平面的配置文件分散在各處的網絡設備中，驗證面臨狀態爆炸問題。相關研究方面，Feamster等人于2005年提出了rcc工具[5]，是第一個能在真實網絡中檢測BGP(邊界網關協議)故障的靜態分析工具，但其檢查的范圍僅限于BGP協議。rcc采用的是靜態分析的方法，其將控制平面信息標準化成SQL數據，然后驗證根據策略轉換成的SQL上的約束條件判斷BGP配置的正確性。為了提高驗證范圍，不再局限于特定的協議，Fogel等人提出了Batfish工具[6]。
Batfish并沒有選擇在控制平面上進行建模，而是選擇通過控制平面生成數據平面，然后調用數據平面驗證工具進行驗證。這種方式結合了控制平面驗證和數據平面驗證的優點，既能提前檢測錯誤也不需考慮協議的復雜交互。但是，Batfish面臨著一個難題，即如何根據配置和環境生成一個可靠的數據平面，其通過使用DataLog(一種數據查詢語言)的一種變式LogiQL建立了一個陳述式模型以解決此挑戰。由于Batfish需要對整個數據平面進行模擬，速度很慢。Gemberjacobson等人發現，生成詳細的數據平面是不必要的，提出了ARC，可以直接在控制平面進行快速分析[7]。
ARC使用加權有向圖對控制平面建模，使用圖算法進行分析完成驗證。對于特定的屬性不變式，可以比Batfish快出了三個數量級。但是，ARC只對一些特定的協議組合進行了分析，如OSPF，RIP，eBGP。為提高驗證的協議范圍，Fayaz等人提出了ERA工具[8]。
ERA使用二元決策圖(BDD)對控制平面建模，通過探索BDD模型完成驗證。相比ARC可以驗證更多協議，相比Batfish驗證速度快了2.5到17倍，且可以擴展到大型網絡中。Beckett等人指出，控制平面驗證的主要難點在于構建一個具有高度的網絡設計覆蓋范圍與高度數據平面覆蓋范圍的驗證工具，同時保持足夠高的可擴展性[9]。
其中，網絡設計覆蓋范圍是指工具能夠支持網絡的拓撲類型、路由協議和其他一些特點的范圍;數據平面覆蓋范圍是指工具能夠支持的數據平面的范圍。為解決該挑戰，Beckett等人提出了Minesweeper工具。Minesweeper使用SMT公式對控制平面建模，將公式放入SMT Solver中完成驗證。相比之前的控制平面驗證工具，可以驗證更多的協議，覆蓋更大的數據平面，且可以擴展到大型網絡。值得說明的是，ARC、ERA和Minesweeper都使用了Batfish的配置解析器將不同廠商的配置轉換為無關廠商的統一格式。表1從網絡設計覆蓋范圍、擴展性、主要基于的技術3個方面對上述工具進行了總結。其中，擴展性是指工具擴展到大型網絡的能力。
表1 傳統網絡控制平面驗證工具總結
在SDN中，網絡行為是集中由控制器決定的，這使得驗證網絡變得簡單。目前SDN控制平面驗證主要集中在兩方面，一是對SDN程序的驗證，二是開發驗證控制器[3]。SDN使用應用程序制定策略管理網絡設備，如路由或訪問控制。如普通的軟件程序一樣，SDN程序會出現設計或實現錯誤，如果盲目的部署在網絡中，很容易引起故障的發生。驗證控制器用于檢查控制器是否按照策略正確安裝規則，因為其特定的編程語言支持不變式驗證，可以在編譯時與規則安裝到交換機之前進行驗證，防止錯誤的規則下發。目前，SDN程序驗證方向有Verificare、VeriCon等工具，驗證控制器方向有NetCore、NDLog、NetKAT等工具。
數據平面驗證
數據平面驗證通過輸入數據平面信息，驗證網絡策略的不變式以確保數據平面與策略要求的一致。其優點是數據平面直接體現了配置的影響，分析起來更加簡單。但是，其不能在配置部署前完成驗證，而且需要重復采集數據以應對網絡波動帶來的數據平面變化。此外，數據平面驗證不能提供錯誤配置的出處，需要人員自行關聯發現，由于網絡行為與配置文件之間的復雜關系，這是十分困難的。數據平面驗證方面，傳統網絡與SDN網絡的唯一區別在于數據采集過程，傳統網絡可以通過SNMP(簡單網絡管理協議)，終端或者控制會話來收集轉發表，而SDN網絡可以監視控制器獲得。
由于控制平面驗證不能發現網絡設備將控制平面轉換成數據平面的實現錯誤，以及存在分析復雜的問題，Mai等人于2011年提出了第一個在真實網絡中發現錯誤的數據平面分析工具Anteater[10]。Anteater首先根據數據平面信息將網絡建模成為一個圖，然后將不變式建模為圖上的函數，最后將函數轉換為SAT公式放入SAT Solver進行求解。Anteater通過實驗證明，分析數據平面是一種可行方法，相比于控制平面驗證速度不一定更快，但實現方法上相比更容易。
Kazemian等人之后提出了一種數據平面驗證框架HSA [11]。HSA框架是基于幾何模型的，其將數據包建模成幾何空間中的點，用頭空間(Header Space)即最大長度為L的{0,1}字符串表示，網絡設備建模成該幾何空間上的轉移函數，通過分析特定數據包頭部在幾何空間的變化，進行不變式的驗證。相比于其他基于形式化驗證方法的工具，HSA可以提供所有反例，使分析錯誤變得高效。Veriflow和NetPlumber使用等價類與增量技術分別改進了Anteater和HSA，有足夠的速度和擴展性。
Lopes等人認為，Veriflow和NetPlumber是定制化的代碼，難以擴展到新的數據包格式和協議。而網絡驗證若要發展成為一個網絡CAD行業，必須要發展成一個更標準化、更加可擴展的技術。為解決該挑戰，Lopes等人基于Datalog技術，提出了NOD工具[12,13]。NOD使用Datalog對策略和協議行為編碼，能夠進行通用的擴展，最后使用基于SMT Solver技術的Z3 Datalog框架進行驗證。實驗表明，NOD的Datalog模型計算可達數據集合比模型檢測和SMT計算單個可達數據都快，相比于基于HSA的Hassel工具，雖然速度相比較慢，但更易于通用化。為專注于驗證訪問控制策略的正確實施，Jayaraman等人提出了SecGuru工具，是NOD的早期版本, 已經被部署在Azure中以檢查數以百計的路由器和防火墻的正確性[14]。
SecGuru使用位向量對數據平面和策略進行編碼，然后將這種位向量邏輯放入Z3 SMT Solver完成驗證。表2從表達性、擴展性、主要基于的技術3個方面對上述工具進行了總結，其中，表達性是指分析網絡功能的能力，如路由、NAT(網絡地址轉換)、IP分片等，擴展性是指工具擴展到大型網絡的能力。
表2 數據平面驗證工具總結
總 結
網絡驗證的目的是保證網絡按照高級策略意圖忠實的運行，即網絡真實行為與策略一致。本文主要對網絡驗證中的控制平面驗證和數據平面驗證兩個方向中的現有研究進行了簡單概述。整體上來看，工具大多是基于形式化方法實現的，如基于SMT/SAT求解器的Minesweeper、Batfish、Anteater、NOD、SecGuru;基于符號執行的HSA。其他工具如rcc、ARC、ERA通過不同的建模方法實現了驗證。上述工具的特點是基于模型的形式化驗證，本質上是一種狀態機驗證技術。其大致框架如圖2所示，首先將平面信息進行建模，然后使用與建模方法對應的算法或工具，驗證對應模型下的策略不變式，以檢測出不符合策略的錯誤，保證網絡的真實行為與該策略一致。
圖2 控制平面驗證與數據平面驗證大致框架
除了控制平面驗證與數據平面驗證，網絡驗證還有很多其他方向。例如，網絡測試通過生成測試數據包以確保網絡設備忠實的按照控制平面建立了轉發信息，而且忠實的按照轉發信息完成轉發;網絡規范的自動綜合旨在開發一種綜合工具從高級的策略中自動生成正確的配置;網絡調試旨在網絡領域中找到逐步調試、監視、斷點、掛起或恢復等功能的等效實現方法。未來，網絡驗證仍需要解決一些面臨的問題，如有狀態網絡(如包含有狀態防火墻等中間件的網絡)下的驗證、復雜路由場景下的控制平面驗證以及定量屬性(延遲、帶寬)不變式的驗證等。
參考文獻
[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.
