計(jì)算機(jī)網(wǎng)絡(luò)通信協(xié)議驗(yàn)證技術(shù)的有機(jī)運(yùn)用

王文韜

（湖北科技學(xué)院，湖北 咸寧 437100）

1 計(jì)算機(jī)網(wǎng)絡(luò)通信協(xié)議的相關(guān)概述

1.1 計(jì)算機(jī)網(wǎng)絡(luò)協(xié)議的定義

計(jì)算機(jī)網(wǎng)絡(luò)協(xié)議的本質(zhì)就是計(jì)算機(jī)必須遵從的通信規(guī)則。網(wǎng)絡(luò)協(xié)議在制定的過程中必須要嚴(yán)格按照標(biāo)準(zhǔn)的體系結(jié)構(gòu)執(zhí)行，在科學(xué)技術(shù)不斷的發(fā)展之中網(wǎng)絡(luò)通信標(biāo)準(zhǔn)體系也不斷更新和完善，如今最為常用的標(biāo)準(zhǔn)為TCP/IP協(xié)議組以及ISO兩種標(biāo)準(zhǔn)。通信技術(shù)的順利實(shí)施就必須要保障其中所有的內(nèi)容完全遵從于統(tǒng)一的信息交換準(zhǔn)則[1]。

1.2 計(jì)算機(jī)網(wǎng)絡(luò)協(xié)議的特性

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

2 計(jì)算機(jī)網(wǎng)絡(luò)通信協(xié)議的主要類型

2.1 局域網(wǎng)使用的通信協(xié)議

TCP/IP作為互聯(lián)網(wǎng)最基礎(chǔ)的協(xié)議，是局域網(wǎng)運(yùn)用最廣泛的通信協(xié)議，其具備高度的靈活性，可以實(shí)現(xiàn)眾多服務(wù)器以及工作站的連接。TCP/IP協(xié)議經(jīng)過其帶有的IP地址來對(duì)網(wǎng)絡(luò)中的詳細(xì)位置以及身份給予高效識(shí)別[2]。IP地址主要包含如下要素，即節(jié)點(diǎn)和網(wǎng)絡(luò)ID。在多網(wǎng)段的背景之下能夠擴(kuò)展網(wǎng)絡(luò)ID，通過子網(wǎng)掩碼管理子網(wǎng)。在連接異種網(wǎng)絡(luò)時(shí)，人們普遍以一個(gè)翻譯者的身份設(shè)置網(wǎng)關(guān)達(dá)到精確翻譯通信協(xié)議的目的，實(shí)現(xiàn)網(wǎng)絡(luò)相互通信的效果。

2.2 廣域網(wǎng)使用的通信協(xié)議

廣域網(wǎng)的通信協(xié)議存在多種多樣的形式，包含點(diǎn)到點(diǎn)協(xié)議等。廣域網(wǎng)協(xié)議從本質(zhì)上講就是對(duì)不同廣域網(wǎng)介質(zhì)上的通信進(jìn)行了明確的界定。

2.3 路由器選擇協(xié)議

路由器選擇協(xié)議主要工作區(qū)間為網(wǎng)絡(luò)層，其實(shí)現(xiàn)了路徑選擇和交換。路由器選擇協(xié)議主要包含內(nèi)部路由協(xié)議和外部路由協(xié)議兩種，前者是在系統(tǒng)內(nèi)部實(shí)現(xiàn)路由協(xié)議的交換，后者實(shí)現(xiàn)不同自治系統(tǒng)的協(xié)議互換。

3 驗(yàn)證技術(shù)在計(jì)算機(jī)網(wǎng)絡(luò)通信協(xié)議中的主要應(yīng)用

3.1 Ping程序在網(wǎng)絡(luò)協(xié)議中的應(yīng)用

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

3.2 基于有限狀態(tài)自動(dòng)機(jī)模型的協(xié)議驗(yàn)證與分析

