网络协议工程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的功能进一步扩大。2023年推出的SPIN4.0版本支持C代码的植入，应用的灵活性进一步增强。随后2023年推出的SPIN4.1版本加入了深度优先搜索算法，2023年连续推出SPIN5.2版本，这使得SPIN的发展又上一个新台阶。NASA使用SPIN检测在1996年火星探测者所存在的错误，结果发现一些错误是可以在发射之前就可以被检测并改正的。SPIN从此就被用来检测土星火箭控制软件和一些应用与外层空间的程序。因SPIN有良好的算法设计和非凡的检测能力，得到了ACM(AssociationforComputingMachinery)(世界最早的专业计算机协会)的认可，在2023年授予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）在,withsources版本，最新版本是6.44，下载的文献名为：spin644.tar.gz。解压后，里面文献内容：（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 fi57 58 ::(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=2SENDER(1):SendSeq=0对于接受者REC