混合直觉线性逻辑验证无线有线通信协议基础性质

理论计算机科学电子笔记133（2005）255-273www.elsevier.com/locate/entcs基于混合直觉线性逻辑的无线和有线通信协议大卫·辛克莱1都柏林城市大学爱尔兰都柏林市中心詹姆斯·鲍尔2爱尔兰国立大学计算机科学系，Maynooth Maynooth，Co. Kildare，爱尔兰摘要在本文中，我们提出了一种技术，用于指定和验证通信协议，并证明这种方法通过指定和验证两个基本的通信协议，即TCP和IP，形成了许多分布式系统的基础。所使用的逻辑形式主义是混合直觉线性逻辑，以便使用交换和非交换算子来建模这些协议中的并发和顺序过程。这两个协议的关键属性被证明。保留字： 复杂系统，形式化方法，混合直觉线性逻辑1介绍本文提出了一种描述和验证通信协议的方法。这种方法将用于指定和验证互联网协议（IP）[7]和传输控制协议（TCP）[8]的元素1电子邮件：David.Sinclair@ co mputti n g. 华盛顿哥伦比亚大学Ie2电子邮件：James. may.ie1571-0661 © 2005 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.068256D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255该方法是基于混合直觉线性逻辑，并描述了如何使用这种逻辑来证明这两个协议的一些关键属性。我们以前在[10]中使用交换线性逻辑给出了IP的一个规范。在本文中，我们将此规范扩展到包括TCP的规范和验证。TCP与许多通信协议和分布式系统一样，包括顺序和并发过程。用线性逻辑的交换算子来证明和验证这样的系统是困难的。线性逻辑特别适合于描述基于状态的系统，因为它跟踪每个演绎步骤中使用的资源。混合直觉线性逻辑是线性逻辑的一种变体，包含交换和非交换运算符，因此在必须指定资源消耗顺序的情况下非常有用。混合直觉线性逻辑的非交换算子非常适合于指定具有顺序和并发过程的系统。这项研究的主要贡献是演示如何混合直觉线性逻辑可以用来指定和验证这些类型的分布式系统。在下面的章节中，我们简要介绍IP和TCP以及混合直觉线性逻辑。然后，我们提出了一个大纲，我们的规范的IP和TCP的用户界面，演示的作用，线性算子的公理。我们提出了TCP协议的数据传输组件的规范;最后，我们概述了为证明IP和TCP的关键属性而进行的验证过程。1.1TCP/IP传输控制协议（TCP）和互联网协议（IP）是许多基于网络的应用程序的核心通信堆栈的两个基本元素。这两种协议都是典型的基于状态的分布式系统。IP负责将数据从一个互联网节点传输到另一个互联网节点，但不保证将数据传递到目的地节点。TCP是位于IP之上的协议，它负责在对等TCP实体之间建立端到端的无错误连接。IP没有提供端到端数据可靠性、流控制、排序或主机到主机通信协议中常见的其他服务无论是端到端还是逐跳，都没有校验，并且IP校验和提供的错误检测仅覆盖IP数据包报头，而不是数据本身。在IP中，没有流控制或重传。IP数据包可能会丢失、复制和以任何顺序传递。TCP位于IP之上，其功能是在对等TCP实体之间建立无错误的端到端连接由于IP不提供D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255257为了保证数据传输，TCP提供了所有必要的机制，如数据流控制、确认和重传，以确保数据按顺序传输，没有重复或错误。TCP通过将数据分段并将唯一的序列号与每个段相关联来实现这一点。1.2混合直觉线性逻辑线性逻辑[4]属于子结构逻辑家族，它修改或消除了通常的结构规则收缩，交换和弱化。在线性逻辑中，允许假设被复制的收缩规则和允许假设被丢弃的弱化规则被修改，使得它们不再是结构规则，而是通过使用模态来专门化。这样做的结果是使逻辑具有此外，非交换线性逻辑[1]删除了另一个结构规则，交换，它允许假设重新排序。术语表中的术语是有序的，通常表示为术语列表。在交换线性逻辑中，这些项是不排序的，可以表示为一个多集或一个包含结构交换规则的列表，以允许重新排序中的项混合直觉线性逻辑（MILL）[3]在一个系统中结合了交换块用于捕获MILL序列中的有序项和无序项。MILL中公式的语法定义为：F：= F F |F F |F &F |F F |FF |F −·F |F·− F|！F|B.F.|B.F.|1|不|0|L其中L是文字。块的语法定义为：G：= F|（）|（G; G）|（G，G）定义块的规则是：A，B = B，A A，（B，C）=（A，B），C A，（）= AA;（B;C）=（A;B）;C A;（）= A258D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255"，“和”;“运算符都是结合的，但只有"，”运算符是交换的。没有“;”操作符的块称为空闲块。块是串并行顺序[11]，并有相关的语法树。符号G[ ]表示语法树的一个叶子为空的块。G[D]表示块G[ ]，其中空叶被D替换。弱化、收缩和交换的结构规则的去除意味着合取、析取和蕴涵的普通逻辑算子被交换和非交换线性版本所取代。其中包括：• 交换乘法合取记为A B。当使用时，这两个假设以任何顺序被消耗，并且不再可用。• 非交换乘法合取记为A <$B，表示A之后B的消耗。• 加法连词写作AB。当使用它时，它代表了要消费的假设的决定性选择。• 加性析取式写作A B。当使用它时，它代表了一个外部（非确定性）的选择，作为假设被消费。• 线性蕴涵写为AB，表示消耗A并产生B的过程。• 直接蕴涵记为A−·B。 如果你有两个非对易假设A和A−·B，按这个顺序发生，那么你可以导出假设B，消耗假设A和A−·B。• 复古的含义写为A·−B。如果你有两个非对易的假设A·−B和B，按这个顺序出现，那么你可以导出假设A，消耗假设A·−B和B。这些操作符由图1中的规则定义。我们规范的基础由一系列公理组成，这些公理使用线性算子来表示，它们指定了系统中可以发生的有效转换。对于IP，我们使用普通的交换线性逻辑，因为IP数据报在传输中可能会重新排序。然而，由于接收顺序对TCP很重要，我们在其规范中使用了交换和非交换运算符的组合。1.3验证工具Isabelle定理证明器[6]用于类型检查和验证我们的TCP和IP规范。在线性逻辑中开发的规范是D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255259Γ[π; π]πCΓ[π， π]πC熵AπAIdΓα[A][Γ]Γ[A，B]<$C<$L <$A<$B<$R<$[A;B]<$CLΓ[A<$B]<$C，Γ[A<$B]<$CI; I;IΓ[A]CΓ[AB]C&L1Γ[B]CΓ[AB]C&L2AABΓ[A]<$CΓ[B]<$CΓ[A<$B]<$C阿吉尔AAIR1ΓBABARR2Γα[B]n [r，A][B]CLA、IBABΓ►A∆[B]►C[Γ;A−·B]<$C−·LA;ΓBΓA−·B−·RΓ►A∆[B]►C<$[B·−A;Γ]<$C·−LΓ;ABΓB·−A·−RΓ[（）]CΓ[1]C1L11R无T左规则<$<$TTR <$[0]<$C0L 无0右规则Γ[（）]C[！A]C[！A，！A]C！wr [！A]CΓ[A]C！c r [！A]C ！d ！ΓC！你好！C！p（r是自由的）Γ[A[t/x]]<$CΓ[x.A]CLΓ► ∀x.C R（x∈/FV（Γ））Γ[A]CΓ[x.A]CL（x∈/FV（Γ[（）]，B））Γ<$C [t/x]<$RΓ►∃x.CFig. 1.混合直觉线性逻辑R260D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255最初基于Coq proof assistant[2][9]中的线性逻辑编码，但后来这种编码和处理MILL的扩展都在Isabelle中实现。Isabelle工具提供：• 符号的统一性• 验证类型正确性;以及• 一个半自动化的系统，可以证明规格的属性。1.3.1在IsabelleMILL规范使用Isabelle定理助手使用HOL库进行验证。除了上述优势外，Isabelle/HOL：• 提供预定义的类型，如列表、集合和多重集合;• 提供定义新类型的能力;以及• 除了函数式语言中的逐例定义风格外，还支持归纳定义。MILL在两个理论文件中实现一个文件定义了块的Isabelle/HOL理论，并使用原始递归定义了可以在块上执行的操作。第二个文件定义了MILL的Isabelle/HOL理论。有效的MILL判断由HOL命题T ruelin表示。一个有效的MILL判断由一个线性项块的前件和一个线性项的后件组成。 一个有效的MILL判断被建模为两个有效的MILL判断之间的结果关系。2TCP/IP的定义在本节中，我们简要概述了描述IP和TCP用户界面的主要公理。应该注意的是，完整的规范还包括对连接这些接口的TCP协议的描述，但本文省略了这些公理2.1Internet协议用户界面IP层的用户可以进行两种主要操作D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255261Send（x，y，ttl，m）从节点x向节点y发送消息m，Rcv（x，y，ttl，m）接收从节点x到节点y的消息m，其我们使用三个公理来定义IP层的操作，描述数据报的发送，传输过程中可能的丢失或复制，以及它们的接收。为了提高所有后续公理的可读性，除非在公理中特别说明，否则所有参数都被假设为普遍量化的。首先，发送一条消息会向系统添加一个数据报（一）这里lower是一个将其操作数减少到[0，ttl）范围内的某个非负整数的函数。第二，在传输时，数据报可能被复制或丢失。（二）1是乘法合取的单位，通常用来表示没有对应乘积的资源消耗最后，如果存在寻址到节点y的数据报并且节点y正在监听它，则节点y将接收消息m或该消息的某个损坏版本corrupt（m（三）当然，这里省略了许多与IP相关的问题（最值得注意的是路由和分片），但这个规范为TCP相关属性的验证提供了足够的基础Datagram（x，y，ttl，m）（Datagram（x，y，lower（ttl），m）Datagram（x，y，lower（ttl），Datagram（x，y，ttl，m）Listen（y）Listen（y）（Rcv（x，y，lower（ttl），m）Rcv（x，y，lower（ttl），发送（x，y，ttl，m）数据报（x，y，lower（ttl），m）262D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）2552.2TCP用户操作我们将TCP层的用户界面定义为由以下操作组成new（s，d）创建一个套接字，用于在源互联网地址s和目的地址d之间建立连接。Accept（s，d）接受来自某些互联网地址s的连接到互联网地址d的尝试。write（s，d，m）在从Internet地址s到Internet地址d的连接上写入数据m。Read（s，d，l）尝试从Internet地址s到Internet地址d的连接中读取l个八位字节。如果连接中的八位字节少于l，则Read将读取连接中的所有八位字节。Close（s，d）终止Internet地址% s和d.2.3TCP层接口规范为了描述TCP用户界面，我们定义了一个谓词来描述连接的当前状态Stream（s，d，mw，mr，b）表示从地址s到地址d的连接的一端。s写入的数据被分割为mw（d尚未读取的数据）和mr（d已经读取的数据）。变量b是一个布尔值，一旦流结束（EOS）字符被写入流，它就为假。因此，完整的TCP会话将由一对这样的流组成，s和d各一个。如果互联网地址s和d的两个主机都主动指定连接，或者如果一个主机主动指定连接而另一个主机被动接受来自指定互联网地址的连接，则在互联网地址s和d（四）公理（5）指定了在s处写入一些数据的效果，然后将其附加到先前写入的数据（我们使用（N ew（s，d）<$N ew（d，s））（Accept（s，d）<$N ew（d，s））Stream（s，d，nil，nil，true）返回Stream（d，D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255263国家）。（五）公理（6）指定了在d处读取某些数据的操作，该操作从m1到m2正好传输l个函数drop（n，l）返回一个列表，其中从列表l的开头删除了n个元素。函数take（n，l）返回列表l中前n个元素的列表。（六）最后，公理（7）指定了正常的关闭序列，其中只需要将相关流上的标记从true更改为false。注意，等式（5）和（6）中的前提将确保该流仍然可以被读取，但不能被写入。（七）我们将有效的TCP连接定义为由两个流组成的连接，其中在一个地址读取的数据正是另一个地址写入的数据。在系统中具体说明这一点很简单：有效会话是任何线性命题块（当然包括上面定义的命令），它产生了一致的、完整的流对。定义2.1ValidSessions，d：节点;按x读取，按y读取：（列表数据）;会话：（线性块）sessionStream（s，d，nil，read by y，false）Stream（d，s，nil，readby x，false）.3TCP数据传输协议在本节中，将介绍TCP中数据传输协议的一个简单、朴素的规范。由于目的是表明该协议规范在IP层接口规范之上，具有TCP连接的属性，即传输的数据和传输中的数据形成一个连接，长度（m 1）。Stream（s，d，m1，m 2，b）Read（s，d，l）−·Stream（s，d，drop（l，m1），m2：：Close（s，d）关闭流（s，d，m1，m 2，true）−·流（s，d，m1，m 2，f alse）Stream（s，d，m1，m 2，true）流（s，d，m）−·Stream（s，d，m1：：m，m2，true）264D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255因此，实际TCP系统所需的许多扩展将被忽略。特别地，将假设分段没有丢失，并且将不会发生由于网络互连而导致的分段分段。这些都不是严重的限制，因为零窗口探测可以用来克服丢失的数据，IPv6允许连接确定源和目的地之间的假设所有IP数据报和TCP数据段的校验和都经过初始检查，未通过此测试的数据报和数据段将被丢弃。上一节的TCP用户界面使用单个谓词表示数据传输在协议级别，我们使用两个谓词来表示这种状态，发送方和接收方各一个。TCP协议规范的任务是确保这些谓词在单独维护时，由每个协议公理保持一致的状态。跟踪发送和接收的数据的序列号将是这项任务的核心。表示从s到d的数据流的两个谓词是：SS（s，d，snxt，suna，wbuf，rtq，rwin）这是数据传输到d时s的状态。这里，suna是最早的未确认序列号，snxt是下一个要发送的序列写缓冲器wbuf保存s写入但尚未发送的数据，而重传队列rtq保存已发送但尚未确认的数据。接收器窗口的当前大小是rwin。RS（d，s，rnxt，rwin，rbuf）这是从s接收数据的流上d处的状态。序列号rnxt是要接收的下一个数据的起始序列号。在接收器的缓冲器中留下的可用空间一旦接收到，数据将存储在rbuf中，其中接收窗口的大小。此外，我们使用两个谓词HaveW ritten和HaveRead分别记录发送方写入的所有数据和接收方读取的所有数据。这些是必要的，以便说明TCP协议的基本一致性属性-发送方写入的所有数据最终都会被接收方以相同的顺序读取。定义TCP数据传输协议的公理如下。用户写操作具有将数据附加到发送者的写缓冲器的效果，如公理（8）中所描述的数据序列通过公理（9）离开写入缓冲器，写入缓冲器通过D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255265IPSend谓词。要发送的数据的大小可以根据接收器窗口的当前值以及最大可传输单元（MTU）来确定。然后，在准备IP消息和重新计算发送方状态中的序列号时使用此值。当数据被发送到IP层时，它也被存放在重传队列中，等待确认。（八）（九）（十）（十一）（十二）suna≤r ack≤s nxtSS（s，d，snxt，suna，wbuf，rtq，rwin）IPRecv（d，s，mkAck（rack，rJ赢得SS（s，d，snxt，rack，wbuf，update（rack，rtq），rJ赢得（length（m）≤rwin）<$（sn+length（m）> rnxt）<$（sn≤rnxt）<$RS（d，s，rnxt，rwin，rbuf）<$IPRecv（s，d，mkMsg（sn，m））−·IPSend（d，s，mkAck（sn+length（m），rwin−length（m））<$RS（d，s，sn+length（m），rwin−length（m），rbuf：：drop（（rnxt−sn），m））sn+length（m）≤rnxtRS（d，s，rnxt，rwin，rbuf）<$IPRecv（s，d，mkMsg（sn，m））−·RS（d，s，rnxt，rwin，rbuf）（SS（s，d，snxt，suna，wbuf，rtq，rwin）{HaveW ritten（s，d，hw）}Write（s，d，m）−·SS（s，d，snxt，suna，wbuf：：m，rtq，rwin）具有W ritten（s，长度（m）≤rSS（s，d，snxt，suna，m：：wb，rtq，rwin）IPSend（s，d，mkMsg（snxt，m））发送SS（s，d，snxt+length（m），suna，wb，rtq：：m，rwin−length（m））266D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255（十三）（十四）公理（11）由接收方的确认触发，该确认包含在来自IP层的IPRecv消息中。假设这是在确认一条仍在重传队列中的消息（即序列号在suna和snxt之间的消息），然后我们使用函数update将所有确认的消息从队列中过滤出来公理（10）、（12）和（13）均由从IP层接收到IPRecv信号触发。损坏的消息会被自动拒绝，但如果消息没有损坏，那么它的接受首先取决于在读取缓冲器中有足够的空间（msgSize rwnd），其次取决于尚未接收到消息，基于将其序列号与rnxt进行比较。最后，公理（14）通过从读缓冲器提供数据来处理来自用户层的读请求。此时也更新了谓词HaveRead4工厂规范的验证4.1IP验证IP规范对从一个节点发送到另一个节点的消息几乎没有保证，因为消息可能被损坏，复制甚至丢失。无论IP规范保证的多么少，它确实意味着到达节点的消息必须在某个节点上创建。如果一个节点接收到一个具有正确报头的消息（通过校验和验证），那么某个节点一定发送了一个具有相同报头的消息（当然，实际消息本身可能被损坏）。事实上，如果初始数据报没有丢失，则从节点A发送到节点B的消息可能导致节点B接收到具有正确报头的一个或多个多消息这些信息不会凭空出现。在这里，我们使用（nRcv（x，y，ttl，m））作为接收消息m的n个可能损坏的版本的简写，我们可以通过乘法合取归纳地定义如下：IPRecv（s，d，corrupt（m））−·1（RS（d，s，rnxt，rwin，m：：rb）HaveRead（s，d，hr））Read（s，d，length（m））−·RS（d，s，rnxt，rwin+length（m），rb）HaveRead（s，d，hr：：m）D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255267（Rcv（x，y，ttl，m））=1（Rcv（x，y，ttl，m））=（Rcv（x，y，ttl，m））Rcv（x，y，ttl，corrupt（m））（nRcv（x，y，ttl，m））为了证明消息不是从半空中产生的，我们需要证明：定理4.1NoMidAirMessagesx，y：节点; ttl：nat; m：消息·发送（x，y，ttl，m）发送监听（y）（（nRcv（x，y，ttlJ，m））发送监听（y））发送监听（y）其中ttl我 们 使 用 MILL 对 IP 进 行 的 指 定 允 许 我 们 证 明 这 个 属 性 ， 并 且 在Isabelle/HOL中MILL的公理化允许我们验证证明步骤是正确的。事实上，为了隔离归纳步骤，我们证明了以下引理，该引理断言由Datagram（x，y，ttl，m）表示的传输中的消息可以生成该消息的任意多个接收引理4.2RecvDG闭包：x，y：节点; ttl：nat; m：消息·发送（x，y，m）监听（y）（发送数据报（x，y，m））监听（y）NoMidAirMessages和RecvDGClosure的证明通过n上的归纳进行。自然数的这种归纳性质，以及许多其他常见的性质，是Isabelle/HOL系统的一部分，因为这存在于我们的线性逻辑编码的元级，可以用来构造我们的证明。归纳证明的一般格式在图2和图3中给出。这些图显示了定理助手Isabelle所验证在这些大纲中，使用了以下缩写L=Listen（y）D=数据报（x，y，ttl，m）S=发送（x，y，m）R=Rcv（x，y，ttl，m）Rcv（x，y，ttl，corrupt（m））4.2TCP验证为了验证规范是否满足TCP数据传输的基本要求，我们必须证明上一节中介绍的TCP协议的每个规则都保持了传输268D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255► S LD LCITDDD（nD）（nD）（nD）DnD）DD（nD）（nD）DLL（nD）L（n+1D）LSL（nD）LSL（n+1D）LSL（nD）L► SL（nD）L图二、RecvDGClosure引理的证明（nD）L（nR）L RR（nD），RL（nR）RLDLRL（nD），D，L（nR）RL（n+1D）L（n+1R）LD LRL（nD）L（nR）L斯佩尔（nD）L（nD）L（nR）LSL（nR）LSL（（nR）L）L► SL（（nR）L）L图三. NoMidAirMessages定理的证明数据也就是说，成功关闭的TCP连接将具有这样的特性，即接收方以相同的顺序接收发送方写入的所有数据。这里采用的方法是制定一个由每个公理维护的不变量，并且在所有数据都已发送的最终状态下，这意味着该数据的有序传输和接收。发送方和接收方状态中涉及的每个数据结构具体来说，在传输过程中的任何一点，系统的状态应该如图4所示。写入的每个数据片段（如由HaveW ritten谓词捕获的）应当驻留在写入缓冲器、重传队列、读取缓冲器中，或者由HaveRead谓词捕获总数据不是这些序列的精确连接，因为在重传队列和读缓冲器之间可能存在重叠。重传队列包含已由发送方发送并由接收方确认的数据，但发送方尚未收到确认。为此，我们根据HaveW ritten捕获的数据来定义每个数据结构。不变量本身在经典逻辑中表示，在这里作为嵌入式MILL演绎的元逻辑操作。功能-D. Sinclair，J.Power/Electronic Notes in Theoretical Computer Science 133（2005）255269写入缓冲器RTQs_nxts_una重叠r_nxtr_wnd数据读取缓冲器HaveRead见图4。传输过程中TCP数据结构的状态子列表返回由索引指定的列表的子部分，重传队列将来自重传队列中的消息的数据合并到单个数据列表中，而丢弃是从列表中删除初始段的函数，如索引所指定的。从这一点来看，这是一个相对简单的事情，证明只要这个不变量成立，我们就必须有：（hr：：rbuf：：drop（ rnxt−suna，rtq））：：wbuf）=hw其中hr=子列表（hw，0，length（hr））rbuf=sublist（hw，length（hr），rnxt）子列表（rtq）=sublist（hw，suna，snxt）wbuf=sublist（hw，snxt，length（hw））长度（hr）

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