01 背景

數(shù)據(jù)平面驗(yàn)證技術(shù)可以通過驗(yàn)證設(shè)備的數(shù)據(jù)平面來檢測網(wǎng)絡(luò)錯誤，盡可能減少網(wǎng)絡(luò)錯誤帶來的代價(jià)，這也是減少網(wǎng)絡(luò)中斷的一種重要技術(shù)。目前，數(shù)據(jù)平面驗(yàn)證工具已經(jīng)做到了在微秒級別上實(shí)現(xiàn)數(shù)據(jù)平面的增量更新的驗(yàn)證。雖然研究人員在實(shí)現(xiàn)快速數(shù)據(jù)平面驗(yàn)證方面取得了重大進(jìn)展，但是現(xiàn)有的數(shù)據(jù)平面驗(yàn)證技術(shù)無法有效處理大規(guī)模網(wǎng)絡(luò)的更新風(fēng)暴場景（短時間內(nèi)發(fā)生大量數(shù)據(jù)平面更新）和長尾更新場景（有些交換機(jī)的更新需要很長時間到達(dá)）。原因：現(xiàn)有的數(shù)據(jù)平面技術(shù)處理大型數(shù)據(jù)中心的更新風(fēng)暴場景往往需要耗費(fèi)數(shù)小時，甚至更長時間；而由于有些數(shù)據(jù)平面更新需要經(jīng)過一段延遲時間才能到達(dá)，那很可能導(dǎo)致驗(yàn)證者使用不完整不一致的數(shù)據(jù)平面來驗(yàn)證，進(jìn)而得到的驗(yàn)證結(jié)果也是不正確的。

02 設(shè)計(jì)

針對上述兩種場景或者當(dāng)兩種場景同時存在，作者提出了Flash，它可以針對更新風(fēng)暴、長尾更新或兩者都存在時的場景實(shí)現(xiàn)快速、一致的數(shù)據(jù)平面驗(yàn)證。Flash引入了快速逆模型轉(zhuǎn)換（Fast IMT）以有效地處理更新風(fēng)暴，引入了早期檢測機(jī)制以處理長尾更新場景。接下來我們將闡述Flash的工作流程和兩種關(guān)鍵技術(shù)（Fast IMT、早期檢測機(jī)制）。

下圖是Flash的架構(gòu)示意圖和工作流程圖。其中有2個關(guān)鍵組成部分：子空間驗(yàn)證器、CE2D（consistent， efficient early detection）調(diào)度器。子空間驗(yàn)證器接收FIB更新，重建數(shù)據(jù)平面狀態(tài)，并驗(yàn)證是否違反了屬性，可以專門用作大規(guī)模網(wǎng)絡(luò)的數(shù)據(jù)平面驗(yàn)證。它與CE2D調(diào)度器協(xié)作來保證早期檢測的一致性和正確性。CE2D調(diào)度器有兩個職責(zé)。首先，它負(fù)責(zé)管理子空間驗(yàn)證器的生命周期，即創(chuàng)建、破壞和重新配置。其次，CE2D調(diào)度器負(fù)責(zé)根據(jù) epoch-verifier映射將FIB更新轉(zhuǎn)發(fā)到子空間驗(yàn)證器。

使用Flash系統(tǒng)的典型工作流程如上圖所示。

1）輸入：基于正則表達(dá)式的規(guī)范語言來指定驗(yàn)證要求，即要驗(yàn)證的數(shù)據(jù)平面屬性。構(gòu)建CE2D驗(yàn)證圖還需要進(jìn)行網(wǎng)絡(luò)拓?fù)浜虸P前綴映射等靜態(tài)配置。

2）在系統(tǒng)啟動并運(yùn)行后，它可以從路由器、代理或網(wǎng)絡(luò)模擬器接收FIB更新。為了獲得一致的早期檢測結(jié)果，這些FIB更新應(yīng)該使用epoch標(biāo)記。

3）在從設(shè)備接收到新epoch后，CE2D調(diào)度程序找到epoch過時的子空間驗(yàn)證器，停止執(zhí)行，并重新配置它們以驗(yàn)證最新epoch。

4）更新epoch-verifier映射，并相應(yīng)地轉(zhuǎn)發(fā)FIB更新。

