胡世超 楊紅麗 秦勝潮 王 非 劉 淵

基于CBMC有界模型檢測的無線抄表路由協(xié)議驗(yàn)證

胡世超1楊紅麗1秦勝潮2王 非1劉 淵3

1(北京工業(yè)大學(xué)計算機(jī)學(xué)院 北京 100124)

2(提賽德大學(xué)計算機(jī)學(xué)院 英國 米德爾斯堡)

3(西安普瑞米特科技有限公司 陜西 西安 710075)

針對工業(yè)界實(shí)現(xiàn)的無線抄表路由協(xié)議WM2RP(Wireless Meter Reading Routing Protocol)，提出將CBMC有界模型檢測工具運(yùn)用到該協(xié)議實(shí)現(xiàn)的驗(yàn)證方法。WM2RP協(xié)議實(shí)現(xiàn)是嵌入式C程序，CBMC工具主要針對嵌入式軟件的驗(yàn)證，運(yùn)用CBMC對WM2RP進(jìn)行驗(yàn)證十分適用。CBMC能夠直接對C/C++源碼進(jìn)行驗(yàn)證，這樣不僅省去了傳統(tǒng)模型檢測技術(shù)需要對代碼抽象建模的工作，而且不用擔(dān)心模型和代碼之間可能存在的不一致性問題。首先利用CBMC系統(tǒng)自生成斷言驗(yàn)證技術(shù)，找到WM2RP協(xié)議實(shí)現(xiàn)中可能存在的漏洞，并對實(shí)現(xiàn)協(xié)議的公司給予反饋。然后進(jìn)一步借助CBMC提供的用戶自定義斷言技術(shù)，通過自定義斷言的插入以及對實(shí)現(xiàn)代碼的適當(dāng)處理，驗(yàn)證了WM2RP協(xié)議的網(wǎng)絡(luò)層接收函數(shù)實(shí)現(xiàn)與協(xié)議規(guī)范的相符性。

模型檢測 WM2RP路由協(xié)議 CBMC

0 引 言

模型檢測[1]是一種被廣泛使用的驗(yàn)證有限狀態(tài)系統(tǒng)滿足規(guī)范的自動化技術(shù)。大部分模型檢測工具，如SPIN[2]、PAT[3]、UPPAAL[5]等都是基于模型的。CBMC[4]是一個針對ANSI-C和C++的邊界模型檢查器，它擅長用來檢查程序的可靠性：諸如檢查緩沖區(qū)溢出、數(shù)值溢出、指針安全等程序性質(zhì)，同時它也允許使用自定義的斷言來對程序進(jìn)行建模驗(yàn)證。

無線抄表路由協(xié)議WM2RP是基于無線傳感器網(wǎng)絡(luò)WSN[8,9]的遠(yuǎn)程抄表協(xié)議，主要用于燃?xì)獗頂?shù)據(jù)的收集，并通過無線網(wǎng)絡(luò)返回給服務(wù)器處理。WM2RP協(xié)議的實(shí)現(xiàn)是用ANSI-C語言編寫的嵌入式程序，程序中有大量的數(shù)值型、指針和位敏感操作。雖然WM2RP協(xié)議設(shè)計時已經(jīng)過了驗(yàn)證，但是依然可能隱含著漏洞。WM2RP協(xié)議目前正處于試運(yùn)行階段，找出協(xié)議中可能的錯誤，有很重要的意義。CBMC模型檢查工具支持系統(tǒng)自生成斷言和用戶自定義斷言，能夠有效地幫助我們進(jìn)行分析。

目前對路由協(xié)議實(shí)現(xiàn)進(jìn)行分析、驗(yàn)證的工作相對比較少。文獻(xiàn)[7]是基于規(guī)則的協(xié)議實(shí)現(xiàn)的靜態(tài)分析，提出了一種規(guī)范的語言對協(xié)議規(guī)則進(jìn)行描述，然后利用靜態(tài)分析算法進(jìn)行分析，不過規(guī)則的描述相對比較復(fù)雜。文獻(xiàn)[6]也是對實(shí)現(xiàn)源碼進(jìn)行模型檢測，首先需要規(guī)定正確的屬性，同時需要對測試環(huán)境進(jìn)行建模，使用起來不是很直接。

