計算機網絡通信協議驗證技術的研究

彭 勃

?

計算機網絡通信協議驗證技術的研究

彭 勃

北京聯海信息系統有限公司，北京 100053

協議設計、開發的復雜性的增加，導致了協議工程技術的出現。針對協議工程活動中的協議驗證與分析階段，闡述了驗證技術的目的與方法，分析了當今常用的協議模型技術，重點介紹了基于Petri網、FMS，以及時序邏輯TL模型的協議驗證技術。

計算機網絡；協議；協議工程；協議驗證；Petri網

通信協議（communication protocol）是一組實體在執行某項任務中相互通信行為的規則和格式（語法和語義）[1]，它是數據通訊、計算機網絡、多機系統等分布式系統的靈魂。隨著網絡與分布式系統的迅速發展，通信協議的形式化技術，其中包括一系列形式化理論、模型及實現方法已獲得了長足的進步。所謂協議的形式化技術是指協議及服務規范的形式描述、設計驗證、實現驗證和一致性測試。在這些形式化技術中，形式描述與驗證技術是整個協議設計與實現的基礎，對協議實現的正確性、完全性和復雜度有至關重要的影響。

1 計算機網絡協議的定義及特性

1.1 網絡協議定義

網絡協議是指在計算機與計算機之間進行通信必須遵循的一些事先約定好的規則。網絡協議必須遵循標準化的體系結構，目前主要有ISO的標準和TCP/IP協議組標準，通信涉及的所有部分必須認同一套用于信息交換的規則。

1.2 網絡協議特性

（1）活動性（liveness）：協議的活動性體現在終止性和進展性兩方面，或者說，如果協議有終止性和進展性，它就具有活動性。如果協議的某個狀態從初態不可達，則表明協議有錯誤。

（2）安全性（Safety）：指協議運行時錯誤的行動、錯誤的條件等，導致兩種現象發生：死鎖（deadlock）和活鎖（livelock）。最典型的死鎖是協議中各實體都處于這樣的一種等待狀態，即只有在“某一事件”發生后才做進一步的動作，但在該狀態下，這個“某一事件”卻不可能發生。死鎖發生時，協議所處的狀態稱為死鎖狀態，死鎖的另一種形式是協議處于無限的死循環中，而沒有別的事件可使協議從這一循環中解脫出來。例如，協議無限制地執行超時重發操作，但總是收不到對方的確認信息。有人將這種形式的死鎖稱為活鎖，表明整個協議的狀態還是變化的，不過不能脫離這種死循環狀態而已。

（3）有界性、完整性及可恢復性或同步性：檢驗協議的某些成分或參數的容量（例如通道容量、窗口容量）是否有界。檢驗協議是否缺少應有的處理，以及有無非期待的接收（即錯收）等。這是當出現差錯后，協議能否在有限的步驟內返回到正常狀態（包括初態）下執行。

2 計算機網絡協議的分類

2.1 局域網協議

局域網協議定義了在多種局域網介質上的通信。目前，常用的局域網主要有NetBEUI、IPX/SPX以及其兼容協議和TCP/IP三類。

2.2 廣域網協議

廣域網協議是在OSI參考模型的最下面三層操作。定義了在不同的廣域網介質上的通信。主要用于廣域網的通信協議比較多，如：高級數據鏈路控制協議、點到點協議（PPP）、數字數據網（DDN）、綜合業務數字網（ISDN）、數字用戶線（XDSL）等協議。

2.3 路由選擇協議

路由選擇協議是網絡層協議，它負責路徑的選擇和交換。路由選擇協議還分為內部路由協議（自治系統內部交換路由信息的路由協議）和外部路由協議（為連接兩個或多個自治系統的路由協議）。

3 協議驗證技術的目的與方法

對協議本身的邏輯正確性進行校驗的過程稱之為驗證。協議驗證有兩種途徑：協議分析和協議綜合，通常所說的協議驗證指的是前者。協議分析的目的是：對已設計的協議進行分析和校驗 這些已設計的協議大都是采用非形式化設計（方法產生的）。協議的正確性驗證試圖在協議開發的前期最大限度地檢測和糾正協議錯誤和缺陷，包括死鎖、活鎖、不可執行的行動、協議外部性能不符合服務要求等。協議驗證技術多種多樣但可以分為3類：可達性分析是最常用的技術，它包括狀態窮舉、狀態隨機枚舉、狀態概率枚舉等方法；邏輯證明試圖用推理演算方法嚴密的證明協議各種性質，采用的推理演算技術主要來自與時序邏輯、謂詞邏輯、代數演算等數學領域；第三類驗證技術是模擬。協議綜合將協議設計和協議驗證緊密結合起來，也可以認為是一類驗證技術。