5）每個子空間驗(yàn)證器都維護(hù)一個逆模型，即數(shù)據(jù)平面的等價(jià)類表示。當(dāng)子空間驗(yàn)證器接收到新的FIB更新時，它首先將它們分派到塊中，這些塊使用Fast IMT覆蓋計(jì)算最新的FIB快照。

6）通過無沖突逆模型覆蓋，獲得與新的FIB快照相一致的最新逆模型。

7）利用逆模型，CE2D驗(yàn)證器對CE2D驗(yàn)證圖進(jìn)行更新，并應(yīng)用早期檢測算法。

8）如果返回一個確定性結(jié)果，驗(yàn)證者將返回子空間的一致的驗(yàn)證結(jié)果。

下圖為Fast IMT的簡單示例。Fast IMT首先使用一種基于合并的高效算法，將大量native更新分解為一組可組合的更新（atomic conflict-free overwrites）。然后，它通過MR2（Map-Reduce-Reduce）算法生成緊湊的conflict-free overwrites，用于更新inverse模型。Map： 在考慮到更高優(yōu)先級規(guī)則后，將每個更新匹配的數(shù)據(jù)包集替換為將由其處理的確切數(shù)據(jù)包集；Reduce-Reduce：這些更新先通過它們執(zhí)行的動作進(jìn)行聚合，再通過它們匹配的數(shù)據(jù)包集進(jìn)行聚合。將MR2（map-reduce-reduce）算法與子空間劃分、重疊規(guī)則的快速查找和持久動作樹等結(jié)合，F(xiàn)ast IMT大大降低了計(jì)算開銷，實(shí)現(xiàn)了高可伸縮性。

早期檢測機(jī)制：Flash使用epoch區(qū)分從不同網(wǎng)絡(luò)狀態(tài)計(jì)算的FIB更新，并對構(gòu)造給一個epoch中的同步設(shè)備的模型應(yīng)用早期檢測機(jī)制，同步設(shè)備的FIB的計(jì)算依據(jù)相同的的網(wǎng)絡(luò)狀態(tài)。然后利用自動機(jī)理論提出新算法以實(shí)現(xiàn)有效的早期檢測。

03 性能評估

作者在更新風(fēng)暴或者長尾更新（或者二者同時存在）場景下對Flash進(jìn)行廣泛的評估。其中，利用大規(guī)模網(wǎng)絡(luò)的數(shù)據(jù)平面，與最先進(jìn)的順序驗(yàn)證更新的數(shù)據(jù)平面驗(yàn)證系統(tǒng)相比，F(xiàn)lash要快9000倍。但在許多情況下，F(xiàn)lash還是比Delta-net要慢。

04 個人觀點(diǎn)

優(yōu)點(diǎn)：

為了在更新風(fēng)暴下有效地執(zhí)行驗(yàn)證，F(xiàn)lash引入了快速逆模型變換，亮點(diǎn)在于不將單個數(shù)據(jù)平面更新逐個合并到數(shù)據(jù)平面模型中，而是將大量native更新分解為一組可組合的更新。此外，為了在長尾更新下有效地執(zhí)行驗(yàn)證，F(xiàn)lash引入的早期檢測機(jī)制能夠在無法獲取完整的數(shù)據(jù)平面情況下進(jìn)行一致、正確的數(shù)據(jù)平面驗(yàn)證，這是其他數(shù)據(jù)平面驗(yàn)證工具做不到的。

不足：

1）文中提到的更新風(fēng)暴和長尾更新情況本質(zhì)上是由于數(shù)據(jù)平面驗(yàn)證工具所采用的集中式架構(gòu)所導(dǎo)致的，F(xiàn)lash仍然采用了這一架構(gòu)，在這種集中式架構(gòu)下，驗(yàn)證器會成為性能瓶頸和單一故障點(diǎn)，因此，無論在大型數(shù)據(jù)中心還是廣域網(wǎng)上，拓展性與實(shí)用性都會受到限制。相比之下，本團(tuán)隊(duì)最近提出的分布式設(shè)備自驗(yàn)證框架Coral（已被HotNets‘22接收，長文版本詳見https://arxiv.org/abs/2205.07808），通過將算力/內(nèi)存密集型的驗(yàn)證計(jì)算分解為輕量、設(shè)備級驗(yàn)證子任務(wù)，下放到網(wǎng)絡(luò)設(shè)備上分布式執(zhí)行，可以實(shí)現(xiàn)大規(guī)模網(wǎng)絡(luò)數(shù)據(jù)平面的網(wǎng)內(nèi)快速自檢。