本文的主要工作：(1)提出將CBMC工具運(yùn)用到WM2RP路由協(xié)議實(shí)現(xiàn)代碼驗(yàn)證的想法。(2)利用CBMC工具系統(tǒng)自生成斷言技術(shù)成功找出WM2RP路由協(xié)議實(shí)現(xiàn)過程中可能存在的一些漏洞。(3)驗(yàn)證了WM2RP路由協(xié)議實(shí)現(xiàn)的網(wǎng)絡(luò)層接收函數(shù)調(diào)用序列的正確性，并總結(jié)了關(guān)于函數(shù)調(diào)用順序和變量訪問順序的一般方法。

1 WM2RP協(xié)議及其實(shí)現(xiàn)

1.1 協(xié)議簡介

WM2RP路由協(xié)議是在PEGASIS[10]協(xié)議的基礎(chǔ)上改進(jìn)而來的，圖1是WM2RP協(xié)議的拓?fù)浣Y(jié)構(gòu)圖，其中Server(服務(wù)器)通過GPRS向Concentrator(集中器)發(fā)送抄表命令，Concentrator再將命令轉(zhuǎn)發(fā)給Meter(燃?xì)獗?節(jié)點(diǎn)，Meter節(jié)點(diǎn)再將抄表信息轉(zhuǎn)發(fā)給下一個Meter節(jié)點(diǎn)，當(dāng)Meter節(jié)點(diǎn)為葉子節(jié)點(diǎn)時，再將收集到的數(shù)據(jù)反向依次返回給Concentrator，最終返回給服務(wù)器。Repeater(中繼器)為路由節(jié)點(diǎn)，當(dāng)Concentrator和Meter節(jié)點(diǎn)超過無線通信范圍的時候，需要借助Repeater進(jìn)行轉(zhuǎn)發(fā)。

圖1 WM2RP協(xié)議的拓?fù)浣Y(jié)構(gòu)圖

1.2 協(xié)議實(shí)現(xiàn)

(1) 協(xié)議實(shí)現(xiàn)代碼分類

WM2RP協(xié)議實(shí)現(xiàn)是在瑞薩(Renesas)嵌入式集成平臺上進(jìn)行的，主要使用ANSI-C，涉及很多變量操作和內(nèi)存讀寫。協(xié)議實(shí)現(xiàn)代碼比較多，還有很多輔助的模塊，比如液晶顯示LCD模塊、IC卡處理模塊等，另外還有很多與硬件相關(guān)的模塊，比如故障、中斷、電池狀態(tài)燈、無線加密模塊等，由于我們主要關(guān)注協(xié)議通信模塊的實(shí)現(xiàn)，所以更多的關(guān)注和協(xié)議通信相關(guān)的實(shí)現(xiàn)代碼，表1是一些主要的代碼文件包括：頭文件和源代碼文件，以及相關(guān)代碼的解釋。

表1 WM2RP協(xié)議實(shí)現(xiàn)代碼分類

續(xù)表1

(2) WM2RP協(xié)議模塊調(diào)用圖

WM2RP協(xié)議模塊調(diào)用關(guān)系如圖2所示，主模塊由IC卡處理模塊、通信處理模塊以及Lcd顯示模塊組成，通信處理模塊包括物理層、數(shù)據(jù)鏈路層、網(wǎng)絡(luò)層和應(yīng)用層。圖2中省略了一些信息，比如變量定義、功能模塊端口定義、寄存器定義、堆棧大小信息定義以及基本功能函數(shù)等。

圖2 模塊調(diào)用關(guān)系圖

2 CBMC工具介紹

2.1 CBMC簡介

CBMC被設(shè)計用來直接分析諸如C,C++的常用語言編寫的程序。圖3虛線框中所示為前端(frontend)處理，首先，C/C++源碼通過語法分析后生成語法分析樹，然后再轉(zhuǎn)化為控制流圖。

