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

有效

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

本發(fā)明公開了一種對計算機網絡數據平面進行增量驗證的方法與系統(tǒng)，驗證方法包括以下步驟：步驟1:根據數據平面設備配置構造PPM模型；步驟2:獲取數據平面狀態(tài)更新，并將獲取的更新轉化為增量更新規(guī)則，然后對每一條更新規(guī)則更新PPM模型，得到每一次更新的移動的謂詞集合；步驟3:根據更新后的PPM模型拓撲與更新后移動的謂詞集構造增量轉發(fā)圖；步驟4:在增量轉發(fā)圖上驗證網絡正確性。對計算機網絡數據平面進行增量驗證的系統(tǒng)根據此方法的各個步驟設置處理系統(tǒng)和處理單元，并對系統(tǒng)各部分按照上述方法步驟邏輯相連，使之能對數據平面進行增量驗證。

技術領域

本發(fā)明屬于網絡驗證技術領域，具體涉及一種對計算機網絡數據平面進行增量驗證的方法與系統(tǒng)。

背景技術

計算機網絡常常由于人為錯誤配置、軟件漏洞、硬件故障而產生故障。傳統(tǒng)的人工故障排查方法是對網絡設備的靜態(tài)配置進行核對，只能在網絡發(fā)生故障后尋找故障發(fā)生的原因并進行解決。由于人工排查期間網絡仍無法正常工作，網絡癱瘓可達數小時。

網絡驗證是近年提出的，通過對網絡正確性進行形式化驗證來防止網絡故障發(fā)生的一類方法。網絡驗證分為控制平面驗證和數據平面驗證，控制平面驗證目的為檢測協(xié)議錯誤配置，而數據平面的檢測則是對更接近于真實網絡轉發(fā)行為的數據平面狀態(tài)進行驗證，可覆蓋更加廣泛的網絡故障問題，包括軟件漏洞和硬件故障等。

現(xiàn)有數據平面驗證方法實現(xiàn)了毫秒級的驗證速度，這使得網絡管理員能夠對數據平面的實時更新進行持續(xù)驗證。為了達到毫秒級的驗證速度，實時數據平面驗證方法通常將數據包劃分為等價類(Equivalence Class,EC)，并維護這些EC的轉發(fā)行為模型。數據平面更新時，他們會增量更新模型，并驗證更新后模型的網絡正確性，例如是否存在環(huán)路和黑洞。

VeriFlow與Delta-net是現(xiàn)有數據平面驗證方法的代表技術，都能根據IP前綴劃分EC。其中，VeriFlow以前綴加掩碼的形式表示每個連續(xù)的IP段，利用Trie樹存儲所有的IP前綴。 Trie樹的每個節(jié)點擁有0，1及通配符*三個分支，每個葉子節(jié)點對應著匹配路徑上的IP前綴，表示一個EC。而Delta-net以區(qū)間形式表示每個連續(xù)的IP段，每個區(qū)間表示一個EC。

最新的實時網絡驗證工具雖然已達到了對每次更新在亞毫秒級的驗證速度，但這種速度大多只能在僅含IP轉發(fā)的設備中實現(xiàn)。對于由IP轉發(fā)以外的各種功能組成的實際網絡設備，這些實時驗證工具存在以下兩個缺陷：

首先，網絡的建模能力不足?，F(xiàn)有技術大多只關注IP層面轉發(fā)行為，而真實網絡設備具有不限于IP轉發(fā)的多種功能，例如基于訪問控制列表(ACL)對數據包進行過濾，基于網絡地址轉換(NAT)技術對IP地址進行轉換等。不同廠商設備的具體處理邏輯也有所不同。Veriflow 與Delta-net只關注IP包的轉發(fā)行為，NetPlumber和AP Verifier只能對特定的功能進行處理，皆不符合復雜多變的實際網絡環(huán)境。

其次，驗證速度和可擴展性不足?，F(xiàn)有技術的EC劃分方法大多僅針對目的IP地址這一單一的數據包匹配模式，在面對真實網絡中的五元組(目的IP地址、源IP地址、目的端口、源端口、協(xié)議號)匹配模式時，這些技術所劃分的EC數量將會爆炸式增長，嚴重影響網絡驗證的速度。因此，現(xiàn)有驗證方法不能適用于真實的大規(guī)模網絡環(huán)境。

發(fā)明內容

本發(fā)明提供了一種對計算機網絡數據平面進行增量驗證的方法與系統(tǒng)，通過端口謂詞映射模型來表示網絡的轉發(fā)行為，并基于二元決策圖，提出了增量維護最小數目等價類的方法。

為達到上述目的，本發(fā)明一種對計算機網絡數據平面進行增量驗證方法，包括步驟以下步驟：

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