2）在更新風(fēng)暴場景下，F(xiàn)lash使用的批處理技術(shù)與最近的研究DNA（NSDI 2022）非常相似，其核心創(chuàng)新并沒有在文中體現(xiàn)出來。

3） Flash對數(shù)據(jù)平面驗(yàn)證標(biāo)稱的最多9000倍的加速效果，有非常大的一部分來自于Libra（NSDI 2014）提出的報(bào)文空間分區(qū)，去除這一部分之后，F(xiàn)lash的加速效果并不高。

4）Flash是否能實(shí)現(xiàn)packet transformer等功能以及是否仍然具備高性能和低開銷，這是不可知的。

5）個人認(rèn)為早期檢測機(jī)制只適用于少數(shù)長尾更新場景。

6）性能上，在許多情況下，F(xiàn)lash還是比Delta-net慢。

7）Fast IMT把一組native updates進(jìn)行分解后map與2次reduce，個人認(rèn)為這個過程在某些場景下會很耗時，而且最終reduce效果不佳。

01 背景

網(wǎng)絡(luò)驗(yàn)證通常需要在不同故障模型（確定性和/或概率性）下分析不同空間（報(bào)頭空間、故障空間或產(chǎn)品流量空間）的屬性。現(xiàn)有的驗(yàn)證器可以高效地處理報(bào)頭或故障空間，但不能兩者兼顧；或者同樣高效地處理確定性和概率性的鏈路故障場景驗(yàn)證，但仍不能兼顧。也就是說，目前沒有一個單一的驗(yàn)證器可以同時支持不同的空間覆蓋度和不確定性故障模型的分析。于是本文提出了一種基于符號執(zhí)行的路由計(jì)算SRE（Symbolic Router Execution），一種支持各種分析場景的通用可擴(kuò)展的驗(yàn)證引擎。SRE可以符號化地模擬網(wǎng)絡(luò)模型從而發(fā)現(xiàn)報(bào)文故障等價(jià)類（PFECs），每個PFEC都表示一種在特定故障場景下的具有相同轉(zhuǎn)發(fā)行為的報(bào)頭空間。此外，SRE在符號執(zhí)行期間支持各種優(yōu)化，同時保持對故障種類的不可知性，因此它可以擴(kuò)展到其他種類的包空間。通過二元決策樹BDD對報(bào)頭空間和故障場景進(jìn)行編碼，各類網(wǎng)絡(luò)驗(yàn)證就可以簡化為BDD上的圖算法執(zhí)行（例如，最短路徑）。

02 設(shè)計(jì)

SRE Workflow：SRE通過對鏈路狀態(tài)以及報(bào)頭空間進(jìn)行符號化計(jì)算得到不確定報(bào)頭空間在不確定鏈路故障情況下的轉(zhuǎn)發(fā)表。如下圖， 每一條轉(zhuǎn)發(fā)表項(xiàng)都包含了相應(yīng)的前綴和鏈路狀態(tài)信息（即滿足約束的目的IP和鏈路狀態(tài)條件下才會匹配該表項(xiàng)）。計(jì)算這樣的轉(zhuǎn)發(fā)表包含兩個步驟：一是對故障狀態(tài)做符號執(zhí)行計(jì)算控制平面，即計(jì)算不同目的網(wǎng)段在不同的鏈路故障情況下的轉(zhuǎn)發(fā)表（類似Hoyan）；二是對IP做符號化執(zhí)行計(jì)算數(shù)據(jù)面，根據(jù)符號化的轉(zhuǎn)發(fā)表和配置的ACL計(jì)算具有相同轉(zhuǎn)發(fā)行為的報(bào)文集合（類似AP）。至此就可以得到PFECs，最后把所有的PFECs合并成BDD，則可以將屬性驗(yàn)證轉(zhuǎn)化成圖算法求解。