CBMC目標(biāo)是檢查斷言屬性的正確性，其思想是沿著CFG路徑到達(dá)一個斷言，然后為相應(yīng)的路徑生成公式，再將生成的公式傳遞給SAT求解器，最終得出是否有滿足條件的解，一般情況下，求出的解是滿足該條路徑的反例，從而判斷該斷言違規(guī)。

總結(jié)來說，CBMC驗(yàn)證程序的過程主要包括3步，如圖3所示。

1) 首先進(jìn)行語法解析，然后構(gòu)建出CFG；

2) 展開(unwind)CFG，形成相應(yīng)的公式(formula)；

3) 通過SAT/SMT求解器求解公式，找到一組滿足公式的賦值。

圖3 CBMC驗(yàn)證流程圖

2.2 CBMC驗(yàn)證原理與驗(yàn)證性質(zhì)

(1) CBMC驗(yàn)證原理

CBMC是使用斷言來表示需要驗(yàn)證的程序性質(zhì)的，斷言是指在程序運(yùn)行到某一特定位置的時候的程序狀態(tài)的一個必須達(dá)到的要求，通常在程序中使用assert宏來顯式指出。CBMC在其根據(jù)源文件生成的CFG中，根據(jù)到達(dá)斷言的路徑生成一個公式(formula)，然后使用SAT查找是否存在滿足這個公式的一個賦值(路徑)，通常情況下這個斷言是一個否定形式的表示，即某條件必須不成立,那么當(dāng)一個滿足公式的賦值找到后，這個賦值對應(yīng)的路徑便是一個違反需要驗(yàn)證的性質(zhì)的反例。

(2) 驗(yàn)證性質(zhì)

CBMC內(nèi)置自動斷言生成器，可以為程序中常見的錯誤自動生成斷言，這可以減少書寫顯然的斷言的重復(fù)工作。這種生成器可以用來檢查緩沖區(qū)溢出、指針安全、除0錯誤、不是數(shù)字、局部變量未初始化、數(shù)據(jù)競爭等性質(zhì)。

CBMC還支持自定義斷言驗(yàn)證，通過插入適當(dāng)?shù)臄嘌詠眚?yàn)證某些特殊的性質(zhì)，例如函數(shù)執(zhí)行順序、代碼實(shí)現(xiàn)與規(guī)范是否相符等。

3 利用CBMC內(nèi)建斷言驗(yàn)證WM2RP協(xié)議

3.1 CBMC內(nèi)建斷言簡介

內(nèi)建斷言主要驗(yàn)證數(shù)組越界、指針安全、除0錯誤、局部變量未初始化、不是數(shù)字和數(shù)據(jù)競爭等以下6類錯誤，而且由系統(tǒng)自動生成，可以直接對源碼進(jìn)行驗(yàn)證。

1) 緩沖區(qū)溢出(buffer overflow)

2) 指針安全(pointer safety)

3) 除0錯誤(divide by zero)

4) 不是數(shù)字(not-a-number)

5) 局部變量未初始化(uninitiated local)

6) 數(shù)據(jù)競爭(data race)

檢查并行程序兩個線程是否在同一時刻訪問同一個共享變量。

CBMC還會對數(shù)值型變量的溢出、動態(tài)申請內(nèi)存的釋放、返回值等進(jìn)行檢查。

3.2 驗(yàn)證結(jié)果

WM2RP協(xié)議整體代碼比較多，當(dāng)我們嘗試從main函數(shù)入手直接進(jìn)行分析時，經(jīng)過很長一段時間之后，CBMC由于內(nèi)存耗盡而退出(實(shí)驗(yàn)所用機(jī)器為8G內(nèi)存)。因此我們從單個文件中的函數(shù)入手進(jìn)行分析。

