基于CBMC有界模型檢測的無線抄表路由協議驗證

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

基于CBMC有界模型檢測的無線抄表路由協議驗證

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

1(北京工業大學計算機學院 北京 100124)

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

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

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

模型檢測 WM2RP路由協議 CBMC

0 引 言

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

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

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

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

1 WM2RP協議及其實現

1.1 協議簡介

WM2RP路由協議是在PEGASIS[10]協議的基礎上改進而來的，圖1是WM2RP協議的拓撲結構圖，其中Server(服務器)通過GPRS向Concentrator(集中器)發送抄表命令，Concentrator再將命令轉發給Meter(燃氣表)節點，Meter節點再將抄表信息轉發給下一個Meter節點，當Meter節點為葉子節點時，再將收集到的數據反向依次返回給Concentrator，最終返回給服務器。Repeater(中繼器)為路由節點，當Concentrator和Meter節點超過無線通信范圍的時候，需要借助Repeater進行轉發。

圖1 WM2RP協議的拓撲結構圖

1.2 協議實現

(1) 協議實現代碼分類

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

表1 WM2RP協議實現代碼分類

續表1

(2) WM2RP協議模塊調用圖

WM2RP協議模塊調用關系如圖2所示，主模塊由IC卡處理模塊、通信處理模塊以及Lcd顯示模塊組成，通信處理模塊包括物理層、數據鏈路層、網絡層和應用層。圖2中省略了一些信息，比如變量定義、功能模塊端口定義、寄存器定義、堆棧大小信息定義以及基本功能函數等。

圖2 模塊調用關系圖

2 CBMC工具介紹

2.1 CBMC簡介

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

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

總結來說，CBMC驗證程序的過程主要包括3步，如圖3所示。

1) 首先進行語法解析，然后構建出CFG；

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

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

圖3 CBMC驗證流程圖

2.2 CBMC驗證原理與驗證性質

(1) CBMC驗證原理

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

(2) 驗證性質

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

CBMC還支持自定義斷言驗證，通過插入適當的斷言來驗證某些特殊的性質，例如函數執行順序、代碼實現與規范是否相符等。

3 利用CBMC內建斷言驗證WM2RP協議

3.1 CBMC內建斷言簡介

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

1) 緩沖區溢出(buffer overflow)

2) 指針安全(pointer safety)

3) 除0錯誤(divide by zero)

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

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

6) 數據競爭(data race)

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

CBMC還會對數值型變量的溢出、動態申請內存的釋放、返回值等進行檢查。

3.2 驗證結果

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

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

表2 基于CBMC內建斷言的WM2RP協議的驗證結果統計

續表2

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

由表3可知，有些錯誤是由于CBMC工具的局限性的誤報所致，程序實際運行中不會發生，例如錯誤10、11、12。還有一些是檢測到的錯誤，公司認為是客觀存在的，只是因為該嵌入式程序的特殊用途所致。如錯誤1、2、3、4、7、8，有的只是取變量低幾位，這樣即使溢出也不會對實際造成不良影響。

4 利用CBMC自定義斷言驗證

基于CBMC自定義斷言驗證協議實現的過程，大致可以分成3個步驟：(1) 確定要驗證的性質：根據具體協議的規范，找出需要驗證的性質。(2) 對協議實現代碼進行適當處理：針對所關心的協議規范對代碼進行適當的處理，比如插入適當的斷言，來驗證是否滿足協議規范，有時還必須對代碼進行優化處理，例如注釋掉某些無關語句，加入一些假設驗證等。(3) 驗證該斷言是否滿足。

4.1 確定需要驗證的性質

通過分析WM2RP協議我們知道節點接收和發送過程如圖4所示。

圖4 WM2RP協議接收發送示意圖

通過對networklayer.c文件進行分析，發現該函數中多次涉及數據發送與接收。發送時，網絡層會調用鏈路層發送函數(linksend)和物理層發送函數(physend)。圖4可看出，將依次調用linksend和physend函數。我們將對此進行驗證，驗證networklayer.c文件的netreceive()函數(或者該函數調用其他的代碼中涉及到linksend和physend的調用)中是否存在違規調用的錯誤。

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

4.2 利用CBMC對代碼進行處理

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

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

圖5 linksend函數的聲明與處理

當我們調用linksend的時候，事實上調用的是CBMC_linksend，這樣方便在該函數中加一些處理。對physend的處理情況大致相同。

在CBMC.h頭文件中的具體內容如圖6所示。

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

(2) 實現中加入合適斷言

CBMC_linksend函數的實現在CBMC_CHECK.c中，CBMC_CHECK.c文件中不能包括CBMC_CHECK.h頭文件，否則會出現無限循環。CBMC_linksend具體代碼如圖7所示。

圖7 linksend函數實現的處理

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

physend的實現也在CBMC_CHECK.c文件中，如圖8所示。

圖8 physend函數實現的處理

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

圖8第5行將CBMC_CHECK_STATUS重新置0，是因為程序可能會出現如圖9所示的程序情況，其中省略號部分不會涉及linksend和physend函數的調用。

圖9 一個可能出現的程序片段

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

(3) 代碼適當優化

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

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

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

圖10 代碼的優化處理

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

4.3 自定義斷言驗證結果

因為CBMC是單步驗證的，在進行自定義斷言之前，先要更正CBMC內建斷言所報錯誤。經過4.2節所述的代碼處理后，就可以對所需要的性質進行驗證，驗證結果如圖11所示。

圖11 函數調用順序的驗證結果

但當我們試圖交換其中一個linksend和physend的調用順序之后，驗證結果如圖12所示。

圖12 更改函數調用順序后的出錯信息

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

4.4 自定義斷言驗證總結

因為要驗證的性質是根據軟件的規范所確定的，不同的軟件需要驗證的性質也會有區別，這樣對代碼的處理就不太一樣，所以對于自定義斷言驗證很難給出一個統一的方案。

即便如此，我們仍然可以從函數調用順序的驗證中得到很多啟發。對于協議規范中，需要滿足某個前提條件。在協議實現代碼中一般表現為某條語句的執行必須在另一條語句之前，或者說某條語句執行時必須滿足什么前提條件這類問題，一般表現在函數調用順序或者是變量的訪問順序上。

5 結 語

本文基于CBMC模型檢查工具驗證了企業實際開發的無線抄表路由協議(WM2RP)。利用CBMC工具內建斷言進行驗證，找出了WM2RP協議實現代碼中可能存在的一些漏洞；運用CBMC的自定義斷言技術，驗證了WM2RP協議網絡層實現中有關接收函數調用序列的正確性，驗證結果對于WM2RP協議的開發者有很大的參考意義。

不足之處是，對于CBMC內建斷言驗證部分，一般是以單元驗證的形式進行的，所以會出現一些誤報現象。對于自定義斷言驗證部分，本文只驗證了網絡層函數調用順序這一性質，今后需要發掘更多可以驗證的性質。

[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] 孫利民,李建中,陳渝,等.無線傳感器網絡[M].清華大學出版社,2005.

[9] 賀康.基于WSN的抄表系統路由協議研究[D].北京:北京工業大學計算機學院,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。胡世超，碩士生，主研領域：無線傳感器網絡協議，程序分析。楊紅麗，副教授。秦勝潮，副教授。王非，碩士生。劉淵，碩士。

TP3

A

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