SRE的屬性驗(yàn)證：SRE將所有滿足/不滿足屬性的PFECs轉(zhuǎn)換成BDD樹來驗(yàn)證，每一條到達(dá)驗(yàn)證節(jié)點(diǎn)的BDD路徑都表示了一種在相同鏈路狀態(tài)條件下的具有相同轉(zhuǎn)發(fā)行為的包空間集合，如圖上所示。然后利用圖算法可以實(shí)現(xiàn)故障場景分析、滿足可能性分析以及差分分析。

03 個人觀點(diǎn)

SRE利用程序分析中的符號執(zhí)行技術(shù)實(shí)現(xiàn)了一種通用的針對網(wǎng)絡(luò)故障場景分析方法。在驗(yàn)證中引入了不確定性，使得流量分析結(jié)果更精確（但不能實(shí)現(xiàn)一些交叉流量分析），同時驗(yàn)證的時間開銷也增長了，但由于只需符號化部分變量，所以開銷相較Minesweeper這類純SMT的驗(yàn)證器耗時仍然較少。這篇文章通過符號化技術(shù)結(jié)合了數(shù)據(jù)面驗(yàn)證和控制面驗(yàn)證的優(yōu)點(diǎn)，達(dá)到了較好的平衡。

01 背景

數(shù)據(jù)平面特定領(lǐng)域編程語言P4在應(yīng)用場景下經(jīng)常伴隨一些錯誤。這些錯誤可以進(jìn)一步細(xì)分為代碼邏輯錯誤、編譯器錯誤和ASIC錯誤。調(diào)查顯示40%的錯誤與編譯器或ASIC有關(guān)（non-code bugs）。目前的p4驗(yàn)證工具（如：Aquila、p4pktgen等）傾向于驗(yàn)證代碼相關(guān)錯誤，而對于非代碼錯誤研究較少。

同時，生產(chǎn)級的應(yīng)用場景會帶來規(guī)模上的挑戰(zhàn)：例如復(fù)雜的控制流圖、多流水線、多交換機(jī)的情況。在一些網(wǎng)關(guān)的生產(chǎn)級程序中，代碼數(shù)量達(dá)到了o（10^14），可能的路徑數(shù)達(dá)到了o（10^197）。面對如此復(fù)雜的程序應(yīng)該如何進(jìn)行遍歷，以達(dá)到100%的路徑覆蓋率同樣也成為很大的挑戰(zhàn)。

02 設(shè)計(jì)

Meissa采用的核心方法是Code Summary。Code Summary是領(lǐng)域特定的，利用了控制流圖中每個流水線都是單起點(diǎn)單終點(diǎn)的特性。總體上來講可以分為流水線內(nèi)的冗余消除和流水線間的公共前置條件過濾。

1）流水線內(nèi)的冗余消除（intra-pipeline redundancy elimination）：使用DFS搜索遍歷流水線內(nèi)部的路徑，選擇其中的合法路徑，同時在過程中收集路徑的語義。這種做法的效果在于1.將一個流水線中本來不合法的路徑刪除以免被其他流水線重復(fù)計(jì)算；2.可以縮短合法路徑的長度。

2）流水線間的公共前置條件過濾（inter-pipeline public pre-condition filtering）：公共前置條件是指從整個控制流圖開始到這個流水線入口處所有可行的合法路徑中共同包含的一些條件。對于下圖中的情況，由于前置流水線將所有協(xié)議統(tǒng)一為TCP，在本流水線中就不需要考慮UDP協(xié)議的情況。

對于整體框架而言，用戶需要輸入P4代碼、對于表項(xiàng)的設(shè)置值以及測試意圖。之后通過拓?fù)渑判虼_定Code Summary的順序。在對于每一個流水線進(jìn)行冗余消除和公共前置條件過濾后得到徹底化簡的CFG。通過對CFG的DFS搜索可以得到全部的測試樣例，將測試樣例跑在真實(shí)的交換機(jī)上即可獲得compiler path 以及 ASIC path以定位非代碼邏輯錯誤。

03 性能評估

實(shí)驗(yàn)顯示Code Summary 能夠在1.2–5.0x的范圍內(nèi)加速M(fèi)eissa的性能，通過Code Summary能夠減少SMT solver 1.8–14.9x 的調(diào)用頻率，同時對于不同的P4程序減少了10^60–10^390x的需遍歷路徑數(shù)量。

