基于SPIN的协议分析验证研究

摘要:为了研究协议分析验证方法的有效性,论文利用协议分析验证工具SPIN对可靠传输协议中的GBN协议进行了分析验证,结果发现单纯依靠工具并不能保证协议的正确性,本文对如何确保协议的正确性进行了研究,提出了具体建议。

关键词:SPIN;协议分析验证;Promela语言;GBN协议

中图分类号:TP393.08

The research of protocol analysis and verification based on SPIN

HOU Fenghan1 BAI Xiaochong2

(1 Department of Computer Engineering , Henan Polytechnic Institute, Nanyang, Henan, China, 473009

2 PLA Uint 95865, Changping, Beijing, China, 102218)

Abstract:In order to research the effectivity of the protocol analysis verification, this paper analyzed and verified the reliable transport protocol GBN by protocol analysis tool SPIN. This paper found that only relying on SPIN can not guarantee the correctness of the protocol, studied how to ensure the correctness of the protocol, and made specific recommendations.

Keywords:SPIN; Protocol Analysis and Verification; Promela; GBN

0 引言

计算机网络及数据通信是当今信息社会的基石,网络协议则是其中不可缺少的重要组成部分,形式化方法与技术已经渗透到网络协议开发的整个过程[1]。研究人员已开发出了支持协议开发活动中形式化描述、正确性验证、性能分析、自动代码生成和一致性测试等各个方面的多种软件工具,SPIN正是其中进行协议分析验证的工具。本文利用用协议分析工具SPIN对可靠传输协议中的GBN协议进行了分析验证。通过研究,发现单纯依靠工具并不能保证协议的正确性,论文对如何确保协议的正确性提出了具体建议。

论文的第1节简单介绍协议分析验证工具SPIN和形式化描述语言Promela。第2节简单介绍GBN协议及其验证。第3节提出单纯依靠工具产生的问题及如何确保协议正确性的具体建议。最后,我们在第4节对全文进行总结。

1 SPIN及相关概念

1.1 协议分析验证工具SPIN

当前,在模型检验分析方面人们已经开发出了多种自动化工具,SPIN就是其中比较典型的一种。SPIN的全称是Simple Promela Interpreter(简单Promela解释器)。它是适合于并行系统,尤其是协议一致性的辅助分析验证工具。该工具由贝尔实验室的形式化方法与验证小组于1980年开始开发[1]。SPIN软件是用ANSI C开发的,可以在Unix操作系统上使用,在windows操作系统上使用则需要安装不同版本,windows下已经开发出了一个图形界面的版本XSPIN,本文即使用XSPIN。

1.2 形式化描述语言Promela

Promela语言是SPIN的核心,它的全称是Protocol/Process Meta Language,是1983年设计的Argos语言的一个扩展,是一种用于描述通信协议或其他类似的分布式系统的一种抽象语言[2]。Promela类似于C语言,对有限状态系统进行建模,允许动态创建并行的进程,并可以在进程之间通过消息通道进行同步(使用会面点(rendezvous port))或异步(使用缓冲)进行通信[1]。一个Promela程序由一组相互之间进行通信的进程构成。每一个进程是一个扩展的有限状态机(EFSM,Extened Finite State Machine)。在这种语言中只支持简单的数据类型,如各种范围的整形、记录类型(与C语言中的typedef类似)。

2 GBN协议及其验证

2.1 GBN协议

GBN(Go-Back-N)协议通常被称为滑动窗口协议(sliding-window protocol),该协议允许发送方发送多个分组(当有多个分组时)而不需要等待确认,但其受限于管道中未被确认的分组数,此数目最大不能超过最大允许数目N,N即为窗口大小。如下图所示[3]。

2.2 GBN协议分析验证

GBN协议的发送方响应三种事件:

(1)上层调用:上层调用udt_send()时,发送方先检查发送窗口是否已满。如果未满,则创建一个分组并发送,否则上层将等待一段时间再试。

(2)ACK的接收:对序号为n的分组的确认用于累计确认(cumulative acknowledgment)。即收到序号为n的确认分组,则表明n之前的报文都正确收到,此时发送方将窗口基序号修改为n。

(3)超时事件:发送方使用一个定时器,它被最早的已发送但未被确认的分组使用。如果超时发生,发送方将重发所有已发送过但还未被确认过的分组。如果收到一个有效ACK,则定时器被重新启动。