形式描述技術(shù)中一個(gè)關(guān)鍵性的形式便是有限狀態(tài)機(jī)FSM，在FDT中扮演了十分重要的角色?？蛇_(dá)性分析技術(shù)是目前有限狀態(tài)機(jī)運(yùn)用最為廣泛的一項(xiàng)技術(shù)[1]。 其力圖對(duì)協(xié)議的可達(dá)狀態(tài)進(jìn)行檢測(cè)?？蛇_(dá)性分析關(guān)鍵性環(huán)節(jié)便是產(chǎn)生和檢查可達(dá)圖，檢測(cè)協(xié)議是否正確，其中包含3個(gè)核心技術(shù)：首先是尋找全部的可達(dá)圖并且建立可達(dá)圖；其次是檢驗(yàn)協(xié)議的正確性；最后是處理狀態(tài)爆炸現(xiàn)象。普遍來看，所有的轉(zhuǎn)變都能夠經(jīng)過運(yùn)用系統(tǒng)全局狀態(tài)達(dá)到明確特性的目的，類似于表明此時(shí)是不是死鎖狀態(tài)，全部的實(shí)體能不能夠接收?qǐng)?bào)文等?；贔SM描述的協(xié)議驗(yàn)證主要是借助于可達(dá)樹來發(fā)揮作用。其中系統(tǒng)的初始狀態(tài)為可達(dá)樹的根。從初始狀態(tài)開始將全部的轉(zhuǎn)移列舉出來，可達(dá)數(shù)的一個(gè)葉節(jié)點(diǎn)便是由這些轉(zhuǎn)移的狀態(tài)空間組成，這個(gè)過程也被叫做一次擾動(dòng)過程。以這些葉節(jié)點(diǎn)為中心持續(xù)延伸出新的葉節(jié)點(diǎn)截止到并未有葉節(jié)點(diǎn)產(chǎn)生?？蛇_(dá)樹上各節(jié)點(diǎn)能夠?qū)崟r(shí)展現(xiàn)出兩個(gè)及以上實(shí)體協(xié)議的互動(dòng)情況。FSM因?yàn)槿菀撞僮鞅容^直接的狀態(tài)被大幅度的運(yùn)用到實(shí)際中，但是其在實(shí)現(xiàn)協(xié)議驗(yàn)證方面存在諸多不足，一般不適用于復(fù)雜的系統(tǒng)。

3.3 基于時(shí)序邏輯的協(xié)議驗(yàn)證與分析

3.3.1 基于模態(tài)邏輯的研究

這種形式的邏輯目前在市場(chǎng)上得到普遍認(rèn)可的便是在20世紀(jì)末期由Burrows M、Abadi M等人發(fā)現(xiàn)的BAN邏輯。BAN邏輯在協(xié)議初始階段便明確了系統(tǒng)之中所有相關(guān)的知識(shí)和信任，經(jīng)過發(fā)送和接收信息來獲取新的知識(shí)，在推導(dǎo)規(guī)則的指引下獲得目標(biāo)信任和知識(shí)[2]。假如最后獲得的語句集不存在目標(biāo)信任和知識(shí)語句時(shí)，那么這個(gè)協(xié)議極易產(chǎn)生安全危機(jī)。由于BAN存在的安全缺陷，后人在此基礎(chǔ)上對(duì)其進(jìn)行了改進(jìn)，獲得了“類BAN邏輯”成果，并且發(fā)布在IEEE軟件工程雜志之上。在此之中，GNY90、AT91邏輯作為其中的一種形式得到了人們的普遍關(guān)注。GNY90對(duì)原始的BAN邏輯的范圍進(jìn)行了延伸，具體界定了消息認(rèn)定的規(guī)則，比原始的BAN更加的精細(xì)化并且覆蓋的范圍也越來越廣。然而其所要遵循的規(guī)則高達(dá)50個(gè)，制約了其實(shí)際應(yīng)用范圍和空間。AT91邏輯在計(jì)算模式以及形式語言方面具備突出性優(yōu)勢(shì)，獲得了大眾的認(rèn)可。在AT91的框架基礎(chǔ)上，20世紀(jì)末期類BAN的邏輯實(shí)現(xiàn)了統(tǒng)一，也就是形成了SVO邏輯。MB93邏輯因?yàn)榧尤肓思细拍畈⑶乙驗(yàn)楦袷交膶憛f(xié)議方法的獨(dú)特方式引發(fā)了人們的關(guān)注。但是本段所述的邏輯形式都不能夠滿足電子商務(wù)協(xié)議的需求，這主要是因?yàn)樾拍钸壿嫳仨氁趪?yán)格的證明之下方能夠執(zhí)行造成的。在這種情況下，Kailar發(fā)現(xiàn)了一種新的形式化分析方法，用來分析電子商務(wù)中的可追究性，即Kailar邏輯。然而Kailar邏輯在實(shí)際中存在不能夠判斷公平性等不足。

3.3.2 基于代數(shù)理論的協(xié)議分析

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

3.3.3 規(guī)約證明

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

4 結(jié) 論

為保障網(wǎng)絡(luò)通信協(xié)議的可靠性，對(duì)其實(shí)施有效的驗(yàn)證顯得尤為重要，本文介紹了能夠在實(shí)際中得到有效運(yùn)用的驗(yàn)證方式，在實(shí)際中可以根據(jù)具體情況進(jìn)行選擇。唯有如此方能夠確保網(wǎng)絡(luò)通信協(xié)議的正常運(yùn)作，推動(dòng)整個(gè)計(jì)算機(jī)系統(tǒng)高效工作。