我們首先對協(xié)議部分進(jìn)行驗(yàn)證，依次對協(xié)議的應(yīng)用層(application.c)、網(wǎng)絡(luò)層(networklayer.c)、數(shù)據(jù)鏈路層(datalinklayer.c)、物理層(413_cc1100.c，413_spi.c)進(jìn)行了驗(yàn)證，發(fā)現(xiàn)了一些其它的相關(guān)函數(shù)問題，例如應(yīng)用層調(diào)用的基本功能模塊和液晶顯示模塊(Lcd.c)發(fā)現(xiàn)了的問題，物理層調(diào)用信息加密處理模塊的一些漏洞。我們根據(jù)CBMC內(nèi)建斷言所能檢查到的錯誤的種類，以模塊的形式展現(xiàn)了相關(guān)錯誤的個數(shù)。由于WM2RP協(xié)議不涉及線程操作，所以不會涉及到數(shù)據(jù)競爭這一類錯誤。表2顯示了驗(yàn)證的結(jié)果。

表2 基于CBMC內(nèi)建斷言的WM2RP協(xié)議的驗(yàn)證結(jié)果統(tǒng)計

續(xù)表2

一共發(fā)現(xiàn)12個可能的錯誤，由于是分模塊進(jìn)行驗(yàn)證的，所以CBMC工具有可能無法掌握全局信息而產(chǎn)生一些誤報。我們把檢查到的錯誤向企業(yè)開發(fā)人員反饋得到了一些回復(fù)。以下是發(fā)現(xiàn)的漏洞編號及錯誤原因、出錯文件、行為描述、公司反饋等信息，如表3所示。

由表3可知，有些錯誤是由于CBMC工具的局限性的誤報所致，程序?qū)嶋H運(yùn)行中不會發(fā)生，例如錯誤10、11、12。還有一些是檢測到的錯誤，公司認(rèn)為是客觀存在的，只是因?yàn)樵撉度胧匠绦虻奶厥庥猛舅隆Ｈ珏e誤1、2、3、4、7、8，有的只是取變量低幾位，這樣即使溢出也不會對實(shí)際造成不良影響。

4 利用CBMC自定義斷言驗(yàn)證

基于CBMC自定義斷言驗(yàn)證協(xié)議實(shí)現(xiàn)的過程，大致可以分成3個步驟：(1) 確定要驗(yàn)證的性質(zhì)：根據(jù)具體協(xié)議的規(guī)范，找出需要驗(yàn)證的性質(zhì)。(2) 對協(xié)議實(shí)現(xiàn)代碼進(jìn)行適當(dāng)處理：針對所關(guān)心的協(xié)議規(guī)范對代碼進(jìn)行適當(dāng)?shù)奶幚恚热绮迦脒m當(dāng)?shù)臄嘌?，來?yàn)證是否滿足協(xié)議規(guī)范，有時還必須對代碼進(jìn)行優(yōu)化處理，例如注釋掉某些無關(guān)語句，加入一些假設(shè)驗(yàn)證等。(3) 驗(yàn)證該斷言是否滿足。

4.1 確定需要驗(yàn)證的性質(zhì)

通過分析WM2RP協(xié)議我們知道節(jié)點(diǎn)接收和發(fā)送過程如圖4所示。

圖4 WM2RP協(xié)議接收發(fā)送示意圖

通過對networklayer.c文件進(jìn)行分析，發(fā)現(xiàn)該函數(shù)中多次涉及數(shù)據(jù)發(fā)送與接收。發(fā)送時，網(wǎng)絡(luò)層會調(diào)用鏈路層發(fā)送函數(shù)(linksend)和物理層發(fā)送函數(shù)(physend)。圖4可看出，將依次調(diào)用linksend和physend函數(shù)。我們將對此進(jìn)行驗(yàn)證，驗(yàn)證networklayer.c文件的netreceive()函數(shù)(或者該函數(shù)調(diào)用其他的代碼中涉及到linksend和physend的調(diào)用)中是否存在違規(guī)調(diào)用的錯誤。