04 個人觀點(diǎn)

本文的創(chuàng)新點(diǎn)主要在于：

1）對p4復(fù)雜的控制流圖進(jìn)行了高效的剪枝操作，通過流水線內(nèi)的冗余消除和流水線間的公共前置條件過濾，極大地簡化了控制流圖。與此同時還保持了高精確性（100\%的路徑覆蓋）。

2）考慮到了p4錯誤驗(yàn)證中的非代碼錯誤（來自編譯器或ASIC），通過將簡化CFG的搜索結(jié)果和實(shí)際交換機(jī)測試結(jié)果進(jìn)行對比以定位此類錯誤，很好地彌補(bǔ)了有關(guān)領(lǐng)域研究中的不足。

這篇文章提出了SwitchV，一種自動化的SDN交換機(jī)驗(yàn)證工具，主要由谷歌團(tuán)隊(duì)實(shí)現(xiàn)，合作者來自于布朗大學(xué)和哈佛大學(xué)等高校，其中包括哈佛大學(xué)的俞敏嵐教授。

01 背景

隨著對計(jì)算機(jī)網(wǎng)絡(luò)的可靠性、靈活性以及效率等需求的不斷增加，促使制造商和運(yùn)營商加速設(shè)計(jì)與實(shí)施新的特性的功能。但是，在增加新的功能的同時，需要根據(jù)非規(guī)范文檔進(jìn)行手工編寫大量的測試以保證可靠性，限制了新功能的開發(fā)效率。因此，本文旨在實(shí)現(xiàn)一種工具，幫助在保證可靠性的同時，能夠?qū)崿F(xiàn)新功能的快速開發(fā)。

02 設(shè)計(jì)

為實(shí)現(xiàn)該目標(biāo)，文章提出了SwitchV，整體思想是使用P4語言建模交換機(jī)行為，然后基于P4程序使用測試技術(shù)完成控制平面和數(shù)據(jù)平面的驗(yàn)證，可以分為3個步驟實(shí)現(xiàn)：

1） 使用P4編程語言建模交換機(jī)行為：P4編程語言原本是用來控制網(wǎng)絡(luò)設(shè)備的數(shù)據(jù)平面轉(zhuǎn)發(fā)行為的，但作者發(fā)現(xiàn)P4的語言特性非常適合表達(dá)交換機(jī)行為，而且可以進(jìn)一步使用符號執(zhí)行技術(shù)。此外，P4程序可以直接作為網(wǎng)絡(luò)交換機(jī)的文檔，相比于非規(guī)范文檔更加適合功能創(chuàng)新。由于P4語言缺少約束的定義，作者擴(kuò)展實(shí)現(xiàn)了P4-constraints，可以用于建模Isolated或Integrity方面的約束。

2）控制平面驗(yàn)證：提出了一個模糊測試工具（Fuzzer）用于檢查交換機(jī)是否會正確接收或拒絕控制平面請求。Fuzzer首先根據(jù)P4程序生成許多有效（valid）或無效（invalid）的控制平面更新請求，然后發(fā)送這些更新請求，并觀察交換機(jī)是否會正確處理。其中，有效和無效是相對于P4程序中的約束而言，且文中提出了一些優(yōu)化方法用于處理狀態(tài)爆炸問題。

3）數(shù)據(jù)平面驗(yàn)證：提出了P4-SYMBOLIC，通過比對P4模擬器和真實(shí)交換機(jī)的轉(zhuǎn)發(fā)行為，完成數(shù)據(jù)平面驗(yàn)證。P4-SYMBOLIC運(yùn)行流程如圖所示，測試人員首先輸入P4程序、表?xiàng)l目以及最小覆蓋范圍，然后基于P4程序使用符號執(zhí)行技術(shù)分析控制流，如果符號執(zhí)行結(jié)果滿足覆蓋約束，則生成測試數(shù)據(jù)包發(fā)送到模擬器和真實(shí)交換機(jī)，通過比對轉(zhuǎn)發(fā)行為完成驗(yàn)證。

03 性能評估

