ＷＴＰ協(xié)議的ＳＰＩＮ模型檢測

摘要：基于模型檢測技術(shù)，使用SPIN對WTP協(xié)議進行了建模和分析.應(yīng)用自動機和Promela對協(xié)議進行建模，利用LTL規(guī)范了協(xié)議需要滿足的安全性，時序性。通過分析發(fā)現(xiàn)了協(xié)議的一個錯誤。

關(guān)鍵詞：WTP協(xié)議；SPIN；模型檢測； Promela

中圖分類號：TP393文獻標識碼：A 文章編號：1009-3044(2008)34-1588-04

Model Checking of WTP Protocol Via SPIN

FENG Jie

(Electronic Science and Information Technology College， Guizhou University， Guiyang 550025， China)

Abstract：This paper deals with a formal verification of WTP， where the model checking approach is applied by SPIN model checker.The Promela model is developed and LTL specifications of secrecy are given. Eventually， some defects has been revealed.

Key words:WTP Protocol; SPIN; model checking; Promela

1 引言

SPIN作為一個有效的軟件系統(tǒng)模型檢測工具，已經(jīng)在分布系統(tǒng)，軟件的形式化驗證，特別是通信協(xié)議和安全協(xié)議上獲得了的成功。SPIN己經(jīng)驗證的協(xié)議有：X. 509認證協(xié)議，距離矢量路由協(xié)議，NS公鑰協(xié)議，Ad Aoc路由協(xié)議。

Gordon[1]基于Petri網(wǎng)的理論，用有色Petri網(wǎng)(CPN)對WTP協(xié)議進行了建模和形式化的分析。他是在無損通道上建立的模型，但在無線應(yīng)用上，信道上數(shù)據(jù)包的丟失是時常發(fā)生的。

在本文中，我對WTPv2[2]協(xié)議方案進行了形式化的驗證。我們用自動機的理論重新形式化了服務(wù)的定義和協(xié)議的規(guī)程，并建立了相應(yīng)的Promela的模型。

2 SPIN對協(xié)議的分析原理

SPIN以Promela為輸入語言，適合于對網(wǎng)絡(luò)協(xié)議設(shè)計中規(guī)格的邏輯一致性進行檢驗。Promela被設(shè)計為可以對協(xié)議模型作出準確的表達。此外，Promela的語義保持了協(xié)議并發(fā)性和不確定性的特征。Promela本質(zhì)上是一種有窮自動機的形式描述語言。

SPIN易于對Promela建立的模型進行仿真和驗證。仿真和驗證是SPIN的兩種工作方式。隨機仿真常被用于仿真協(xié)議的執(zhí)行過程。同時，如果在驗證階段發(fā)現(xiàn)了錯誤，可以由此指導(dǎo)仿真重現(xiàn)相應(yīng)的錯誤軌跡。這樣就能幫助我們找出錯誤的來源。

當(dāng)我們用SPIN進行驗證時，我們就需要解決模型檢測的問題：證明時序邏輯公式φ是在模型M中成立（即證明M│=φ）。當(dāng)我們把φ轉(zhuǎn)化成Buchi自動機Aφ并且模型M轉(zhuǎn)化成自動機AM就相當(dāng)于

證明：

■ (1)

證明過程實際上就是計算(1)式是否為空集。如果(1)式成立，就可認為該協(xié)議滿足這些性質(zhì)，如果(1)式不成立，則說明該協(xié)議可能存在某些性質(zhì)上缺陷或攻擊。使用SPIN 對協(xié)議進行驗證和分析過程如圖1所示。

3 WTP協(xié)議的形式化

由于人們無時無處通信的需求，對無線網(wǎng)絡(luò)移動數(shù)據(jù)服務(wù)的要求也越來越迫切。無線用戶的需求不同于有線用戶的需要，因為移動數(shù)據(jù)服務(wù)受到移動終端以及無線網(wǎng)絡(luò)特點的限制——移動終端本身顯示屏微小，處理能力很低，同時無線網(wǎng)絡(luò)具有高延遲和低帶寬的性質(zhì)。WAP(Wireless Application Protocol)定義了一個體系結(jié)構(gòu)就是針對無線環(huán)境下的傳輸，通信等問題。WTP是WAP體系結(jié)構(gòu)中的事務(wù)層（Transaction Layer)。它定義了一個協(xié)議實現(xiàn)在兩個實體之間的請求/響應(yīng)事務(wù)，作為瀏覽應(yīng)用的一個組件。

3.1 協(xié)議的設(shè)計及內(nèi)容

