基于promela模型的socfe協(xié)議調(diào)用順序模型

基于promela模型的socfe協(xié)議調(diào)用順序模型

1基于c語言的socet函數(shù)調(diào)用套接字api連接tcp或ip地址，并為操作系統(tǒng)應(yīng)用層提供可靠的傳輸和不可靠的傳輸接口。socket提供成熟穩(wěn)定的通信功能,眾多互聯(lián)網(wǎng)軟件構(gòu)建在socket接口之上,如網(wǎng)絡(luò)服務(wù)軟件(FTP,SMTP,Telnet,DNS,http的實現(xiàn)等)、中間件(CorbaORB的實現(xiàn))、互聯(lián)網(wǎng)通信應(yīng)用軟件。但由于軟件開發(fā)人員的水平和經(jīng)驗原因,socket函數(shù)調(diào)用順序不正確而產(chǎn)生的運行時潛在問題(內(nèi)存泄漏、死鎖、邊界數(shù)據(jù)丟失等)往往在編譯時發(fā)現(xiàn)不了。鑒于此,程序開發(fā)人員需要一個可以自動檢測socket通信軟件潛在問題的開發(fā)環(huán)境。目前,模型檢測技術(shù)已成為提高軟件質(zhì)量和可靠性的一種現(xiàn)實的、可行的方法,一種方法(如Feaver,JPF1,Bandera,C2Spin)是將高級語言轉(zhuǎn)換成模型檢測工具支持的語言,但這種方法缺乏對系統(tǒng)調(diào)用(如socket函數(shù))的支持。文獻(xiàn)對socket系統(tǒng)調(diào)用實現(xiàn)過程采用Promela語言嵌入C語言代碼的方式進(jìn)行系統(tǒng)建模,較好地對socket通信可靠性進(jìn)行了形式化驗證。文獻(xiàn)假設(shè)Java使用的中間件、網(wǎng)絡(luò)函數(shù)庫依賴于TCP/IP傳輸層的協(xié)議,擴展JPF,驗證基于socket的分布式軟件。但文獻(xiàn)未能對socket通信程序中由于socket系統(tǒng)調(diào)用函數(shù)執(zhí)行順序所導(dǎo)致的運行時潛在問題進(jìn)行討論,然而實際應(yīng)用中此類問題不容忽視。本文針對socket函數(shù)調(diào)用順序正確性問題,設(shè)計從C語言開發(fā)的socket程序源代碼抽取模型方案。通過分析順序結(jié)構(gòu)的socket程序,提出socket通信程序中socket函數(shù)調(diào)用序列抽取算法;描述Promela消息數(shù)據(jù)結(jié)構(gòu)和通道;構(gòu)建socket函數(shù)的Promela模型;定義socket函數(shù)到Promela的映射規(guī)則;提出目標(biāo)Promela模型生成算法,并對模型應(yīng)滿足的性質(zhì)用線性時態(tài)邏輯(LTL)進(jìn)行規(guī)約。開發(fā)了基于SPIN的socket通信程序分析系統(tǒng),并以死鎖檢測為例說明系統(tǒng)的有效性。本文第2節(jié)簡單介紹SPIN和Promela;第3節(jié)闡述服務(wù)、客戶socket程序的socket函數(shù)調(diào)用流程,分析socket函數(shù)調(diào)用順序不正確所產(chǎn)生的問題并提出檢測方案;第4節(jié)闡述從socket程序抽取Promela驗證模型;第5節(jié)對socket函數(shù)調(diào)用序列應(yīng)滿足的性質(zhì)用LTL進(jìn)行刻畫;第6節(jié)闡述socket通信程序分析系統(tǒng),以死鎖檢測實例說明系統(tǒng)的有效性;最后進(jìn)行總結(jié)和展望。2promela自適應(yīng)識別模型模型檢測方法是對一個給定系統(tǒng)(模型),通過窮盡列舉(顯示或隱式)所有系統(tǒng)可達(dá)狀態(tài)和發(fā)生的行為,來驗證期望的行為屬性。SPIN(SimplePromelaInterpreter)是一個對并發(fā)(分布式)系統(tǒng)進(jìn)行形式化驗證的模型檢測工具,用于驗證并發(fā)進(jìn)程的正確性。它支持Promela規(guī)約語言,使用線性時態(tài)邏輯LTL公式描述系統(tǒng)應(yīng)滿足的性質(zhì)。在驗證模式下如果出現(xiàn)違反模型性質(zhì)的一個反例,在仿真模式下可以再現(xiàn)錯誤軌跡。Promela(ProcessMetaLanguage)是建模語言,它對分布式系統(tǒng)進(jìn)行抽象。Promela是基于Dijkstra的非確定性衛(wèi)式命令語言,語法類似于C語言。一般是在假設(shè)的環(huán)境下,使用SPIN驗證Promela模型。Promela模型包括進(jìn)程、消息通道和變量。進(jìn)程是全局對象,表示分布式系統(tǒng)中的并發(fā)實體。消息通道和變量可以聲明為全局的或局部的。進(jìn)程規(guī)約行為,通道和全局變量定義進(jìn)程運行環(huán)境。3socet函數(shù)調(diào)用順序不正確socket系統(tǒng)調(diào)用可分類為初始化(socket、bind)、服務(wù)(listen、accept)、客戶(connect)、輸入(read、readv、recv、recvfrom、recvmsg)、輸出(write、writev、send、sendto、sendmsg)、I/O(select)、終止(shutdown、close)。圖1列出應(yīng)用程序可能使用的socket調(diào)用序列。其中大框的I/O可以以任何順序調(diào)用。socket通信原理、實現(xiàn)及應(yīng)用在文獻(xiàn)[8-10]中有詳細(xì)闡述。socket函數(shù)調(diào)用順序不正確通常導(dǎo)致下列問題:1)在一個服務(wù)程序服務(wù)于多個客戶程序網(wǎng)絡(luò)通信場景下,如果新建立的連接在收發(fā)數(shù)據(jù)結(jié)束后未正常釋放,一方面造成內(nèi)存泄漏,尤其是服務(wù)進(jìn)程將占用大量內(nèi)存空間;另一方面內(nèi)核傳輸層的socket鏈將越來越大,影響IP層交付數(shù)據(jù)包到傳輸層對應(yīng)socket連接時的查找效率,造成內(nèi)核IP層數(shù)據(jù)包處理吞吐量降低;2)socket通信程序通常運行在復(fù)雜的分布式環(huán)境下,讀寫操作交替執(zhí)行,如果出現(xiàn)運行異常,將很難確定是否因為死鎖造成;3)應(yīng)用層數(shù)據(jù)收發(fā)數(shù)據(jù)結(jié)束時未調(diào)用shutdown函數(shù)將影響數(shù)據(jù)的完整性;4)其他情況(如服務(wù)程序未綁定網(wǎng)絡(luò)地址、發(fā)送數(shù)據(jù)前未建立連接等)也將導(dǎo)致出現(xiàn)運行時錯誤問題。通過分析順序結(jié)構(gòu)的socket通信程序,從socket通信程序源代碼中抽取模型,并對所抽取模型的性質(zhì)以LTL進(jìn)行規(guī)約。使用模型檢測工具SPIN驗證模型,可在開發(fā)階段排除socket程序的上述問題,可大大縮短程序調(diào)試時間和減少程序投入使用時的維護(hù)量,從而提高程序可靠性。4promela模型生成SPIN支持的是Promela語言,系統(tǒng)需要將C語言轉(zhuǎn)換成Promela。所以在生成Promela模型之前,對服務(wù)、客戶socket程序進(jìn)行解析,并從中抽取出socket函數(shù)調(diào)用序列,然后調(diào)用模型生成器建立Promela模型。圖2列出模型抽取過程。模型生成器將模板(包括消息通道、全局變量、socket函數(shù)的Promela模型)、socket函數(shù)到Promela語言的映射、LTL性質(zhì)與從socket程序中抽取出來的socket函數(shù)調(diào)用序列組合在一起,生成一個完整的目標(biāo)Promela待驗證模型。4.1基于socet函數(shù)的調(diào)用算法根據(jù)從系統(tǒng)調(diào)用順序正確性角度對socket通信程序可靠性進(jìn)行驗證的需要,結(jié)合一般情況下(假設(shè)socket函數(shù)的調(diào)用只出現(xiàn)在程序的順序結(jié)構(gòu)中,且不在子函數(shù)中調(diào)用socket函數(shù))通信程序的特點,設(shè)計從socket通信程序源代碼中抽取socket函數(shù)調(diào)用序列的算法(以下稱解析算法)。服務(wù)與客戶程序解析過程類似,本文僅給出對客戶程序進(jìn)行解析的算法,如算法1所示。創(chuàng)建匹配字符1)初始化一個堆棧2)初始化socket客戶程序所調(diào)用的socket函數(shù)數(shù)組,Scall={‘socket’,‘connect’,‘read’,‘readv’,‘recv’,‘recvfrom’,‘recvmsg’,‘write’,‘writev’,‘send’,‘sendto’,‘sendmsg’,‘select’,‘shutdown’,‘close’}3)初始化一個空文件tFile4)打開客戶程序源文件sFile(假設(shè)源程序無語法錯誤,無注釋)6)如果當(dāng)前字節(jié)是空格,跳轉(zhuǎn)到第5)步7)將當(dāng)前字節(jié)入棧,繼續(xù)循環(huán)從sFile讀出字節(jié)并入棧(如果遇回車、換行符,則清空堆棧并跳轉(zhuǎn)到第5)步),直到讀出的字節(jié)是左括號字符“(”8)將當(dāng)前堆棧中的所有字節(jié)出棧,并按原順序賦值到一個字符串S(如有空格符,則移除空格),在Scall數(shù)組中查找匹配S的字符串,如果找到匹配則將對應(yīng)的socket函數(shù)字符串插入到tFile9)如果未到文件末尾,跳轉(zhuǎn)到第5步4.2基于主機的統(tǒng)一編碼信息緩沖區(qū)實現(xiàn)是系統(tǒng)建模的一個重要部分。由于socket通信程序中讀寫緩沖區(qū)的函數(shù)調(diào)用序列千差萬別,因此需充分考慮消息數(shù)據(jù)結(jié)構(gòu)的通用性。通過對socket通信消息結(jié)構(gòu)進(jìn)行歸納總結(jié),并假設(shè)客戶和服務(wù)程序在同一主機中運行,我們定義兩個通道,一個用于客戶進(jìn)程發(fā)送消息、服務(wù)進(jìn)程接收消息;另一個用于客戶進(jìn)程接收消息、服務(wù)進(jìn)程發(fā)送消息。下面以客戶進(jìn)程發(fā)送數(shù)據(jù)到服務(wù)進(jìn)程的消息數(shù)據(jù)結(jié)構(gòu)為例進(jìn)行說明:chansBuffer=16of{mtype}消息通道容量大小為16字節(jié)。客戶進(jìn)程使用它發(fā)送消息,服務(wù)進(jìn)程使用它接收來自客戶進(jìn)程的消息。針對本文所關(guān)注的socket函數(shù)調(diào)用順序問題,模型的每一個對sBuffer的讀或?qū)懖僮骶y(tǒng)一為向它讀取或?qū)懭胍粋€字節(jié)。其中“1”表示建立一次連接的請求;“2”表示發(fā)送一次數(shù)據(jù);“3”表示一次由客戶程序發(fā)出的關(guān)閉連接請求。4.3正常讀寫操作socket通信程序通過調(diào)用socket函數(shù)實現(xiàn)系統(tǒng)的信息交換過程,具體到Promela語言中,使用原子序列atomic實現(xiàn)通信原語,在通信原語中對模型的兩個消息通道進(jìn)行讀寫操作。另外,模型建立連接之前、之后及關(guān)閉連接之前的狀態(tài)轉(zhuǎn)換(如連接、讀、寫等狀態(tài))也需要使用變量標(biāo)識出來,而狀態(tài)變量是刻畫socket程序中socket函數(shù)調(diào)用序列LTL性質(zhì)的基礎(chǔ)。下面以服務(wù)進(jìn)程的讀、寫操作為例進(jìn)行說明:此處需要指出,服務(wù)程序模型支持的讀寫序列是:1)建立連接階段->fREADs->fWRITEs->關(guān)閉連接階段;2)建立連接階段->fWRITEs->fREADs->關(guān)閉連接階段。4.4promela通信原語socket函數(shù)以Promela建模后,在模型抽取過程中需將socket函數(shù)系統(tǒng)調(diào)用轉(zhuǎn)換成對應(yīng)的Promela原語。表4列出服務(wù)程序的Csocket函數(shù)與Promela通信原語之間的映射關(guān)系。其中輸入、出入函數(shù)統(tǒng)一轉(zhuǎn)換成fREADs和fWRITEs保證了建模的簡單性,同時也可以保留原程序基本特征。客戶程序映射(轉(zhuǎn)換)表與之類似。4.5目標(biāo)模型生成器算法服務(wù)程序模型的生成過程與客戶程序模型的類似,本文僅給出客戶程序的建模過程算法,如算法5所示。目標(biāo)模型1)打開解析器生成的文件tFile4)根據(jù)當(dāng)前關(guān)鍵詞在映射表中找到相應(yīng)Promela通信原語,并將Promela通信原語插入到模板文件相應(yīng)位置下面列出目標(biāo)模型樣例:5基于oses的socet實現(xiàn)在定義讀寫Promela原語時,涉及下列全局變量:bitREADs=0;#define_WRITEs(WRITEs==1)可得:性質(zhì)1!((_READs&&_READc)&&(!_WRITEs&&!_WRITE))表示客戶和服務(wù)程序新建連接后,在雙方未向緩沖區(qū)寫入數(shù)據(jù)之前不能同時進(jìn)行讀操作,否則將產(chǎn)生死鎖。類似地,可得其它socket函數(shù)調(diào)用順序性質(zhì),包括:性質(zhì)2((_SOCKETs)->(〈〉_CLOSEs))表示服務(wù)或客戶程序中由進(jìn)程創(chuàng)建的socket或由accept調(diào)用成功產(chǎn)生的socket最終將被釋放?？梢允褂迷撔再|(zhì)驗證程序是否存在內(nèi)存泄漏問題。性質(zhì)3((!_SOCKETsU_SOCKETs)U_BIND)表示服務(wù)程序在調(diào)用bind函數(shù)之前必須先調(diào)用socket函數(shù)。性質(zhì)4((!_BINDU_BIND)U_LISTEN)表示服務(wù)程序在調(diào)用listen函數(shù)進(jìn)入監(jiān)聽狀態(tài)之前應(yīng)先綁定網(wǎng)絡(luò)地址。性質(zhì)5((!_LISTENU_LISTEN)U_ACCEPT)表示服務(wù)程序在調(diào)用accept函數(shù)之前應(yīng)先進(jìn)入監(jiān)聽狀態(tài)。否則accept函數(shù)將產(chǎn)生運行時錯誤。性質(zhì)6((!_SOCKETcU_SOCKETc)U_CON-NECT)表示客戶程序在調(diào)用connect與熟知網(wǎng)絡(luò)地址建立連接時應(yīng)先調(diào)用socket新建一個socket。性質(zhì)7((!_CONNECTU_CONNECT)U(_WRITEc‖_READc))表示客戶程序在進(jìn)行讀、寫操作時應(yīng)先調(diào)用connect與熟知網(wǎng)絡(luò)地址建立連接。性質(zhì)8((_WRITEs‖_READs)->(〈〉_SHUT-DOWNs))((_WRITEc‖_READc)->(〈〉_SHUT-DOWNc))表示客戶或服務(wù)程序在調(diào)用讀、寫操作后在調(diào)用close函數(shù)之前應(yīng)調(diào)用shutdown函數(shù)清空讀緩沖,或?qū)懢彺鎱^(qū)數(shù)據(jù)推送出去。使用該性質(zhì)可驗證socket程序是否存在邊界數(shù)據(jù)丟失問題。6promela模型選取流程socket通信程序分析系統(tǒng)包括以下3部分:1)用戶界面模塊,用戶可通過該模塊錄入C語言socket通信程序、模型抽取和驗證等;2)模型自動抽取模塊,系統(tǒng)對錄入服務(wù)、客戶socket程序進(jìn)行詞法分析,并從中抽取出socket函數(shù)調(diào)用序列,然后調(diào)用模型生成器來建立Promela模型;3)自動驗證模塊,驗證模塊集成SPIN子模塊,它的輸入是從socket程序自動抽取的Promela模型,系統(tǒng)返回SPIN運行結(jié)果和出錯信息等,并在發(fā)現(xiàn)問題時給出圖形化的代碼執(zhí)行軌跡。系統(tǒng)內(nèi)部結(jié)構(gòu)圖如圖6所示。使用socket通信程序分析系統(tǒng)可以驗證本文第5節(jié)所列的LTL性質(zhì),下面以死鎖檢測為例進(jìn)行說明。socket通信過程中,在建立socket連接之后,服務(wù)和客戶程序的read及write將會交替執(zhí)行,而read及write操作調(diào)用順序不正確,將可能發(fā)生死鎖。如果客戶和服務(wù)進(jìn)程同時執(zhí)行讀操作,而客戶和服務(wù)進(jìn)程雙方的緩沖區(qū)都為空,則系統(tǒng)發(fā)生死鎖(或發(fā)生讀超時)。假設(shè)服務(wù)程序建立連接后以read->write->關(guān)閉連接運行,客戶程序建立連接后以read->write-