网络协议工程SPIN实验报告

网络协议工程SPIN实验报告摘要：本文主要介绍了一种基于模型检测的协议自动分析工具SPIN的使用。对经典的AB协议在理想状态、信道有误码无丢失和信道有误码有丢失三种不同环境中分别进行建模，并运用SPIN进行自动分析。在信道有误码有丢失的情况中，我们分别设置了两种错误，以进一步观察协议的运行，分析协议存在的问题。从而加深对协议验证技术和形式化描述技术的认识和理解，进一步掌握运用PROMELA语言对协议进行建模，同时掌握SPIN的基本操作，熟悉运用SPIN对网络协议进行分析，提高实验能力。关键词：模型检测；AB协议；SPIN。0.引言随着计算机通信与网络技术的迅猛发展，网络技术在人们日常的工作、学习和生活的各个方面都得到了普遍地运用。各种网络通信系统在提供越来越丰富的功能的同时，其设计和实现也日益复杂。面对复杂网络系统的挑战，传统的自然语言进行的协议描述，虽然具有表达能力强、可读性好、方便的优点，但是存在不严格、不精确、没有描述标准和存有二义性等缺点。形式化方法使得对网络通信系统的描述、实现和测试变得容易，在对于协议实现、测试的自动化和协议验证上得到了广泛运用。本文主要介绍一种基于模型检测的协议自动分析工具SPIN及其在分析网络协议中的应用。1.SPIN概述随着计算机通信与网络技术的迅猛发展，网络技术在人们日常的工作、学习和生活的各个方面都得到了普遍运用。各种网络通信系统在提供越来越丰富的功能的同时，其设计和实现也日益复杂。面对复杂网络系统的挑战，传统的自然语言进行的协议描述，虽然具有表达能力强、可读性好、方便等优点，但是存在不严格、不精确、没有描述标准和存有二义性等缺点。形式化方法使得对网络通信系统的描述、实现和测试变得容易，在对于协议实现、测试的自动化和协议验证上得到了广泛运用。本文主要介绍一种基于模型检测的协议自动分析工具SPIN及其应用。1.1SPIN概述SPIN(SimplePROMELAInterpreter)是一种用丁对并发系统验证模型检测器，采用深度优先搜索算法，偏序化简和on-the-fly策略从不同的角度来解决模型检测方法中普遍存在的状态空间爆炸问题，其适合对协议验证。SPIN支持随机、交互和指导性的自动机验证，它主要针对设计规范进行检测。最早是由贝尔实验室的形式化方法与验证小组于1980年开始开发的。1995年偏序简约和线性时态逻辑转换的引入使得SPIN的功能进一步扩大。2001年推出的SPIN4.0版本支持C代码的植入，应用的灵活性进一步增强。随后2003年推出的SPIN4.1版本加入了深度优先搜索算法，2023年连续推出SPIN5.2版本，这使得SPIN的发展又上一个新台阶。NASA使用SPIN检测在1996年火星探测者所存在的错误，结果发现一些错误是可以在发射之前就可以被检测并改正的。SPIN从此就被用来检测土星火箭控制软件和一些应用与外层空间的程序。因SPIN有良好的算法设计和非凡的检测能力，得到了ACM(AssociationforComputingMachinery)(世界最早的专业计算机协会)的认可，在2001年授予SPIN的开发者Holzmann享有声望的软件系统奖。迄今为止SPIN也是唯一获得ACM软件系统奖的模型检测工具。SPIN通过模仿系统的执行并产生C程序，探测系统的状态空间，最终验证系统的属性是否满足，如不满足，通过提供系统轨迹的形式帮助使用者找出违反正确性属性的状态。SPIN作为一种形式化自动验证工具，其目的是：提供系统建模语言，用于直观、明确地描述系统模型规约，而不考虑具体实现细节；功能强大而简明的描述系统应满足性质属性要求的逻辑表示法：提供一套验证系统建模逻辑一致性及系统是否满足所要验证性质的方法。它以PROMELA为输入语言，用线性时态逻辑(LTL)公式描述系统必须满足的性质。SPIN可以对大型的协议系统进行有效的正确性分析，即使这个系统覆盖了最大限度的状态空间。SPIN首先从一个描述的协议系统的高层模型规格开始，经分析没有语法错误后，对系统的交互进行模拟，直到确认系统设计拥有预期的行为；然后，SPIN将产生一个明C语言描述的验证程序，经检验器编译后被执行，执行中如果发现了违背正确性说明的任何反例，则可反馈给交互模拟机，通过重现细节剔除引起错误的原因。图1-1描述了SPIN模拟和检测的过程。PROMELA解析器PROMELA解析器LTL公式解析和转换器SPIN语法错误报告验证机产生器交互模拟模型优化测试器执行on-the-fly验证反例图1-1SPIN模拟和检测的过程1.2SPIN安装及使用SPIN可以在很多平台上运行，具有很多版本，我们在这个实验中是在Windows764位操作系统中，基于Cygwinlinux模拟器中实现的，下面是简要的安装过程。1.软件准备：（1）在://spinroot/spin/Src/index.html网页上下载Fulldistribution,withsources版本，最新版本是6.44，下载的文件名为：。解压后，里面文件内容：（2）下载并运行cygwin软件，选择64位windows版本。选择默认参数安装。需要注意以下几点：a.选择下载站点要选择等国内镜像站点，加快下载速度。b.需要选择相应的安装组件：(binutils、bison、byacc、xinit、x-org-server、m4、tcl等)选择红色框部分，展开分别选择：binutils、bison、byacc继续选择：继续选择：make退到上一层，选择展开x11选项：继续选择：下面2项然后，退回上层，搜素m4在结果中选择安装搜素tcl，选择相应包（tcl是运行图形界面ISPIN的必须环境）。点击下一步，等待安安装完成。最后选择创建桌面和开始菜单文件，完成安装。3）安装完cygwin后，在系统盘（C盘）会有文件夹，进入：c:/cygwin64/bin中，将第一步已解压的SPIN文件夹复制进来，并改名为Spin1。进入Spin1文件夹中的iSpin文件夹，复制ispin.tcl至外面的bin目录中，并去掉.tcl后缀。c.编译配置ISPIN安装完cygwin后，先在windows7命令行运行：C:\>setCYGWIN=ttynotitleglob，打开cygwin的控制台程序：进入到spin源码目录中c:/cygwin64/bin/spin1/src然后进行make：（如果编译不成功，往往因为cygwin编译环境没装好，重新检查安装环节组件的选择）输入命令：make–fmakefile成功后，src目录里会产生spin.exe，将其复制到bin目录中。测试tcl环境(如果找不到相应文件，则无法运行ISPIN，重新检查安装环节tcl组件的选择)输入命令：Whichtclsh输入命令：Whichwishd.运行ISPIN运行开始->cygwin-x->xwinserver桌面右下角会出现当前的xserver的虚拟桌面编号（:2.0）在cygwin的控制台中指定ISPIN运行界面的虚拟桌面编号输入命令：exportDISPLAY=:2.0运行ISPIN输入命令：ispin这样就可以使用ISPIN。2.实例分析本次实验主要分析AB协议，分别针对理想状态、信道有误码无丢失和信道有误码有丢失，三种不同的通信环境，设计测试三组实验。在第三组实验过程中，又进行了协议的两种错误处理。2.1AB协议简介AB(AlternatingBit)协议是最早的端到端通信协议之一。在AB协议系统中，包含有发送端和接收端两个实体。发送端协议实体从发送方获取一个报文，将序号寄存器值赋给报文，然后向接收端实体发出报文，发送方发出报文之后启动超时计时器，等待确认报文。如果在给定的时间内没有收到确认报文，则重发该报文。如果收到确认报文，其序号与发出报文序号相同，则序号寄存器的内容加l模2，然后发送端实体从发送方用户获取下一个报文；如果收到否定的确认报文，则重发该报文；接收端协议实体在收到报文后，如果确认报文无错误，并且序号和序号寄存器的值相等，则向发送端实体发送确认报文(认可报文的序号值等于接收报文的序号值)，然后将报文递交给接收方用户，序号寄存器的内容加l模2。如果接收的报文有错误，或者序号不正确，则发送否定确认报文。2.2理想状态下的AB协议实验在理想状态下，信道没有误码，没有丢失，接收方有无限接收能力。这种状态下，协议比较简单，一方发送，一方接收，不设超时计时器，不进行报文确认。下面是协议的PROMELA描述模型。1#defineMAXSEQ32chanSenderToReceiver=[1]of{int};//只含有1个int类型的通道34proctypeSENDER()//发送方5{6 intseq=0;7 end: do8 ::SenderToReceiver!seq;//发送序号9process: seq=(seq+1)%MAXSEQ;//10 od;11 12}1314proctypeRECEIVER()//接收方15{16 intData;17 end1: do18 ::SenderToReceiver?Data;//从通道接收数据19 od;20}21//--------------------开始运行协议-----------------------22init23{24 atomic//原子操作25 {26 runSENDER();27 runRECEIVER();28 }29}将上述代码保存为RTD1.pml，在ISPIN中打开，点击SyntaxCheck进行语法错误检测，如图所示，没有语法错误。然后选择verification选项卡，进行模型验证，模型验证分成三块，safety、liveness、以及LTLneverclaims。刚开始我们先对程序进行安全性和可活动性验证，下面截图中用的是默认勾选的选项，第一个表示死锁，进程无法执行下去，第二个表示程序的断言冲突（在RTD1.pml中不包含断言），第三个是允许循环，就是允许只有一个进程一直处于活动状态，而另一个不动。点击run进行验证，如图所示，没有存在error。Unreached说明两个进程一直在循环运行。点击Simulate/Replay，进行模拟重放，点击(Re)Run，可以形象地观察协议运行过程。发送方按0,1,2有序发送，接收方按0,1,2有序接收。2.3信道有误码、无丢失下的AB协议实验在此实验中，我们考虑收发信道都产生误码，但没有发生丢包的情形。分别用进程SENDER和RECEIVER来对AB协议的发送端和接收端进行建模：通过进程SENDER的发送语句“OutCh!Msg(SendData,SendSeq)”和“OutCh!Err(8,8)”分别模拟正确传送和误码两种情况；通过进程RECEIVER的发送语句“OutCh!Ack(ReceivedSeq,0)”、OutCh!Nak(ReceivedSeq,0)和“OutCh!Err(8,8)”来分别模拟确认报文、否定确认报文和回执报文发送误码三种情况。在SENDER和RECEIVER进程中使用了assert语句来检验在可能会发生任意的消息丢失的情况下，数据是否能全部按顺序正确地传送到接收端。在SENDER和RECEIVER进程中使刚progress状态标记两端传送确实的数据所必须要执行的语句。因为有可能发送端和接收端只在某些无效的状态中循环，使用progress标记可以在检测过程中检测出没有任何实质意义的不可推进的循环。下面是协议的PROMELA描述模型。1#defineMAXSEQ523mtype={Msg,Ack,Nak,Err};45chanSenderToReceiver=[1]of{mtype,byte,byte};6chanReceiverToSender=[1]of{mtype,byte,byte};78proctypeSENDER(chanInCh,OutCh)9{10byteSendData;//发送的数据11byteSendSeq;//发送序号12byteReceivedSeq;//接收序号13SendData=MAXSEQ-1;//下一个要发送的序号14do15 ::SendData=(SendData+1)%MAXSEQ;//下一个消息16again:if17 ::OutCh!Msg(SendData,SendSeq)//正确发送数据18 ::OutCh!Err(8,8)//出现误码19fi;2021 if22 ::InCh?Nak(ReceivedSeq,0)->23end: gotoagain//收到否定确认，重传24 ::InCh?Err(8,8)->gotoagain//收到ACK误码，重传25 ::InCh?Ack(ReceivedSeq,0)->//收到肯定确认26 if2728 ::(ReceivedSeq==SendSeq)->gotoprogress//确认号正确，传下一报文29 ::(ReceivedSeq!=SendSeq)->30end1: gotoagain//确认号有误，重传31 fi32 fi;33progress: SendSeq=1-SendSeq;//产生下一个报文序号34od;35}3637proctypeRECEIVER(chanInCh,OutCh)38{39byteReceivedData;//接收的数据40byteReceivedSeq;//接收的序号41byteExpectedData;//期望的数据42byteExpectedSeq;//期望的序号4344do45 ::InCh?Msg(ReceivedData,ReceivedSeq)->46 if47 ::(ReceivedSeq==ExpectedSeq)->//数据按序到达，发送确认报文48 assert(ReceivedData==ExpectedData);//检验数据是否能按顺序传送到接收端49progress: ExpectedSeq=1-ExpectedSeq;50 ExpectedData=(ExpectedData+1)%MAXSEQ;51 if52 ::OutCh!Ack(ReceivedSeq,0);//ACK报文正确53 ::OutCh!Err(8,8);//模拟ACK报文误码54 ExpectedSeq=1-ExpectedSeq;55 ExpectedData=(ExpectedData+4)%MAXSEQ;56 fi5758 ::(ReceivedSeq!=ExpectedSeq)->59 if60 ::OutCh!Nak(ReceivedSeq,0);//数据不按序到达，发送否定确认报文61 ::OutCh!Err(8,8);//模拟ACK报文误码62 fi63 fi64 ::InCh?Err->OutCh!Nak(ReceivedSeq,0);//数据错误，发送否定确认报文65od;66}676869init70{71 atomic//原子操作，执行过程不允许打断72 {73 runSENDER(ReceiverToSender,SenderToReceiver);//发送者74 runRECEIVER(SenderToReceiver,ReceiverToSender);//接收者75 }76}将上述代码保存为RTD2.pml，在ISPIN中打开，点击SyntaxCheck进行语法错误检测，没有语法错误。然后选择verification选项卡，进行模型验证，点击run进行验证，如图所示，没有存在error。Unreached说明两个进程一直在循环运行。点击Simulate/Replay，进行模拟重放，点击(Re)Run，可以形象地观察协议运行过程。从图中，我们可以直观的看到否定确认、正确确认、回执产生误码和发送报文产生误码的情况。否定确认确认报文否定确认确认报文回执误码发送误码2.4信道有误码、有丢失下的AB协议实验在此实验中，我们考虑收发信道都产生误码，并且都有发生丢包的情形。分别用进程SENDER和RECEIVER来对AB协议的发送端和接收端进行建模：通过进程SENDER的发送语句“OutCh!Msg(SendData,SendSeq)”、“OutCh!Err(8,8)”和“skip”分别模拟正确传送、误码和丢包三种情况；通过进程RECEIVER的发送语句“OutCh!Ack(ReceivedSeq,0)”、“OutCh!Nak(ReceivedSeq,0)”、“OutCh!Err(8,8)”和“skip”来分别模拟确认报文、否定确认报文、回执报文发送误码和回执报文丢失三种情况。进程RECEIVER中，对正确接收的报文回执时，产生回执报文误码“OutCh!Err(8,8)”和丢包“skip”的情况，应该用“ExpectedSeq=1-ExpectedSeq;ExpectedData=(ExpectedData+4)%MAXSEQ;”，来还原因前一个数据包正确接收而更改的“ExpectedSeq”和“ExpectedData”的值，否则会因为期望接收序号与实际接收序号不一致而一直处于回执“OutCh!Nak(ReceivedSeq,0)”的情况。在SENDER和RECEIVER进程中使用了assert语句来检验在可能会发生任意的消息丢失的情况下，数据是否能全部按顺序正确地传送到接收端。在SENDER和RECEIVER进程中使刚progress状态标记两端传送确实的数据所必须要执行的语句。因为有可能发送端和接收端只在某些无效的状态中循环，使用progress标记可以在检测过程中检测出没有任何实质意义的不可推进的循环。在此实验中，我们分别模拟了两种错误情况：一是发送方对否定确认报文的忽略，二是接收方在回执发生丢包时，未及时还原期望接收数据和期望接收序号。下面是协议的PROMELA描述模型。1#defineMAXSEQ523mtype={Msg,Ack,Nak,Err};45chanSenderToReceiver=[1]of{mtype,byte,byte};6chanReceiverToSender=[1]of{mtype,byte,byte};78proctypeSENDER(chanInCh,OutCh)9{10byteSendData;//发送的数据11byteSendSeq;//发送序号12byteReceivedSeq;//接收序号13SendData=MAXSEQ-1;//下一个要发送的序号14do15 ::SendData=(SendData+1)%MAXSEQ;//下一个消息16again:if17 ::OutCh!Msg(SendData,SendSeq)//正确发送数据18 ::OutCh!Err(8,8)//出现误码19 ::skip//报文丢失20fi;2122 if23 ::timeout->gotoagain//超时重传24 ::InCh?Nak(ReceivedSeq,0)->25end: gotoagain//收到否定确认，重传26 ::InCh?Err(8,8)->gotoagain//收到ACK误码，重传27 ::InCh?Ack(ReceivedSeq,0)->//收到肯定确认28 if2930 ::(ReceivedSeq==SendSeq)->gotoprogress//确认号正确，传下一报文31 ::(ReceivedSeq!=SendSeq)->32end1: gotoagain//确认号有误，重传33 fi34 fi;35progress: SendSeq=1-SendSeq;//产生下一个报文序号36od;37}3839proctypeRECEIVER(chanInCh,OutCh)40{41byteReceivedData;//接收的数据42byteReceivedSeq;//接收的序号43byteExpectedData;//期望的数据44byteExpectedSeq;//期望的序号4546do47 ::InCh?Msg(ReceivedData,ReceivedSeq)->48 if49 ::(ReceivedSeq==ExpectedSeq)->//数据按序到达，发送确认报文50 assert(ReceivedData==ExpectedData);//检验数据是否能按顺序传送到接收端51progress: ExpectedSeq=1-ExpectedSeq;52 ExpectedData=(ExpectedData+1)%MAXSEQ;53 if54 ::OutCh!Ack(ReceivedSeq,0);//ACK报文正确55 ::OutCh!Err(8,8);//模拟ACK报文误码，并还原期望的序号和数据56 ExpectedSeq=1-ExpectedSeq;57 ExpectedData=(ExpectedData+4)%MAXSEQ;58 ::skip//报文丢失，并还原期望的序号和数据59 ExpectedSeq=1-ExpectedSeq;60 ExpectedData=(ExpectedData+4)%MAXSEQ;61 fi62 63 ::(ReceivedSeq!=ExpectedSeq)->64 if65 ::OutCh!Nak(ReceivedSeq,0);//数据不按序到达，发送否定确认报文66 ::OutCh!Err(8,8);//模拟ACK报文误码67 ::skip//报文丢失68 fi69 fi70 ::InCh?Err(8,8)->OutCh!Nak(ReceivedSeq,0);//数据错误，发送否定确认报文71od;72}737475init76{77 atomic//原子操作，执行过程不允许打断78 {79 runSENDER(ReceiverToSender,SenderToReceiver);//发送者80 runRECEIVER(SenderToReceiver,ReceiverToSender);//接收者81 }82}将上述代码保存为RTD3.pml，在ISPIN中打开，点击SyntaxCheck进行语法错误检测，没有语法错误。然后选择verification选项卡，进行模型验证，点击run进行验证，如图所示，没有存在error。Unreached说明两个进程一直在循环运行。点击Simulate/Replay，进行模拟重放，点击(Re)Run，可以形象地观察协议运行过程。从图中，我们可以直观的看到丢包、否定确认、正确确认、回执产生误码和发送报文产生误码的情况。丢包回执误码丢包回执误码发送误码正确确认否定确认2.4.1下面来观察两种错误的处理。1.发送方对否定确认报文的忽视如果我们修改25行中，对否定确认报文正确的处理应该是重传，而改为忽视，不重传，还是继续发送下一个数据，则在进行模型验证时，会产生一个错误“assertionviolated(ReceivedData==ExpectedData)(atdepth121)”，我们在程序中第50行用assert标记进行检验数据是否能按顺序传送到接收端时，系统产生违反这一检测的错误。在进行Simulate/Replay，进行模拟重放，在Mode选项页中，会自动勾选Guided，withtrail，ISPIN会将错误的运行结果存储到RTD3.pml.trail文件中，点击(Re)Run进行回放，在运行到最后一步时，我们从变量窗口发现：RECEIVER(2):ExpectedData=0RECEIVER(2):ExpectedSeq=0RECEIVER(2):ReceivedData=2RECEIVER(2):ReceivedSeq=0SENDER(1):ReceivedSeq=1SENDER(1):SendData=