如果協(xié)議實(shí)現(xiàn)過程中先調(diào)用了physend函數(shù)再調(diào)用linksend函數(shù)將會導(dǎo)致數(shù)據(jù)發(fā)送混亂和發(fā)送失敗。雖然可以人工分析代碼中是否會存在這一問題，但是鑒于實(shí)現(xiàn)代碼繁多，并且控制流程復(fù)雜，這樣不僅費(fèi)時，而且容易出現(xiàn)遺漏現(xiàn)象。因此可利用CBMC工具對代碼進(jìn)行處理，驗(yàn)證該性質(zhì)。

4.2 利用CBMC對代碼進(jìn)行處理

(1) 頭文件中進(jìn)行申明和宏處理

我們之前提到對于代碼進(jìn)行的處理不能影響代碼本身的功能，對于linksend進(jìn)行如圖5所示的處理，放在頭文件CBMC_CHECK.h中。

圖5 linksend函數(shù)的聲明與處理

當(dāng)我們調(diào)用linksend的時候，事實(shí)上調(diào)用的是CBMC_linksend，這樣方便在該函數(shù)中加一些處理。對physend的處理情況大致相同。

在CBMC.h頭文件中的具體內(nèi)容如圖6所示。

圖6 頭文件中對linksend和physend的處理

(2) 實(shí)現(xiàn)中加入合適斷言

CBMC_linksend函數(shù)的實(shí)現(xiàn)在CBMC_CHECK.c中，CBMC_CHECK.c文件中不能包括CBMC_CHECK.h頭文件，否則會出現(xiàn)無限循環(huán)。CBMC_linksend具體代碼如圖7所示。

圖7 linksend函數(shù)實(shí)現(xiàn)的處理

由于表示調(diào)用狀態(tài)的變量CBMC_CHECK_STATUS在圖6中被初始化為0，因此圖7第4行調(diào)用linksend函數(shù)后，第5行將其置為1。在調(diào)用physend函數(shù)時檢查CBMC_CHECK_STATUS的值進(jìn)行檢查如果不為1，該斷言違規(guī)，表明調(diào)用順序錯誤。

physend的實(shí)現(xiàn)也在CBMC_CHECK.c文件中，如圖8所示。

圖8 physend函數(shù)實(shí)現(xiàn)的處理

圖8中，第4行加了一個自定義斷言來檢查CBMC_CHECK_STATUS變量是否為1，如果不為1，則程序終止接著第5行將CBMC_CHECK_STATUS重新置為0。第6行調(diào)用physend函數(shù)保持程序行為的不變。

圖8第5行將CBMC_CHECK_STATUS重新置0，是因?yàn)槌绦蚩赡軙霈F(xiàn)如圖9所示的程序情況，其中省略號部分不會涉及l(fā)inksend和physend函數(shù)的調(diào)用。

圖9 一個可能出現(xiàn)的程序片段

這段代碼根據(jù)協(xié)議規(guī)范是錯誤的(第1、2行調(diào)用正確，第3、4行調(diào)用錯誤)。但是如果不將CBMC_CHECK_STATUS重新置0，分析工具將會查不出問題。因?yàn)樵趌inksend和physend函數(shù)被多次調(diào)用的情況下，如果第一次調(diào)用順序正確，CBMC_CHECK_STATUS會被置為1，并且一直不會變化，接下來的調(diào)用就都會顯示正確，從而有可能會出現(xiàn)誤報。

(3) 代碼適當(dāng)優(yōu)化

CBMC通過不確定性選擇對用戶輸入進(jìn)行建模，例如當(dāng)在程序中使用scanf()，getchar()輸入。CBMC用nondet_為前綴的方式(如int nondet_int())處理這類輸入，返回一個不確定性的int值。這類函數(shù)是CBMC內(nèi)建的，并且提供有不同的類型。CBMC將會計算每一個可能值產(chǎn)生的各種情況。

對于程序輸入的不確定性，分析工具要考慮每一種可能的情況，這樣就會浪費(fèi)大量的時間。為此，CBMC提供有假設(shè)機(jī)制。CBMC使用__CPROVER_assume語句來約束需要考慮的程序的跡(trace)，并且保證假設(shè)是合理的。__CPROVER_assume語句接受一個邏輯表達(dá)式。