GBN协议的接收方动作很简单,如果一个序号为n的分组被正确收到,并按序,则接收方为分组n发送一个ACK,并将分组中的数据交付到上层,在所有其他情况下,接收方丢弃该分组并为最近按序接收的分组重发ACK。

为研究方便,同时不影响实验目的,在发送方去除了上层调用检查判断发送窗口是否已满的动作,简化为发送方的skip动作,同时,发送方和接收方向上层递交分组不予考虑,假定为收到即交付。GBN协议用Promela语言描述如下:

#define WIN 4 /*定义窗口大小*/

#define MAX 25/*定义发送报文计数最大值*/

chan s_r=[10] of {mtype,byte,byte};/*定义发送端到接收端传输通道*/

chan r_s=[10] of {mtype,byte,byte};/*定义接收端到发送端传输通道*/

mtype={mesg, ack, err};/*定义消息类型*/

proctype udt_sender() /*发送端进程*/

{

byte s,r,swl;/*s为要发送的报文的序号,r为确认报文的序号,swl为滑动窗口下限*/

swl = 0; /*窗口初始化*/

do::swl = swl;

progress:s = swl; /*将要发送报文指针移到窗口头*/

progress1: if

::s_r!mesg(0,s)-> /*成功发送正确报文*/

(swl

if

::goto progress1; /*在窗口内连续发送*/

::skip/*也可以不发送*/

fi;

::s_r!err(s,0) -> /*发送的报文在传输通道中出错*/

(swl

if

::goto progress1;

::skip

fi;

::skip -> /*报文在传输通道中丢失*/

(swl

if

::goto progress1;

::skip

fi;

fi;

if

::timeout -> goto progress /*超时,从超时报文开始重发*/

::r_s?err(0,r) -> skip /*收到错误报文不工作*/

::r_s?ack(r,0) ->/*收到正确应答报文*/

if

::(r skip /*确认序号低于窗口下限*/

::(r>s) -> skip /*高于已发送报文最大值*/

::(swl

swl = r;/*移动窗口*/

goto progress; /*继续发送*/

fi;

fi;

od

}

proctype udt_receiver()/*接收端进程*/

{

byte t,es;/*t为接收报文的序号,es为期望收到的报文序号*/

es = 0; /*初始化*/

do

::s_r?mesg(0,t) ->/*收到正确报文*/

if

::(t==es)-> /*收到报文为所期望报文*/

progress2:es = (es + 1)%MAX;/*更新期望值*/

if

::r_s!ack(es,0) /*发送确认*/

::r_s!err(0,es) /*发送的确认报文在传输通道中出错*/

::skip /*确认报文在传输通道中丢失*/

fi

::(t!=es)->/*收到无效报文*/

if

::r_s!ack(es,0)/*重发确认*/

::r_s!err(0,es) /*发送的确认报文在传输通道中出错*/

::skip /*确认报文在传输通道中丢失*/

fi

fi

::s_r?err(t,0)->/*收到的报文出错*/

if

::r_s!ack(es,0)/*重发确认*/

::r_s!err(0,es) /*发送的确认报文在传输通道中出错*/

::skip /*确认报文在传输通道中丢失*/

fi

od

}

init

{ /*启动进程*/

run udt_sender();

run udt_receiver();

}

本协议描述在xspin工具下运行正常,经仿真验证,验证了该描述的正确性。

3 问题和建议

3.1 问题的提出

在分析验证GBN协议的过程中,我们发现,在确保协议正确性方面单纯依靠工具会产生一些问题:

(1)书写形式化描述同使用c、delphi等高级语言编程有很多类似的方面,只是语法更简单,为处理方便和适应形式化描述语言,协议分析验证人员常常(或者必须)简化或忽略某些操作,如本文对发送方同上层交互的简化。这些简化或忽略掉的操作是否不重要而可以被简化或忽略?简化或忽略掉这些操作是否会产生问题?这些问题单纯依靠工具无法解决。

(2)当研究人员分析了协议并使用形式化描述语言编写出一个形式化描述,并用spin进行了验证,穷举了所有的状态空间,于是就认为协议百分之百正确。事实上,研究人员只是证明了自己写的形式化描述(或程序)在spin这个解释器上运行没有问题,并不能保证协议的正确性。有这样一种可能:某研究人员设计了一个协议,协议分析研究人员根据这个协议编写了形式化描述,验证没问题,但事实上这个形式化描述所代表的协议同研究人员设计的协议可能根本不是同一个,而是协议分析研究人员根据自己的理解所产的“协议”。这样,如何确保协议分析人员的“协议”同设计人员的“协议”之间的一致性?单纯依靠工具无法解决。

(3)形式化描述语言往往语法较简单,数据类型少,优点是可以很快掌握,但存在问题就是往往表现不了太细节的内容,只能对被验证系统作简化,简化后的系统往往因不能处理细致的问题而没有实用价值,因此,即使验证了形式化描述的正确性也只是说明简化系统正确,但实际的系统是否正确,不能肯定。如何确保形式化描述系统同实际应用系统的一致性?同样单纯依靠工具无法解决。

如果spin工具生成的代码能同用户的实际程序相媲美,那么上面的问题就能解决,遗憾的是目前的工具在代码自动生成方面还不是很理想,例如生成代码往往比较长,可读性差,等等,最重要的是与实际系统性能相差甚远,而现在似乎也看不到在将来自动生成的代码能达到完成实际功能的希望。

3.2 具体建议

当开发一个新的系统时,在软件工程上需要确保最终生成的实际系统与用户需求的一致,协议设计分析同样如此,必须保证最终在实际系统中运行的协议同用户需求一致才能够满足要求,即保证下面的等式成立:

实际系统=用户需求

但用户需求的原始描述往往比较随意,而实际开发的系统往往代码冗长,分析源代码不便,因而通过分析源代码保证上述等式成立不可行,而通过软件测试的方法也比较难以保证所有情况都考虑到,难以有效判断上述等式是否成立。形式化描述的抽象性介于用户需求和实际系统二者之间,具有比程序更好的可读性又不像原始描述那样随意,因此,为提高协议开发的正确性,通过形式化描述在用户需求原始描述与程序代码之间加入了一个变换、缓冲,从而有助于分析判断,即下面的等式:

实际系统=形式化描述=用户需求

3.2中提出的第3个问题,如何确保形式化描述系统同实际应用系统的一致性,即如何确保前一个“=”成立,第2个问题,如何确保协议分析人员的“协议”同设计人员的“协议”之间的一致性,即如何确保后一个“=”成立,第1个问题,如何判断简化或忽略掉的操作不重要,即如何确保简化或忽略掉一些操作后上述两个“=”仍然成立。

协议分析验证工具本身并不能解答这些问题,它仅仅为研究人员提供了一个能够对形式化描述语言进行编辑、编译、运行的可视化工具,方便研究人员完成形式化描述并对该形式化描述进行检验验证,其他的问题必须靠研究人员自身解决,因此,提出如下建议:

(1)在用户需求到形式化描述的过程中,研究人员必须慎重判断协议中的各种操作,尽量少的简化和省略操作,尽力去理解设计人员开发的协议,即尽可能完全地理解用户需求,从而人工保证形式化描述=用户需求。

(2)在协议验证过程中,如有可能,研究人员必须详细观察协议在实际系统中的运行,从而判断协议执行中的操作和其重要性,尽量保证简化系统能够反映实际系统的主要特性和操作;而在协议开发过程中,在应用到实际系统时必须使程序与形式化描述尽量一致,从而人工保证形式化描述=实际系统。

在执行上述两项建议后,协议分析验证人员能够以人工方式保证实际系统=形式化描述=用户需求,从而能够正确验证已经应用的协议或者开发新的协议并确保新协议正确应用。

4 结语

论文简单介绍了协议分析验证工具SPIN,并利用其对GBN协议进行了分析验证,在此过程中发现了协议分析工具的局限性,提出了相关问题,并对如何解决这些问题给出了具体建议,为协议开发和验证人员在研究过程中解决问题提供帮助。如何为研究人员提供更加方便、直观的辅助从而减少研究过程中人为原因造成的不一致是今后协议分析验证工具的一个重要的发展方向。

参考文献

[1] 古天龙,蔡国永. 网络协议的形式化分析与设计[M]. 北京:电子工业出版社,2003.

[2]叶新铭,郝松侠. IPv6邻居发现协议的形式化验证[J]. 软件学报,2005(6).

[3] 库罗斯[美]等著. 陈鸣,李兵,贾永兴 译. 计算机网络-自顶向下方法与Internet特色(第三版)[M].北京:机械工业出版社,2009.