4 網絡協議中Ping程序及其應用

這個程序用來檢測一幀數據從當前主機傳送到目的主機所需要的時間。當網絡運行中出現故障時，采用這個實用程序來預測故障和確定故障源是非常有效的。如果執行ping不成功，則可以預測故障出現在以下幾個方面：網線是否連通，網絡適配器是否正確，IP地址是否可用等；如果執行ping成功而網絡仍然不能使用，那么問題很可能出現在網絡系統的軟件配置方面，ping成功只能保證當前主機與目的主機存在一條連通的物理路徑，它還提供了許多參數，如-t使用當前主機不斷向目的主機發送數據，直到使用ctel-c中斷；-n可以自己確定想目的主機發送數據偵數等等。

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

有限狀態機FSM是最為重要的一種形式描述技術，它是很多形式化方法的基礎。它直觀性強，可實現與其他形式方法的組合和轉換，且易于自動實現[2]，因而在FDT中占有重要的地位。有限狀態機最常用的技術是可達性分析技術。可達性分析技術試圖產生和檢查協議所有或部分可達狀態。一般來說，對于每次發生的轉變，可通過使用系統全局狀態來決定特性，像是否表示一個死鎖狀態，所有實體是否在當前狀態能接收發給它的所有報文等。基于FSM描述的協議驗證可通過構造可達樹來實現。可達樹的根為系統的初始狀態[3]。從初始狀態出發，列舉出全部可能的轉移，每一個轉移將產生一個新的狀態空間。在此葉結點的基礎上，不斷生長新的葉節點，直到沒有新的葉節點為止。可達樹上各節點分別表示某一給定時刻的全局狀態矩陣（GMS），它動態地反映了兩個或多個協議實體或進程的交互活動。FSM由于簡單、直觀而得到廣泛應用，但不利于協議驗證的實現，不易于描述復雜的系統。

6 基于時序邏輯的協議描述與驗證

從邏輯角度來說，時序邏輯TL（Tempoeal Longic）是模態邏輯的擴充，以狀態為可能世界，以狀態的演變次序關系為可能世界間的可到達關系。時序邏輯的種類很多，隨時間結構不同，算子的選擇也有差異。時序邏輯應用較為成熟，并且數學抽象能力很強，它側重于通過定義系統外部可見的行為事件來描述系統，即直接描述系統的輸入/輸出行為，而不關心協議實體的內部變化，比FSM、Petri網更易于刻劃協議的活動性，因而有利于對協議的各種性質進行分析驗證。

7 其他協議分析技術

除前面介紹的協議形式化技術以外，由R.Miler開拓性創建的通訊進程演算CCS（the SCalcula for Communicating System），以及C.A.R.Hoare在基礎上創立的通訊順序進程CSP（the Communing Sequential processes）也在協議工程中得到了重要的應用。

[1]張小亮，涂勇策，馬恒太，等.一種適用于衛星通信網絡的端到端認證協議[J].計算機研究與發展，2013，50（3）：540-547.

[2]朱雪寒，夏卓群，劉品超，等.基于網絡編碼的ECC驗證方案在WSN中的研究[J].計算機技術與發展，2011，21（2）：173-176.

[3]張沖，劉涌，楊海波，等.移動社交網絡實時通信機制的研究[J].計算機系統應用，2014，23（2）：205-208.

Computer Network Communication Protocol Verification Technology

Peng Bo

Beijing MINUSTAH Information System Co., Ltd.,Beijing 100053

Protocol design，complexity increases development，led to the emergence of protocol engineering technologies for protocol engineering activities protocol verification and analysis phases，on the purposes and methods of verification technology， analyzes commonly used today protocol model technology，focusing on the verification protocol based on Petri nets，FMS，and temporal logic TL model technology.

computer network；protocol engineering；protocol validation；Petri nets

TP393.04

A

1009-6434(2016)07-0108-02