我們按照網(wǎng)絡(luò)協(xié)議的5個基本要素來對WTP協(xié)議進行說明

3.1.1 協(xié)議環(huán)境的假定

在層次化的WAP體系結(jié)構(gòu)中，事務(wù)層位于傳輸層的上層。傳輸層為事務(wù)層提供服務(wù)。然而，在WAP體系中傳輸層采用的是無連接的無線數(shù)據(jù)報協(xié)議（WDP）(對應(yīng)于TCP/IP中的UDP)。所以，我們假定在事務(wù)層兩個對等的協(xié)議實體（TR-PES）之間消息交換可能會丟失、重排，重復(fù)。

3.1.2 服務(wù)定義

在WTP中，CLASS 2的事務(wù)層服務(wù)被定義為向上層的會話層用戶（TR-Users）提供可靠的事務(wù)服務(wù)。這種可靠性是通過一個可靠的請求（Invoke）消息（事務(wù)的發(fā)起者Initator發(fā)送）就會響應(yīng)一個可靠的結(jié)果（result）消息（響應(yīng)者Responder發(fā)送）的機制實現(xiàn)。TR-Service通過服務(wù)原語和它們的序列抽象定義。

這里我們只討論涉及到模型的三個原語：Invoke，Result，Abort。每個原語都可以作為四種原語類型(Request簡寫為Req，Indication簡寫為Ind，Response簡寫為Res，Confirm簡寫為Cnf)的前綴，從而形成“提交-交付”對。例如Invoke.Req和Invoke.Cnf。

3.1.3 協(xié)議詞匯

協(xié)議詞匯中我們需要用到有四種協(xié)議數(shù)據(jù)單元：Inovoke，Result，Ack，，Abort。它們分別對應(yīng)于響應(yīng)的服務(wù)原語。

3.1.4 報文格式

每一個報文由兩部分組成：控制字段和數(shù)據(jù)字段。我們主要集中在控制字段中的幾位。它們是RID，表明是一個重傳PDU。U/P位指示Ack-Type的參數(shù)開關(guān)。位TIDve/TIDok用來驗證事務(wù)標識。

3.1.5 協(xié)議規(guī)程

協(xié)議規(guī)程保證了消息交換的一致性。在WTP的設(shè)計方案中，協(xié)議規(guī)程是由一組狀態(tài)表所規(guī)范。它定義了對等協(xié)議實體之間當(dāng)協(xié)議實體有輸入事件發(fā)生時如何改變它們的狀態(tài)。表2給出了一個示例，每個狀態(tài)都要參考一個四元組（Event，Condition，Action，NextState）。當(dāng)事件發(fā)生，條件滿足時，行為集就會發(fā)生，并且更新狀態(tài)信息。

3.2 協(xié)議的Promela模型和自動機模型

我們的系統(tǒng)建模主要是基于以下假設(shè)。這些假設(shè)是：僅僅是涉及一個事務(wù)發(fā)起者和一個事務(wù)響應(yīng)者的單個事務(wù)。在對等協(xié)議實體間的信息交換緩存在異步通道中，這個通道是允許重排和丟包。

我們基于TR-Protocol和TR-Service構(gòu)建了兩個Promela模型。兩個模型共享相同的架構(gòu)。（圖2）這個架構(gòu)的核心是由兩個進程組成，一個是發(fā)起者進程，另一個是響應(yīng)者進程。兩個進程通過異步通道共享控制變量。

圖2中每個進程被定義為一個自動機Ai=(Si，s0i，∑i， δi，F(xiàn)i)。在TR-Protocol模型中，i=PI是指發(fā)起進程(Initiator)，i=PR是指響應(yīng)進程。每個自動機由下面5個組件組成：

1) 狀態(tài)集Si:Vi→ Di映射變量集Vi到相應(yīng)的定義域Di。

Vi=(Globali，Locali)是包含全局變量和本地變量的元組。

Globali=(channels，toggles)其中全局變量集也是一個元組，由通道變量集和原語觸發(fā)集組成。兩個擴展變量通道模擬了進程間的異步通信。這兩個通道分別是I2R和R2I。以下給出了I2R通道的Promela語言的描述：

mtype = {INVOKE， ACK， RESULT， ABORT};

chan I2R = [4] of {mtype， bit， bit};

Toggles=(Primitive_tgls，Dlock)是一個元組。他包含的變量常用來規(guī)范協(xié)議的正確性需求。Primitive_tgls是一個位變量，用來記錄服務(wù)原語的發(fā)生。例如，iind_tgl的值為1，那就表示Invoke.ind原語已經(jīng)提交。而Dlock用來指示進程執(zhí)行中是否發(fā)生死鎖。

