計算機網絡通信協議驗證技術的有機運用

王文韜

（湖北科技學院，湖北 咸寧 437100）

1 計算機網絡通信協議的相關概述

1.1 計算機網絡協議的定義

計算機網絡協議的本質就是計算機必須遵從的通信規則。網絡協議在制定的過程中必須要嚴格按照標準的體系結構執行，在科學技術不斷的發展之中網絡通信標準體系也不斷更新和完善，如今最為常用的標準為TCP/IP協議組以及ISO兩種標準。通信技術的順利實施就必須要保障其中所有的內容完全遵從于統一的信息交換準則[1]。

1.2 計算機網絡協議的特性

計算機網絡協議主要包含如下特性。（1）活動性，在實際中通常表現為進展性和終止性，假如網絡協議不具備這兩種特性，那么他的活動性也是不存在的。（2）安全性。安全性主要是指協議在執行時發生活鎖和死鎖等安全問題。例如，出現死鎖現象時，網絡協議所有的實體都呈現等待狀態，唯有發生“某一事件”之后方能夠執行下一環節的操作。但是，在現實之中便是當網絡協議處于這種等待情況時，是不可能發生“某一事件”的，也就是說協議處于死鎖狀態之后便不可能通過某一事件解脫。這就類似于網絡協議一直在接受一個重復的循環命令，然而其又沒有辦法接受相關的確認信息，因此一直處于一個固定的狀態。（3）有界性、完整性以及同步性。工作人員要重點檢測網絡協議中的成分和參數，還要針對協議之中有無未解決的問題以及非期待的命令等進行檢驗和檢測。在此期間，假如協議出現無錯的情況，是否可以保障協議重新開始并且順利運行下去，這些都是需要重點觀察的部分。

2 計算機網絡通信協議的主要類型

2.1 局域網使用的通信協議

TCP/IP作為互聯網最基礎的協議，是局域網運用最廣泛的通信協議，其具備高度的靈活性，可以實現眾多服務器以及工作站的連接。TCP/IP協議經過其帶有的IP地址來對網絡中的詳細位置以及身份給予高效識別[2]。IP地址主要包含如下要素，即節點和網絡ID。在多網段的背景之下能夠擴展網絡ID，通過子網掩碼管理子網。在連接異種網絡時，人們普遍以一個翻譯者的身份設置網關達到精確翻譯通信協議的目的，實現網絡相互通信的效果。

2.2 廣域網使用的通信協議

廣域網的通信協議存在多種多樣的形式，包含點到點協議等。廣域網協議從本質上講就是對不同廣域網介質上的通信進行了明確的界定。

2.3 路由器選擇協議

路由器選擇協議主要工作區間為網絡層，其實現了路徑選擇和交換。路由器選擇協議主要包含內部路由協議和外部路由協議兩種，前者是在系統內部實現路由協議的交換，后者實現不同自治系統的協議互換。

3 驗證技術在計算機網絡通信協議中的主要應用

3.1 Ping程序在網絡協議中的應用

Ping程序的作用是實施對一幀數據的檢測工作，即計算機進行數據轉換所需要的時間。假如計算機網絡在正常運行時突然產生問題，ping程序能夠幫助工作人員迅速辨別問題產生的原因。Ping程序的成功執行只是為主機與目標主機的連接提供一條成物理路徑并且給予一些相關的參數。例如，-n可以依賴于自身的力量明確地向目標主機發送數據幀數。

3.2 基于有限狀態自動機模型的協議驗證與分析

形式描述技術中一個關鍵性的形式便是有限狀態機FSM，在FDT中扮演了十分重要的角色。可達性分析技術是目前有限狀態機運用最為廣泛的一項技術[1]。 其力圖對協議的可達狀態進行檢測。可達性分析關鍵性環節便是產生和檢查可達圖，檢測協議是否正確，其中包含3個核心技術：首先是尋找全部的可達圖并且建立可達圖；其次是檢驗協議的正確性；最后是處理狀態爆炸現象。普遍來看，所有的轉變都能夠經過運用系統全局狀態達到明確特性的目的，類似于表明此時是不是死鎖狀態，全部的實體能不能夠接收報文等。基于FSM描述的協議驗證主要是借助于可達樹來發揮作用。其中系統的初始狀態為可達樹的根。從初始狀態開始將全部的轉移列舉出來，可達數的一個葉節點便是由這些轉移的狀態空間組成，這個過程也被叫做一次擾動過程。以這些葉節點為中心持續延伸出新的葉節點截止到并未有葉節點產生。可達樹上各節點能夠實時展現出兩個及以上實體協議的互動情況。FSM因為容易操作比較直接的狀態被大幅度的運用到實際中，但是其在實現協議驗證方面存在諸多不足，一般不適用于復雜的系統。

3.3 基于時序邏輯的協議驗證與分析

3.3.1 基于模態邏輯的研究

這種形式的邏輯目前在市場上得到普遍認可的便是在20世紀末期由Burrows M、Abadi M等人發現的BAN邏輯。BAN邏輯在協議初始階段便明確了系統之中所有相關的知識和信任，經過發送和接收信息來獲取新的知識，在推導規則的指引下獲得目標信任和知識[2]。假如最后獲得的語句集不存在目標信任和知識語句時，那么這個協議極易產生安全危機。由于BAN存在的安全缺陷，后人在此基礎上對其進行了改進，獲得了“類BAN邏輯”成果，并且發布在IEEE軟件工程雜志之上。在此之中，GNY90、AT91邏輯作為其中的一種形式得到了人們的普遍關注。GNY90對原始的BAN邏輯的范圍進行了延伸，具體界定了消息認定的規則，比原始的BAN更加的精細化并且覆蓋的范圍也越來越廣。然而其所要遵循的規則高達50個，制約了其實際應用范圍和空間。AT91邏輯在計算模式以及形式語言方面具備突出性優勢，獲得了大眾的認可。在AT91的框架基礎上，20世紀末期類BAN的邏輯實現了統一，也就是形成了SVO邏輯。MB93邏輯因為加入了集合概念并且因為格式化改寫協議方法的獨特方式引發了人們的關注。但是本段所述的邏輯形式都不能夠滿足電子商務協議的需求，這主要是因為信念邏輯必須要在嚴格的證明之下方能夠執行造成的。在這種情況下，Kailar發現了一種新的形式化分析方法，用來分析電子商務中的可追究性，即Kailar邏輯。然而Kailar邏輯在實際中存在不能夠判斷公平性等不足。

3.3.2 基于代數理論的協議分析

該方式具備本文分析方式所具有的優勢，如精密度高以及具備強大的推理功能等。20世紀90年代初期Meadows等人便運用該方式對NRL分析器的推理模型進行延伸，但是并未取得突出性實效。近期以來，該方面的研究得到了業界的廣泛關注并且采取了一系列的實際活動，產生了FDR模型檢測器。Bruno Dutertre經過長期的研究發明了PVS驗證系統。此外，基于代數理論的協議分析還包括Spi演算分析。但是這種方式在存在一定的安全缺陷，在實際應用中存在一定的局限性。

3.3.3 規約證明

規約證明是一種最新被提出的新型的技術，最早被Kemmerer提出。該方式可以實現手動以及自動的自由切換，但是自動證明較之前者還不夠成熟比較復雜，需要更深一步的完善和探索。

4 結 論

為保障網絡通信協議的可靠性，對其實施有效的驗證顯得尤為重要，本文介紹了能夠在實際中得到有效運用的驗證方式，在實際中可以根據具體情況進行選擇。唯有如此方能夠確保網絡通信協議的正常運作，推動整個計算機系統高效工作。