胡世超 杨红丽 秦胜潮 王 非 刘 渊

基于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]的远程抄表协议，主要用于燃气表数据的收集，并通过无线网络返回给服务器处理。……