2) 初始狀態(tài)S0i

3) ∑i={a|a=L(s)，s∈Si}，定義為狀態(tài)轉(zhuǎn)換的哨崗（條件）。

4) 轉(zhuǎn)換(變遷)關(guān)系δi:Si×∑i→2Si定義了進程執(zhí)行的控制流。Si(s，a)給出了狀態(tài)下所有可能的后繼。通常|δi(s，a)|≥1時，下個狀態(tài)就是不可確定的。

5) Fi包含了所有可能的終態(tài)。(?坌SFi∈Fi)SFi(Locali)=s0i(Locali)，在一個完整的轉(zhuǎn)換，在清除了所有的狀態(tài)信息后對等的協(xié)議實體最終回到它的初始狀態(tài)。

然后TR-Protocol的基本行為被模擬為自動集AM，它是發(fā)起進程自動機API和響應(yīng)進程自動機APR的交叉積。AM=API×APR。同理我們用相同的方法也會得TR-Service的自動機模型。

在從有窮自動機(FSA)定義轉(zhuǎn)換到Promela模型前，我們需要創(chuàng)建條件表作為一個中間步驟來指定狀態(tài)轉(zhuǎn)換和相應(yīng)的哨崗。條件表是用集合理論對WTP協(xié)議方案的狀態(tài)表進行形式化得到的。

如表3，第一個條目定義的哨崗就是:a=(PE_state=TIDok_Wait)∧(Ack∈I2R)∧(TIDok=1)

其中(ACK∈I2R)∧(TIDok=1)在用Promela建模時，可以用通道輪詢操作來模擬（I2R∪[ACK，RID，1]）。當(dāng)哨崗(條件)滿足后，Action一欄就計算變量的新值，例如當(dāng)前狀態(tài)的后繼狀態(tài)。如表2當(dāng)哨崗條件成立后，變量會進行如下更新。從輸入通道中接收消息，并從通道中清除掉，如I2R-{ACK} 。同時，由于我們假設(shè)了通道允許消息重排，所以我們在用Promela建模時，我們使用Promela語言中的隨機接收操作。I2R∪ACK(RID，1)

向輸出通道中發(fā)送信息，如I2R∪{INVOKE}，對應(yīng)的Promela模型是I2R!INVOKE(1，0)。

iind_tgl+1表明提交了INOVKE.ind服務(wù)原語。

同狀態(tài)轉(zhuǎn)換有關(guān)的每個條件表中的條目，實際上定義了一個在臨界區(qū)域當(dāng)中更新共享變量。為了確保在Promela模型中臨界區(qū)域的原子屬性，我們在每個哨崗中都用一個全局控制變量Aflag。

inline Entry i( ) {

atomic {

if (Guard == TRUE AND Aflag == 1) {

Aflag = 0;

Actions of updating variables;

Aflag = 1;

}

}

}

這里我們給出了發(fā)起者進程的Promela模型的偽碼。

proctype Initiator ( ) {

progress:

do

:: Entry 1 ( ) // 在表4中以定義

:: ...

:: Entry n ( )

:: atomic {

if (?nal state conditions == TRUE) {

Indicate the transaction completed;

break

}

}

:: atomic {

if (timeout) {

DLock = 1;

break

}

}

od

}

最后，我們用一個獨立的進程 模擬通道存在數(shù)據(jù)包丟失的假設(shè)

proctype Stealing( ) {

end: do

:: I2R?? ， ， ，

:: R2I?? ， ， ，

od

}

3.3 協(xié)議性質(zhì)LTL描述

對WTP協(xié)議設(shè)計規(guī)范，我們分類了三種屬性對協(xié)議描述：安全性PS，活性PL，時序特征PT。

3.3.1 安全性

安全性通常來說就是指沒有“壞事”發(fā)生。正式的，給出一個協(xié)議的自動機 AM，(?坌ps∈PS)(?坌s∈SM)ps∈L(s)，例如：每一個安全屬性 在所有狀態(tài)下為真。

從變量的一致性考慮，安全性要求：協(xié)議是有邊界約束的。每個變量不能溢出他的取值范圍假如SM:VM->DM，因此(?坌v∈VM)(?坌s∈SM)s(v)∈DM。例如我們考慮本地的重傳計數(shù)器PE_data.RCR，它的最大取指是RCR_MAX。所以我們的安全屬性的LTL公式為：ps1=(PE_data.RCR?燮RCR_MAX)

