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

基于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