01 背景

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

02 設計

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

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

使用Flash系統的典型工作流程如上圖所示。

1）輸入：基于正則表達式的規范語言來指定驗證要求，即要驗證的數據平面屬性。構建CE2D驗證圖還需要進行網絡拓撲和IP前綴映射等靜態配置。

2）在系統啟動并運行后，它可以從路由器、代理或網絡模擬器接收FIB更新。為了獲得一致的早期檢測結果，這些FIB更新應該使用epoch標記。

3）在從設備接收到新epoch后，CE2D調度程序找到epoch過時的子空間驗證器，停止執行，并重新配置它們以驗證最新epoch。

4）更新epoch-verifier映射，并相應地轉發FIB更新。

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

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

7）利用逆模型，CE2D驗證器對CE2D驗證圖進行更新，并應用早期檢測算法。

8）如果返回一個確定性結果，驗證者將返回子空間的一致的驗證結果。

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

早期檢測機制：Flash使用epoch區分從不同網絡狀態計算的FIB更新，并對構造給一個epoch中的同步設備的模型應用早期檢測機制，同步設備的FIB的計算依據相同的的網絡狀態。然后利用自動機理論提出新算法以實現有效的早期檢測。

03 性能評估

作者在更新風暴或者長尾更新（或者二者同時存在）場景下對Flash進行廣泛的評估。其中，利用大規模網絡的數據平面，與最先進的順序驗證更新的數據平面驗證系統相比，Flash要快9000倍。但在許多情況下，Flash還是比Delta-net要慢。

04 個人觀點

優點：

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

不足：

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

2）在更新風暴場景下，Flash使用的批處理技術與最近的研究DNA（NSDI 2022）非常相似，其核心創新并沒有在文中體現出來。

3） Flash對數據平面驗證標稱的最多9000倍的加速效果，有非常大的一部分來自于Libra（NSDI 2014）提出的報文空間分區，去除這一部分之后，Flash的加速效果并不高。

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

5）個人認為早期檢測機制只適用于少數長尾更新場景。

6）性能上，在許多情況下，Flash還是比Delta-net慢。

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

01 背景

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

02 設計

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

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

03 個人觀點

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

01 背景

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

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

02 設計

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

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

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

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

03 性能評估

實驗顯示Code Summary 能夠在1.2–5.0x的范圍內加速Meissa的性能，通過Code Summary能夠減少SMT solver 1.8–14.9x 的調用頻率，同時對于不同的P4程序減少了10^60–10^390x的需遍歷路徑數量。

04 個人觀點

本文的創新點主要在于：

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

2）考慮到了p4錯誤驗證中的非代碼錯誤（來自編譯器或ASIC），通過將簡化CFG的搜索結果和實際交換機測試結果進行對比以定位此類錯誤，很好地彌補了有關領域研究中的不足。

這篇文章提出了SwitchV，一種自動化的SDN交換機驗證工具，主要由谷歌團隊實現，合作者來自于布朗大學和哈佛大學等高校，其中包括哈佛大學的俞敏嵐教授。

01 背景

隨著對計算機網絡的可靠性、靈活性以及效率等需求的不斷增加，促使制造商和運營商加速設計與實施新的特性的功能。但是，在增加新的功能的同時，需要根據非規范文檔進行手工編寫大量的測試以保證可靠性，限制了新功能的開發效率。因此，本文旨在實現一種工具，幫助在保證可靠性的同時，能夠實現新功能的快速開發。

02 設計

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

1） 使用P4編程語言建模交換機行為：P4編程語言原本是用來控制網絡設備的數據平面轉發行為的，但作者發現P4的語言特性非常適合表達交換機行為，而且可以進一步使用符號執行技術。此外，P4程序可以直接作為網絡交換機的文檔，相比于非規范文檔更加適合功能創新。由于P4語言缺少約束的定義，作者擴展實現了P4-constraints，可以用于建模Isolated或Integrity方面的約束。

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

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

03 性能評估

SwitchV已經在谷歌的實際網絡中部署運行，實驗結果表明SwitchV可以發現出多種類型的錯誤（如圖所示），且許多錯誤不能被傳統的測試技術發現。性能方面，在生產網絡中，整個測試過程可以以秒級速度完成，且最慢的是SMT求解過程。

04 個人觀點

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

01 背景

在實際物理測試平臺中，整個系統中端到端時延的測量對網絡系統的評估具有有重大意義，但往往很難取得。現存的模擬軟件（ns-2， ns-3， OMNet+等）由于不支持所有的組件，或不支持某些技術細節，同樣也很難實現端到端測量。本文旨在提出一種模塊化的模擬測試工具，靈活的將各種組件（內存、處理器、多種設備、網絡）專屬的模擬器組合在一起，搭建了能夠實現端到端測量的測試平臺。

02 設計

不同于重新構建一個模擬器的思路，simBricks 選擇將現存的一些模擬器整合為一個支持不同操作系統、驅動和具體應用的全系統模擬器。

主要面臨以下困難：1） 不同模擬器之間沒有相互調用接口。2） 模塊間實現同步困難 。3） 需要將不兼容的模塊進行整合。

simBricks根據實際物理設備的邊界（PCIe and Ethernet links）來定義接口，每個模塊都由獨立、并行的進程運行，通過共享內存隊列進行交流。simBricks設計了一個針對模擬器之間拓撲關系和時延，用來進行時鐘同步的協議。同時為了實現可擴展性，simBricks引入了代理來基于TCP 或 RDMA傳輸消息。

03 性能評估

simBricks的模擬實驗在以下環境中進行：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. 模擬中每臺主機有單核8G內存，運行 Ubuntu 18.04 with kernel 5.4.46。實驗顯示simBricks相比于gem5模擬器性能上有較大提升。同時還通過ns-3 默認參數的 network link和SimBricks Ethernet adapter在傳輸報文的log-level對比，表明simBricks的以太網和PCIe接口能夠精確地實現模擬器之間的同步。

04 個人觀點

全系統的端到端通信時延測量對于用戶體驗評估、系統性能瓶頸定位具有實用價值。本文提出的SimBricks是一款高性能、高可擴展性的端到端模擬器，能夠精確的同步不同的模擬器組件。SimBricks的主要設計思路在于將現有的模擬器整合到一起，其處理時鐘同步以及模塊間通信的設計具有相當的工作量。