SwitchV已經(jīng)在谷歌的實(shí)際網(wǎng)絡(luò)中部署運(yùn)行，實(shí)驗(yàn)結(jié)果表明SwitchV可以發(fā)現(xiàn)出多種類型的錯誤（如圖所示），且許多錯誤不能被傳統(tǒng)的測試技術(shù)發(fā)現(xiàn)。性能方面，在生產(chǎn)網(wǎng)絡(luò)中，整個測試過程可以以秒級速度完成，且最慢的是SMT求解過程。

04 個人觀點(diǎn)

本篇文章創(chuàng)新性地使用了P4語言建模交換機(jī)行為，相比以往采用的英文文檔描述方法，P4語言更加規(guī)范易讀而且利于未來的迭代開發(fā)。在其基礎(chǔ)之上，SwitchV使用自動化測試技術(shù)（fuzz，符號執(zhí)行）對交換機(jī)的控制平面與數(shù)據(jù)平面進(jìn)行驗(yàn)證，以保證交換機(jī)行為的正確性，相比以往采用的手工測試套件，具有更高的可靠性和效率。不過，SwitchV也存在一定的局限性，例如需要人工將交換機(jī)行為抽象成P4程序；只支持部分P4語言特性；測試技術(shù)無法完全保證正確性等。

01 背景

在實(shí)際物理測試平臺中，整個系統(tǒng)中端到端時延的測量對網(wǎng)絡(luò)系統(tǒng)的評估具有有重大意義，但往往很難取得。現(xiàn)存的模擬軟件（ns-2， ns-3， OMNet+等）由于不支持所有的組件，或不支持某些技術(shù)細(xì)節(jié)，同樣也很難實(shí)現(xiàn)端到端測量。本文旨在提出一種模塊化的模擬測試工具，靈活的將各種組件（內(nèi)存、處理器、多種設(shè)備、網(wǎng)絡(luò)）專屬的模擬器組合在一起，搭建了能夠?qū)崿F(xiàn)端到端測量的測試平臺。

02 設(shè)計(jì)

不同于重新構(gòu)建一個模擬器的思路，simBricks 選擇將現(xiàn)存的一些模擬器整合為一個支持不同操作系統(tǒng)、驅(qū)動和具體應(yīng)用的全系統(tǒng)模擬器。

主要面臨以下困難：1） 不同模擬器之間沒有相互調(diào)用接口。2） 模塊間實(shí)現(xiàn)同步困難 。3） 需要將不兼容的模塊進(jìn)行整合。

simBricks根據(jù)實(shí)際物理設(shè)備的邊界（PCIe and Ethernet links）來定義接口，每個模塊都由獨(dú)立、并行的進(jìn)程運(yùn)行，通過共享內(nèi)存隊(duì)列進(jìn)行交流。simBricks設(shè)計(jì)了一個針對模擬器之間拓?fù)潢P(guān)系和時延，用來進(jìn)行時鐘同步的協(xié)議。同時為了實(shí)現(xiàn)可擴(kuò)展性，simBricks引入了代理來基于TCP 或 RDMA傳輸消息。

03 性能評估

simBricks的模擬實(shí)驗(yàn)在以下環(huán)境中進(jìn)行：two 22-core Intel Xeon Gold 6152 processors at 2.10 GHz with 187 GB of memory， hyper-threading disabled， and 100 Gbps Mellanox ConnectX-5 NICs. 模擬中每臺主機(jī)有單核8G內(nèi)存，運(yùn)行 Ubuntu 18.04 with kernel 5.4.46。實(shí)驗(yàn)顯示simBricks相比于gem5模擬器性能上有較大提升。同時還通過ns-3 默認(rèn)參數(shù)的 network link和SimBricks Ethernet adapter在傳輸報(bào)文的log-level對比，表明simBricks的以太網(wǎng)和PCIe接口能夠精確地實(shí)現(xiàn)模擬器之間的同步。

04 個人觀點(diǎn)

全系統(tǒng)的端到端通信時延測量對于用戶體驗(yàn)評估、系統(tǒng)性能瓶頸定位具有實(shí)用價(jià)值。本文提出的SimBricks是一款高性能、高可擴(kuò)展性的端到端模擬器，能夠精確的同步不同的模擬器組件。SimBricks的主要設(shè)計(jì)思路在于將現(xiàn)有的模擬器整合到一起，其處理時鐘同步以及模塊間通信的設(shè)計(jì)具有相當(dāng)?shù)墓ぷ髁俊?/p>