IEEE 802.1D生成树协议的形式化验证

理论计算机科学电子笔记159（2006）139-154www.elsevier.com/locate/entcsIEEE 802.1D生成树协议的形式化验证侯赛因·霍贾特德黑兰大学电气与计算机工程系伊朗德黑兰Hootan Nakhost2德黑兰大学电气与计算机工程系伊朗德黑兰Marjan Sirjani3德黑兰大学电气与计算机工程系伊朗德黑兰摘要以IEEE 802.1D为标准的STP（Spanning Tree Protocol，生成树协议）已被广泛应用于网络的网桥和交换机中。该算法试图消除桥接网络中的环路。在这项研究中，STP算法的正确性进行了形式化验证，使用扩展的Rebeca。为了不局限于一个特定的情况或一组情况，我们使用了组合验证方法。这使得我们在验证算法时具有普遍性。扩展的Rebeca语言在模型检验方面的清晰性和方便性表明，该语言可以用于将来验证更多的网络协议关键词：Rebeca，生成树协议（STP），IEEE 802.1D，形式验证，组合验证。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.066140H. Hojjat等人/理论计算机科学电子笔记159（2006）1391引言随着网络的增长，越来越多的计算机被添加到系统中，不可能将所有计算机都放在一个LAN中。通常，两个或多个独立的LAN使用网桥互连，形成扩展LAN。由于这些局域网中的管理是分开的，因此不容易避免环路的产生。在扩展的局域网中，环路可能会造成一些破坏性的影响如果网络中存在环路，主机可能会收到重复的数据包。 此外，循环可以使用“bro adcas tsto r m s“phe n om e n o n n。一个broadcstt r r e r s t tr r ster s t r r s t e rs t r r s t r s t r r s tr st广播风暴可以迅速关闭网络[5]。当支持生成树协议（STP）的网桥识别出网络拓扑中的环路时，它会阻塞一个或多个冗余端口。网桥会不断地探索网络，因此当网络拓扑发生变化时，STP会通过阻塞某些端口来自动重新配置网桥端口，以避免出现故障。STP算法最早由Perlman [13]在20世纪80年代中期在DEC LAN网桥中实现，它在IEEE 802.1D标准中定义。由于其状态空间的指数大小，网络协议很难测试[11]。此外，协议中的错误需要大量时间才能被发现，并且复制错误通常是不可能的。形式化验证技术可以用于网络协议的正确性检验。在网络协议的验证方面已经做了大量的工作[3，7，16，24]。据我们所知，IEEE 802.1D尚未得到正式验证。在这项研究中，我们使用基于角色的[1，8]模型，Rebeca [19，21]及其组合验证方法验证了STP的正确性。如IEEE标准802.1D中所定义的，生成树协议是检测环路和关闭冗余链路的方法。如果我们想确保协议正常工作，我们应该保证它在每个网络拓扑中都能工作。一般来说，在特殊网络配置中证明STP的正确性通过在验证中使用组合方法，我们可以对协议操作有一个广泛的了解在这项工作中使用的建模语言是ExtendedRebeca [17，19]，相应的工具用于验证我们的模型[18，20]。reebeca是一种工具支持的建模语言，它利用了组合验证技术。它是基于演员模型的。Rebeca中的模型由一组并发反应式1电子邮件：h. ece.ut.ac.ir2电子邮件：h. ece.ut.ac.ir3电子邮件：msirjani@ut.ac.irH. Hojjat等人/理论计算机科学电子笔记159（2006）139141reactiveclass 1（2）{knowwnobjects{Rebec2d;}statevarsmsgsrvinitial（）{self. mysql（）;}mysql（）{d. askforrService（）;}msgsrvmsg2（）{/*Handlingmessage2*/}}Fig. 1. 一个典型的类定义在Rebeca对象，称为rebecs。rebecs是事件驱动的，这意味着它们通过执行某些代码来响应接收到的消息。这是我的错。与其他可用的类似语言相比，这种语言的主要特点可以用两个核心功能来解释：基于角色的建模和组合验证。在ExtendedR ebeca [17]中，有一些额外的功能使我们的建模过程更容易。ExtendedR ebeca旨在为建模者提供两种更有用的功能：组件和同步消息传递。组件允许我们将高度耦合的对象连接在一起。同步消息传递在建模某些本质上是同步的交互时特别有用。这项工作的主要贡献是tomodel802. 1D使用Rebeca和使用Rebeca的 复 杂 性 验 证 方 法 及 其 工 具 来 证 明 ST P 。本文的组织如下：第3节一般描述生成树协议我们介绍了扩展Rebeca的关键概念，第2款.第4节讨论了一个典型示例的验证。我们在第5节中解释我们的证明。2扩展的RebecaRebeca（ReactiveObjec t La nuage）的设计旨在为非正式方法专家的从业者提供验证过程的便利。从一个角度来看，Rebeca是一种类似Java的语言，易于软件工程师使用，从另一个角度来看，它是一种具有形式验证支持和背景理论的建模语言。 Rebeca中的一个模型由并发执行的reactive对象jects，rebecs组成。 计算通过rebecs之间的异步消息传递和执行相应的消息方法来进行。每个消息都放在接收方rebec的无限队列中，并指定在服务消息时要调用的唯一方法。142H. Hojjat等人/理论计算机科学电子笔记159（2006）139图1展示了一个简单的Rebeca类定义。虽然在纯Actor模型中队列长度是无限的，但作为模型检查的一部分，建模者必须在类定义中声明最大队列大小。这个大小应该在reactiveClass名称旁边的括号中表示在一个类的定义中有两个中心声明：knownobserver和statevars。knownobacks条目显示了这个对象可以与它们通信的rebecs。州议员负责控制雷贝克州。在这些声明之后，消息处理方法在类似Java的代码中定义。我们将这些方法称为这个反应类的消息服务器，因为它们的任务是为传入的消息提供服务。与Java中一样，点表示法用于表示向rebec发送消息。对象内并发在Actor和Rebeca中是不同在丽贝卡，对象具有唯一的控制线程。这为Rebeca的模型检查带来了简单和轻松。在每一步中，rebec从它的队列中获取一条消息并执行相应的消息服务器。每个响应式类定义都有一个名为initial的消息服务器。在初始状态下，每个rebec在其消息队列中有一个初始消息，因此每个rebec执行的第一个方法是初始消息服务器。在定义了反应类之后，有一个关键字main，后面跟着Rebeca模型的定义，它是一个有限的rebecs集在声明一个rebec时，到它的已知rebec的绑定在knownoblock列表中指定。Rebeca已经扩展到包括两个新概念：组件和同步消息传递[17]。一个扩展的瑞贝卡模型是由多个组件组成的。一个组件通常包含一些强耦合的rebecs，它们可以被许多模型使用。组件中的rebecs可以异步通信也可以同步通信。同步消息通过握手进行建模，并且没有匹配的消息服务器。调用rebec请求通过调用目标rebec上的方法与另一个rebec握手。此方法未直接在数据库的数据库中指定，因此无法将其作为一个数据库。rebec通过执行receive语句接受与任何调用者的握手。如果没有呼叫者rebec正在等待，它将被阻止。组件之间的协作是通过匿名消息广播完成的。广播类似于普通的异步消息传递，不同之处在于没有指定目标。组合验证[6，15]，是一种可行的方法，以减少状态空间避免了模型检验中的空间爆炸。在这种验证方法中，整个系统的属性是从本地组件的属性。通常，组件的验证是在一个假设的保证风格，其中一些假设的环境和组件的行为是有条件地证明系统结构。H. Hojjat等人/理论计算机科学电子笔记159（2006）139143为了从组成上验证一个Rebeca模型，应该将模型分解为组件和环境。每个组件都是系统的rebecs的子集，其余的组成了环境。 环境的行为不需要完全建模。环境由发送到组件的一组消息建模。在[19]中，通过使用弱模拟关系，证明了如果某个部件满足某些安全特性，则它们对于系统保持不变。 因此，通过模型检验证明了组件的属性，并用于推导系统的属性。与将外部消息放入队列不同，假定它们存在于所有状态中。这需要始终启用与执行外部消息相对应的转换。因此，组件的rebecs在从内部队列中取出消息和执行外部消息之间交替。还有一个工具，Rebeca Verifier [18，20]，用于将Rebeca翻译为现有模型检查器的语言，Promela [22]和SMV [12]。该工具还自动化了抽象和组合验证方法。结果代码可以通过Spin [22]或NuSMV [12]进行模型检查。必须检查的属性在后端模型检查器的规范语言中声明。我们选择Spin作为我们的后端模型检查器。3生成树协议通过关闭网桥的冗余端口，在STP中对网络进行修剪。该算法将扩展的局域网看作是一个由局域网和网桥组成的图。扩展LAN中的每个网桥由其网桥ID唯一标识应该选择ID最小的网桥在生成的树中，每个节点都有一个唯一的祖先。此祖先直接连接到节点，并且位于到树根的最短路径上。LAN的前身是一个称为指定网桥的网桥。网桥的前身是一个单独的局域网，称为前身局域网. STP中的 主 要 协 议 数 据 单 元 是 Hello 消 息 或 配 置 网 桥 协 议 数 据 单 元（BPDU）。网络中的每一个网桥都交换Hello消息来收集网络中其他网桥的信息Hello消息是由三部分组成的三元组：发送网桥ID、根网桥的网桥ID和从该网桥到根网桥的距离（或成本）如果（a）A的根ID小于B，144H. Hojjat等人/理论计算机科学电子笔记159（2006）139则A的发送网桥ID小于B。Hello消息由根网桥定期发起，并通过扩展LAN进行传播。消息的这种传播导致以下结果[4]：(i) 为稳定的生成树网络拓扑选择唯一的根桥(ii) 为每个LAN网段选择指定的网桥(iii) 为每一个网桥选举一个前身LAN。每个网桥都将自己视为根，开始传输Hello消息。当网桥收到Hello消息时，它会将消息中的根网桥ID的值与它当前信任的根网桥ID进行比较。如果消息中的值较小，网桥将改变其对树根的信任。然后，它在其他端口上发送带有新值的Hello消息。否则，网桥将继续使用先前的值发送Hello消息。通过这个过程，扩展LAN中的所有网桥最终将学习根网桥的网桥ID。祖先节点的选举与根桥的选举方式相同如果网桥从一个LAN收到一条消息，指出有另一个网桥连接到这个LAN，并且它离根更近，它将停止向那个LAN发送消息因此，只有具有到根的最短路径的网桥（或在为了选择前身LAN，每个网桥都考虑它从所连接的LAN接收到的消息更接近根的LAN是前代LAN。在平局的情况下，选择类似于指定网桥选举，采用具有较小指定网桥ID的LAN如果网桥至少被指定用于一个LAN，它将保持与前一个LAN的链路端口以全双工模式运行。STP算法停用LAN到网桥方向以关闭端口。永远不要禁用反向。网络中的动态变化，如选举新的根网桥，或网桥由于致命错误条件而变得不可用，通常会导致选举新的指定网桥[2]。网络中的故障由Hello消息中的额外字段（年龄字段）检测。一旦网桥接收到Hello消息并将其存储，它就会处理其年龄值并不断增加[13]。当指定的网桥想要将Hello消息转发到LAN时，它会将最新的年龄值复制到该消息中。消息的寿命有一个最大界限，如果H. Hojjat等人/理论计算机科学电子笔记159（2006）139145如果超过该阈值，则将发生超时每当网络中发生超时时，信息就会被丢弃，网桥会重新计算新的根或新的路径[13]。我们不考虑网络中的超时，因为它不会改变我们证明STP算法的方法。在发现网络中的超时后，超时的网桥用相同的算法找到新的生成树4一个典型的例子在本节中，我们考虑一个典型的验证示例。我们在Rebeca中对这个简单的例子进行建模，指定所需的属性，并使用Rebeca Verifier工具对其进行模型检查。在下面的部分中，我们将使用组合验证方法进行一般证明。4.1问题规格我们要找到其生成树的网络拓扑如图2所示。在这幅图中，圆圈代表桥梁。每个网桥都有一个独特的ID，分别是B1、B2和B3。假设sender ID）&{//similartoabove}else{//call config}}}if（IamRoot）{波尔·T·S。sendLann（myID，0，myID）;}}reactiveclassPort{knowwnobjects{RotControl lerotControl ler;LANlan;}状态变量{通过trotID;通过trotDistance;通过tbestSenD;boolleannisTheBestPort;boolleannisEnabled;boolleannisDesignatd;}mysql（）{//.. }msgsrvsetBestPort（）{这是B=true;rootControllleer. intcount（）;publicvoidrun（）{这是一个错误，但不是一个错误。intn=0;}msgsrvsendLan（bytesenderID，bytedistance，bytebelevedRootID）{if（belevedRootIDrootID）{isEnabled=true;isDesignated=true;lan. recv（s_end_r_ID，d_i_t_n_ce，b_e_v_d_R_ot_ID）;}其他if（believedRootID==rootIDdistancerootDistance）{//similartooabove}其他if（believedRootID==rootIDistance==rootDistancestSender ID>SenderID）&{//similartooabove}else//i. e. ，新的方法会使预存的数据更少{isDesignated=false;if（！ isTeBest）{isEnabled=false;}}} }个文件夹消息gsrvsendBridge（按teprtID、按tesender ID、按tedistance、按tebelevedRotID）{//sendigthemessagetorotcontrolleupdatedata}}图三.桥梁构件148H. Hojjat等人/理论计算机科学电子笔记159（2006）139reactiveclasLAN（3）{knowwnobjects{}statevars{}msgsrvinitial（）{}msgsrvrecv（byteportID，bytesender ID，bytedistance，bytebelivedRootID）{brodCast（portID，sender ID，distance，belivedRootID）;}}见图4。LAN代码探索状态六、09741 ×106表示系统状态476字节总内存使用量1487.768兆字节状态空间树755表1抽象模型状态我们指的是当网桥关于它们的前一个LAN以及它们被指定用于哪个LAN的信念达到稳定状态时，假设网络配置在生成树形成期间不改变Pro perty4. 1：（（Q（（IamRoot[B1]）（<$IamRoot[B2]）（<$IamRoot[B3]）第二个属性说明了稳定状态下的链路状态。有些链接应该禁用，有些应该启用。网桥B3的所有端口将在最终网络中被禁用（图2）.Pro perty4. 2：（（Q（（<$enabled_B3_C））（<$enabled_B3_B））（enabled_B2_C）（enabled_B2_A）（e n a bl e d_B 2_（enabled_B1_A）（enabled_B1_B）5STP证明在上一节中，我们展示了一个具体的例子。在本节中，我们使用组合验证方法来证明STP。为了证明STP算法的正确性，我们需要证明[13]中采用的以下性质这些性质在稳定状态下被H. Hojjat等人/理论计算机科学电子笔记159（2006）139149图五.指定桥接选举(i) 根选择：正确选择根，每个网桥正确计算从自身到根网桥的最短路径距离(ii) 唯一指定网桥：每个LAN在生成树中都有一个正确的唯一指定网桥。(iii)Unique Predecessor LAN：每个网桥在生成树中都有一个正确且唯一的Predecessor LAN。第一个属性被假设为真，另外两个属性被证明使用Rebec a的公司在一家私营公司中排名第一。从上述性质可以得出结论[13]，网络的形成图是一棵树。图中的每个节点都有一个祖先。结果图是连通的，因为每个节点都有一个祖先。它也是无循环的，因为每个节点都有一条通过其祖先到根的路径。Root选举Leader Election问题[23]是计算机科学中的一个基本问题我们在这里不讨论这个算法，我们假设它是正确的。唯一指定桥梁我们必须证明，使用STP算法，可以为LAN正确选择指定的网桥。指定网桥是指与连接到局域网的其它网桥相比，具有最短路径到达根的网桥。在平局的情况下，具有较小ID的网桥将被选为指定网桥。我们将图5中所示的LAN视为一个连接了任意n个LAN的通用LAN。请注意，图5中的网桥编号并不显示网桥ID。我们表明，指定的桥梁是正确的。引理5.1考虑两个网桥i和j，它们连接到LAN 1。假设i和j到根的距离是路径i和路径j，i是150H. Hojjat等人/理论计算机科学电子笔记159（2006）139见图6。 桥j不是为l比j更好（路径i<路径j或路径i=路径j和i

下载后可阅读完整内容，剩余1页未读，立即下载