基于CBMC有界模型检测的无线抄表路由协议验证  

VERIFICATION OF WIRELESS METER READING ROUTING PROTOCOL BASED ON CBMC

作　　者：胡世超[1] 杨红丽[1] 秦胜潮 王非[1] 刘渊 

机构地区：[1]北京工业大学计算机学院,北京100124 [2]提赛德大学计算机学院英国米德尔斯堡 [3]西安普瑞米特科技有限公司,陕西西安710075

出　　处：《计算机应用与软件》2016年第4期138-142,共5页Computer Applications and Software

摘　　要：针对工业界实现的无线抄表路由协议WM2RP(Wireless Meter Reading Routing Protocol),提出将CBMC有界模型检测工具运用到该协议实现的验证方法。WM2RP协议实现是嵌入式C程序,CBMC工具主要针对嵌入式软件的验证,运用CBMC对WM2RP进行验证十分适用。CBMC能够直接对C/C++源码进行验证,这样不仅省去了传统模型检测技术需要对代码抽象建模的工作,而且不用担心模型和代码之间可能存在的不一致性问题。首先利用CBMC系统自生成断言验证技术,找到WM2RP协议实现中可能存在的漏洞,并对实现协议的公司给予反馈。然后进一步借助CBMC提供的用户自定义断言技术,通过自定义断言的插入以及对实现代码的适当处理,验证了WM2RP协议的网络层接收函数实现与协议规范的相符性。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 selfgenerate 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.

关 键 词：模型检测 WM2RP路由协议 CBMC 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术]