對于網(wǎng)絡(luò)層的接收函數(shù)netreceive()而言，該函數(shù)的主框架是一個switch語句，共分為四種情況，分別為接收到命令、接收到應(yīng)答、命令是否跳級和應(yīng)答是否跳級。程序中利用Rnetflag標(biāo)志來區(qū)分這4種不同的標(biāo)識。我們對程序進(jìn)行了一個小的優(yōu)化處理。原程序中Rnetflag是一個int型變量，實(shí)際使用中我們只有4種不同的值(1,2,3,4)，由于靜態(tài)分析的方法，不可能知道實(shí)際傳來的值的情況，所以對代碼進(jìn)行了如圖10所示的優(yōu)化處理：

圖10 代碼的優(yōu)化處理

圖10中，第1行將Rnetflag標(biāo)記與它原來的輸入對應(yīng)起來， nondet_int()表示用戶輸入的一個不確定性的值。第2行則進(jìn)行了假設(shè)，保證Rnetflag的值在1、2、3、4之間，不僅簡化了分析過程，同時沒有改變程序原來的行為。

4.3 自定義斷言驗(yàn)證結(jié)果

因?yàn)镃BMC是單步驗(yàn)證的，在進(jìn)行自定義斷言之前，先要更正CBMC內(nèi)建斷言所報錯誤。經(jīng)過4.2節(jié)所述的代碼處理后，就可以對所需要的性質(zhì)進(jìn)行驗(yàn)證，驗(yàn)證結(jié)果如圖11所示。

圖11 函數(shù)調(diào)用順序的驗(yàn)證結(jié)果

但當(dāng)我們試圖交換其中一個linksend和physend的調(diào)用順序之后，驗(yàn)證結(jié)果如圖12所示。

圖12 更改函數(shù)調(diào)用順序后的出錯信息

圖12中報告錯誤的位置在18行，所在的文件是CBMC_CHECK.c，這說明了如果代碼中出現(xiàn)這樣的問題是可以檢測出來的，我們對于代碼的建模處理是正確的。

4.4 自定義斷言驗(yàn)證總結(jié)

因?yàn)橐?yàn)證的性質(zhì)是根據(jù)軟件的規(guī)范所確定的，不同的軟件需要驗(yàn)證的性質(zhì)也會有區(qū)別，這樣對代碼的處理就不太一樣，所以對于自定義斷言驗(yàn)證很難給出一個統(tǒng)一的方案。

即便如此，我們?nèi)匀豢梢詮暮瘮?shù)調(diào)用順序的驗(yàn)證中得到很多啟發(fā)。對于協(xié)議規(guī)范中，需要滿足某個前提條件。在協(xié)議實(shí)現(xiàn)代碼中一般表現(xiàn)為某條語句的執(zhí)行必須在另一條語句之前，或者說某條語句執(zhí)行時必須滿足什么前提條件這類問題，一般表現(xiàn)在函數(shù)調(diào)用順序或者是變量的訪問順序上。

5 結(jié) 語

本文基于CBMC模型檢查工具驗(yàn)證了企業(yè)實(shí)際開發(fā)的無線抄表路由協(xié)議(WM2RP)。利用CBMC工具內(nèi)建斷言進(jìn)行驗(yàn)證，找出了WM2RP協(xié)議實(shí)現(xiàn)代碼中可能存在的一些漏洞；運(yùn)用CBMC的自定義斷言技術(shù)，驗(yàn)證了WM2RP協(xié)議網(wǎng)絡(luò)層實(shí)現(xiàn)中有關(guān)接收函數(shù)調(diào)用序列的正確性，驗(yàn)證結(jié)果對于WM2RP協(xié)議的開發(fā)者有很大的參考意義。

不足之處是，對于CBMC內(nèi)建斷言驗(yàn)證部分，一般是以單元驗(yàn)證的形式進(jìn)行的，所以會出現(xiàn)一些誤報現(xiàn)象。對于自定義斷言驗(yàn)證部分，本文只驗(yàn)證了網(wǎng)絡(luò)層函數(shù)調(diào)用順序這一性質(zhì)，今后需要發(fā)掘更多可以驗(yàn)證的性質(zhì)。

