Page 165 - 《软件学报》2026年第6期

2484 软件学报 2026 年第 37 卷第 6 期

理和安全性增强等方面具有重要的作用.

表 1 安全目标的形式化

序号 形式化安全目标
∀Mi,Mj ∈ Validator,∀S ∈ Parachains, Mi ∈ S.egressQueue∧Mj ∈ S.egressQueue∧
目标1
(Mi.sendtime < Mj.sendtime) ⇒ Mi.arrivetime < Mj.arrivetime
∀Mi,Mj ∈ Validator,∀D ∈ Parachains, Mi ∈ D.ingressQueue∧Mj ∈ D.ingressQueue∧
目标2
(Mi.sendtime < Mj.sendtime) ⇒ Mi.arrivetime < Mj.arrivetime
∀S ∈ Parachains,∀B ∈ Block,∀Mi,Mj ∈ Validator,(Mi,Mj ∈ B.messages∧ Mi ∈ S.ingreesQueue∧
目标3
Mi ∈ S.ingressQueue) ⇒ (sucess(Mi)∧ sucess(Mj))∨( fail(Mi)∧ fail(Mj))
目标4 ∀Mi ∈ Validator,∀S ∈ Parachains,(Mi ∈ S.ingressQueue) ⇒ Mi < RelayChain.messages
目标5 ∀Mi ∈ Validator,|Mi| ⩽ MaxSize
目标6 ∀S,D ∈ Parachains,(S , D) ⇒ (mkChannel(S,D) ∈ openChannels ⇒ ∃Mi ∈ Validator,Mi.source = S ∧ Mi.dest = D)
∀Mi,Mj ∈ Validator,D ∈ Parachains,(Mi.source , Mj.source) ⇒ (WaitTime(Mi) >
目标7
WaitTime(Mj) ⇒ QueuePosition(D, Mi) < QueuePosition(D,Mj))
∀Mi ∈ Validator,S,D ∈ Parachains,(Mi.source = S ∧Mi.dest = D∧
目标8
Mi ∈ D.ingressQueue) ⇒ Mi ∈ S.egressQueue
∀Mi ∈ Validator,S,D ∈ Parachains,(Mi.sounce = S ∧ Mi,dest = D) ⇒ ((Mi ∈ S.egressQueue∧
目标9
Mi < D.ingressQueue)∨(Mi ∈ D.ingressQueue ⇒ Mi ∈ S.egressQueue))
∀Mi ∈ Validator,S ∈ Parachains,(Mi.source = S )∧ Mi ∈ S.egressQueue ⇒
目标10
∃t.(Mi.timestamp = t)∧(currentTime−t > 24 hours)

目标 4. 跨链消息不会传递到中继链. 每个平行链有能力直接与其他平行链通信, 而无需通过一个中心化的中
继链. 这表明 XCMP 协议需要实现发送链和接收链之间的状态同步等细节.
目标 5. 跨链消息的大小将受到字节数限制. 限制消息大小有助于防止网络拥塞, 同时保护网络中的节点资源,
避免单个节点因处理过大的消息而耗尽内存或计算资源. 此外, 较小的消息可以更快地在网络中传播, 有助于提高
跨链操作的同步效率.
目标 6. 创建通道是启动跨链消息传递队列的前提. 通道具有单向性和唯一性, 它由发送方和接收方的平行链
辨识, 这意味着它是一个单向通道. 一对平行链之间最多可以有两个通道, 一个用于发送消息, 另一个用于接收消息.
目标 7. 收件人将在各个发件人之间公平地接收消息. 收件人在处理跨链消息时, 不会偏好任何特定的发件人.
这表明所有发件人的消息都有平等的机会被接收和处理. XCMP 协议通常会采用队列系统来管理跨链消息, 进而
实现公平性.
目标 8. 到达的消息是在发送链的最终确定的记录中发送的. 确保消息在发送链的最终确定记录中发送, 可以
防止双重花费或其他类型的攻击, 并保证了接收链收到的消息与发送链的最终状态一致, 维护了跨链操作的一致
性. 同时, 由于消息是作为最终确定记录的一部分发送的, 因此可以在发送链上进行追溯和验证.
目标 9. 消息的发送和接收的状态是一致的. 消息发送后无法撤回, 不存在一条消息同时存在未发送, 但是已
被接收两种状态. 无论消息是否发送系统都可以达到最终状态, 因为任何中继链都提供了一致的历史记录.
目标 10. 任何区块的任何传出消息需要保证可用 1 天左右. 为确保消息能够最终到达目的地并被正确执行,
系统需要保持这些消息可用, 以便在需要时重新发送或验证. 同时, 发送平行链的所有节点都会存储这些传出消
息, 直到它们确认这些消息已被中继链或其他目标平行链接收并执行.

4 协议建模及安全分析

为全面、精确地分析 XCMP 协议的安全性, 本节选择 Z 语言进行协议建模. Z 语言的优势在于它是一种数学
化的形式化语言, 能够用精确、无歧义的方式描述系统的行为、结构以及约束条件, 特别适用于复杂系统的建模
与验证. 采用 Z 语言进行建模, 确保能够全面、严谨地分析 XCMP 协议的功能、数据流及其安全属性. 基于这种
形式化分析方法, 本节明确了 XCMP 协议的形式化安全目标, 以确保协议设计和实现过程中符合既定的安全目标.