[發明專利]一種對計算機網絡數據平面進行增量驗證的方法與系統

有效

• 申請號: 202010087150.6
• 申請日: 2020-02-11
• 公開（公告）號: CN111431732B
• 公開（公告）日: 2021-04-20
• 發明（設計）人: 張鵬;劉旭;楊宏坤
• 申請（專利權）人: 西安交通大學
• 主分類號: H04L12/24
• 分類號: H04L12/24;H04L29/06;G06F40/126;G06F40/289
• 代理公司: 西安通大專利代理有限責任公司 61200
• 代理人: 郭瑤

1.一種對計算機網絡數據平面進行增量驗證的方法，其特征在于，包括以下步驟：

步驟1:根據數據平面設備配置構造端口謂詞映射模型，即PPM模型，PPM模型將在每個元素中轉發行為相同的數據包劃分為一個等價類，并將等價類用謂詞表示，PPM用謂詞對等價類進行編碼；

步驟2:獲取數據平面狀態更新，并將獲取的更新轉化為增量更新規則，然后對每一條更新規則更新PPM模型，得到每一次更新的移動的謂詞集合；

步驟3:根據更新后的PPM模型拓撲與更新后移動的謂詞集合構造增量轉發圖；

步驟4:在增量轉發圖上驗證網絡正確性；

步驟4包括驗證網絡不變量、驗證網絡策略和分析鏈路故障；

1)一種用于驗證網絡不變量的遍歷增量轉發圖的方法，該方法的輸入為增量轉發圖G，移動的謂詞集D，圖中的節點集V；

對每個節點s∈V，其中V包含了與更新規則的元素相關的所有節點，開始執行遍歷過程；在每次遍歷之前，初始化當前謂詞集pset為移動的謂詞集D，初始化遍歷過的節點集history為空；在pset為空或遍歷的節點已存在于history中，又或下一跳為default這三種情況時終止流程；第一種情況表示不變量未被破壞，第二種情況表示網絡存在環路，第三種情況表示pset不匹配任何轉發規則，即網絡存在黑洞；若三種情況都不滿足，則將當前謂詞集pset更新為pset∧A(s,s′)，將遍歷過的節點集history更新為history∪{s}，向下一跳繼續遍歷增量轉發圖；

2)驗證網絡策略的過程為：令D為某一次更新后移動的謂詞集，計算新的謂詞集合D_q←{δ∈D|δ∧q≠False}，并基于新的謂詞集合D_q構造增量轉發圖Gq；網絡策略驗證單元遍歷Gq，同時為每個謂詞p_i∈D_q更新自動機A的一個實例，記為A_i；每當謂詞p_i訪問增量轉發圖中的新節點，網絡策略驗證單元就更新自動機A_i；如果遍歷后所有自動機都進入接收狀態，則網絡更新滿足該策略；否則，將違反該策略；

3)分析鏈路故障的過程為：首先使用失效鏈路上的等價類構造增量轉發圖，然后應用上述一種用于驗證網絡不變量的遍歷增量轉發圖的方法遍歷增量轉發圖進行不變量驗證。

2.根據權利要求1所述的一種對計算機網絡數據平面進行增量驗證的方法，其特征在于，所述步驟1中，構造PPM模型的具體過程為：將網絡功能劃分轉發、過濾和重寫三種類型，對應地定義轉發、過濾和重寫三種元素，將交換機按功能表示為一個或多個元素，并按照功能之間的邏輯通過端口連接這些元素得到PPM模型。

3.根據權利要求1所述的一種對計算機網絡數據平面進行增量驗證的方法，其特征在于，所述步驟1中，為不同類型的元素單獨計算等價類。

4.根據權利要求1所述的一種對計算機網絡數據平面進行增量驗證的方法，其特征在于，所述步驟2中，記待更新規則為r，表示為一個三元組(priority,match,action)，其中priority表示優先級，match表示匹配域，action表示動作域；待更新規則的元素記作e，對每一條待更新規則更新PPM模型包括以下步驟：

步驟2.1、編碼規則匹配域，得到二元決策圖：利用二元決策圖對一個規則的匹配域的布爾表達式進行編碼，編碼后，規則r的匹配域被編碼為一個二元決策圖，二元決策圖用r.match表示；

步驟2.2、分析轉發行為變化：

步驟2.2.1、定義三元組(δ,from,to)表示轉發行為的變化，其含義為滿足謂詞δ的數據包最初轉發到端口from，在規則更新后將轉發到端口to；為每個規則定義hit和port域，其中，規則r的hit域r.hit定義為：

而規則r的port域r.port即規則的動作域r.action所對應的元素端口；

步驟2.2.2、通過從r.match中減去高優先級規則的匹配域來計算命中域r.hit，并通過分析r.hit如何覆蓋不同端口的低優先級規則來找出所有發生變化的轉發行為，得到轉發行為變化集合C；

步驟2.3、更新謂詞：以轉發行為變化集合為輸入，計算移動的謂詞集合D。