原子性，全局控制變量Aflag應(yīng)該總是安全的。ps2=(Aflag==0）從進程的執(zhí)行考慮，安全性要求：無死鎖ps3=(DLock==0）

上面屬性的安全性，我們用一個Promela的進程來實現(xiàn)(見圖)。一個Promela的斷言語句assert( )常被用來報告psi是否違規(guī)然后定位一個錯誤的狀態(tài)。

active proctype monitor() {

end: atomic {

if

:: !BOUNDNESS -> assert(BOUNDNESS);

:: !Aflag -> assert(Aflag);

:: (DLock_R || DLock_I) -> assert(!DLock_R !DLock_I);

fi

}

}

3.3.2 活性

活性通常是指“某些好事發(fā)生”。既是說，指定的條件或狀態(tài)最終會到達。從進程執(zhí)行來考慮，活性是指:協(xié)議不能包含不可達狀態(tài)。當(dāng)用SPIN驗證Promela模型時，如果協(xié)議含有不可達狀態(tài)，SPIN將會報告“unrearched states”。

3.3.3 時序行為

時序行為主要是處理服務(wù)原語間的序列。他們也常用來驗證由TR-Protocol生成的服務(wù)語言是否是TR-Service生成的子集，從而判斷TR-Protocol忠實于TR-Service的服務(wù)定義。

PTi=[]((<>ICNF_tgl)=>■ICNF_tglUires_tgl))（2）

這里我們給出其中的一個將被驗證的時序需求，n其中，[](always)表示一直，<>(future or eventually)表示未來的某個狀態(tài)點或最終，U(Until)表示直到。這個公式規(guī)范了Invoke.res原語（即觸發(fā)位Ires.tgl=1)的發(fā)生是Invoke.cnf原語（位ICNF_tgl=1）發(fā)生的先決條件。

4 檢驗結(jié)果分析

我們給出了驗證TR-Service模型和TR-Protocol模型的結(jié)果，重點是給出了最初協(xié)議設(shè)計方案中的一些錯誤。

驗證TR-Service模型的目的是為了證明我們我們建立的Promela模型是符合WTP協(xié)議設(shè)計方案中定義服務(wù)語言（需求）。經(jīng)驗證所有屬性都是滿足TR-Service的Promela模型。圖3給出了安全屬性的驗證，沒有錯誤報告。其他的活性，時序特性驗證也是類似的。

■

圖3TR-Service模型的安全性屬性驗證

在TR-Protocol模型中發(fā)現(xiàn)的錯誤表明TR-Protocol沒有忠實于TR-Service模型定義需求。如圖4，這個錯誤的發(fā)生違反了PS3定義的安全屬性死鎖。首先，TR-Resp驗證完TR-Init的INVOKE消息（包含正確的TID），發(fā)送Result消息，但是這個消息沒有立即到達TR-Init。最后TR-Resp異常終止了這次事務(wù)。但由于TR-Init重傳時間超時TR-Init重發(fā)了INVOKE消息（包含了不正確的TID），這個時候TR-Resp發(fā)送一個ACK進行TID的驗證，并進入TIDok狀態(tài)等待。此時Result消息由于網(wǎng)絡(luò)延遲等原因，TR-Init終于收到了。于是TR-Init最后完成了這次事務(wù)，而TR-Resp還在等待TR-Init響應(yīng)完成TID的驗證。從而TR-Resp形成了死鎖。

5 結(jié)束語

我們的工作主要是形式化分析了一個真實運行的協(xié)議WTP的設(shè)計方案。首先建立了一個有窮自動機模型，然后利用條件表這樣一個中間步驟，我們把有窮自動機模型轉(zhuǎn)化為一個SPIN能夠檢驗的Promela模型。使我們用Promela建模的過程不在看起來僅僅是用Promela編程的過程，而更多的是進行形式化推理的過程。

參考文獻：

[1] Gordon S.Verification of the WAP Transaction Layer Using Coloured Petri Nets[D].Ph D Thesis，University of South Australia，2001.

[2] Open Mobile Alliance(WAP Forum).WAP Wireless TransactionProtocol Specification， Version 2.0[S].Available via http://www.openmobilealliance，2001-07-10.

[3] Holzmann G J.Spin Model Checker， The: Primer and Reference Manual[M].Addison Wesley，2003.

[4] 古天龍，蔡國勇.網(wǎng)絡(luò)協(xié)議的形式化分析和設(shè)計[M].北京:電子工業(yè)出版社，2003.