[1] Clarke E M,Emerson E A.Design and synthesis of synchronization skeletons using branching time temporal logic[C]//Logic of Programs,volume 131 of Lecture Notes in Computer Science,Springer-Verlag,1981:52-71.

[2] Holzmann G J.The model checker SPIN[J].IEEE Transactions on Software Engineering,1997,23(5):279-295.

[3] Jun Sun,Yang Liu,Jin Songdong,et al.PAT:Towards Flexible Verification under Fairness[C]//Proceedings of the 21st International Conference on Computer Aided Verification (CAV’09),2009:709-714.

[4] Clarke E M,Kroening D,Lerda F.A Tool for Checking ANSI-C Programs[C]//Conferences on Theory and Practice of Software(TACAS),ETAPS 2004,Barcelona,Spain,March 29-April 2,2004.Proceedings,2004:168-176.

[5] Bengtsson J,Larsen K G,Larsson F,et al.UPPAAL-a Tool Suite for Automatic Verification of Real-Time Systems[C]//Proceedings of the DIMACS/SYCON workshop on Hybrid systems III:verification and control Springer-Verlag New York,Inc.Secaucus,NJ,USA,1996:232-243.

[6] Musuvathi M,Park D Y W,Chou A,et al.CMC:A Pragmatic Approach to Model Checking Real Code[C]//Proceedings of the 5th symposium on Operating systems design and implementation,2002:75-88.

[7] Octavian Udrea,Cristian Lumezanu,Jeffrey S Foster.Rule-based static analysis of network protocol implementations[C]//Proceedings of the 15th USENIX Security Symposium,2006:193-208.

[8] 孫利民,李建中,陳渝,等.無線傳感器網(wǎng)絡(luò)[M].清華大學(xué)出版社,2005.

[9] 賀康.基于WSN的抄表系統(tǒng)路由協(xié)議研究[D].北京:北京工業(yè)大學(xué)計算機(jī)學(xué)院,2012.

[10] Lindsey,Raghavendra C.PEGASIS:Power-efficient gathering in sensor information systems[C]//Aerospace Conference Proceedings,2002,3:1125-1130.

VERIFICATION OF WIRELESS METER READING ROUTING PROTOCOL BASED ON CBMC

Hu Shichao1Yang Hongli1Qin Shengchao2Wang Fei1Liu Yuan3

1(BeijingUniversityofTechnology,Beijing100124,China)2(SchoolofComputer,TeessideUniversity,Middlesbrough,TeesValley,UK)3(Xi’anPrepaidMeterTechnologyCo.,Xi’an710075,Shaanxi,China)

In light of the wireless meter reading routing protocol WM2RP implemented by industry sector, we presented a verification approach for applying CBMC bounded model checking tool to the implementation of this protocol. The implementation of WM2RP protocol is to embed C programs, and the CBMC tool mainly targets at the verification of embedded software, so to apply CBMC to verifying WM2RP is quite applicable. CBMC can verify C/C++ source directly, which not only omits the work of abstractly modelling the code in traditional model detection technology, but also relieves the worry on inconsistencies between model and code. We first used CBMC system to self-generate the assertion-based verification technique, and found some vulnerabilities possibly existed in the implementation of WM2RP protocol, and sent the feedbacks to companies implementing the protocol. Then we further got the support from user-defined assertions technology provided by CBMC to have verified the WM2RP protocol in terms of the conformity between the implementation of reception function on network layer and the specification of protocol by the insertion of user-defined assertions and proper processing on the implemented codes.

Model checking WM2RP routing protocol CBMC

2014-09-16。胡世超，碩士生，主研領(lǐng)域：無線傳感器網(wǎng)絡(luò)協(xié)議，程序分析。楊紅麗，副教授。秦勝潮，副教授。王非，碩士生。劉淵，碩士。

TP3

A

10.3969/j.issn.1000-386x.2016.04.033