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

吕永阳 等: XCMP 协议的形式化验证与改进: 提升跨链交互安全性 2483

2.2 协议工作流
本节分析现有 XCMP 协议的工作流, 帮助读者清晰地理解其跨链消息发送与接收过程, 步骤可对应图 2.
(1) 触发请求: 平行链 S 中的用户调用智能合约, 触发跨链数据的发送请求.
(2) 区块构建: Collator S 接收到跨链数据后, 将其打包成跨链消息, 并将该消息放入平行链 S 的出口队列, 待平
行链 S 的出口队列中积累了一定数量的跨链消息, Collator S 会构建新的平行链区块.
(3) 记录元数据: 随后, Collator S 将消息的元数据 (metadata) 记录在中继链 (relay chain) 上, 包括消息的哈希值、
发送信息及相关 Merkle 证明, Merkle 证明是一种验证数据完整性和来源的技术, 通过提供该证明, 接收链的节点
可以确认接收到的消息是有效的, 并且确实来自特定发送链的指定区块.
(4) 发送请求和消息接收: Collator D 节点定期向所有其他收集者节点发送请求, 查询是否有新的跨链消息. 当
Collator D 节点在请求中发现平行链 S 发送跨链消息时, 它会通过已建立的单向通道将该消息添加到平行链 D 的
入口队列.
(5) 消息验证: Validator D 接收到跨链消息调入队列的消息后, 通过中继链提供的元数据来验证消息的真实性,
确保消息在发送链上已被最终确认.
(6) 打包区块: 验证通过后, Collator D 将队列中的跨链消息打包成区块, 并执行相应的操作.
(7) 区块验证和区块添加: 执行完毕后, Collator D 将队列中的跨链消息打包成区块提交给 Validator D 验证, 验
证通过后, 该区块被添加到中继链尾部, 完成跨链消息的传递和处理.
3 安全假设和安全目标

在对 XCMP 协议的分析中, 本文主要关注在跨链数据传递过程中的平行链的收集者和验证者所带来的安全
问题, 目标是尽可能多地研究收集者和验证者的行为, 以更全面地分析用户可能面临的安全风险.
3.1 安全假设
本文的分析是基于对 XCMP 协议的参与者和实体的以下安全假设.
(1) 区块链的假设: XCMP 协议为独立区块链提供了一种相互通信的机制, 负责确保链间的可靠性, 不考虑区
块链内的拜占庭错误, 如共识机制的失败. 此外, XCMP 协议适用于不同共识机制的异构区块链, 包括概率最终共
识算法. 因此, 本文假设所涉及的区块链是安全的.
(2) 诚实和攻击的假设: XCMP 协议中验证者和收集者被认为是半诚实的, 他们遵守协议规则, 但会尝试从执
行协议过程中获取额外信息. 他们不会主动去破坏协议的执行, 但会尽可能地利用协议的漏洞来获取他们不应该
访问的信息. 而中继链和钓鱼者是诚实的, 他们严格遵守协议的每一步, 不会尝试获取任何额外的信息, 也不会尝
试干扰协议的正常执行, 完全按照协议的设计意图行事. 由于平行链共享中继链的安全和钓鱼者的存在, 本文认为
跨链消息传递过程是安全的. 因此, 本文重点研究分析 XCMP 协议实体的不诚实行为所引发的安全问题.
3.2 安全目标

XCMP 协议为实现跨链消息传递, 需要满足以下安全目标 [14] . 表 1 详细列出了这些安全目标的形式化结果,
而表中各符号的具体含义将在第 4.1 节中进行详细阐述.
目标 1. 平行链的跨链消息按顺序到达另一平行链. 如果消息不是按照发送顺序到达, 可能会导致接收链的状
态与发送链的状态不一致. 此外, 在资产转移的场景中, 如果消息乱序到达, 攻击者可能会利用这个漏洞进行双花
攻击 [38] ; 同时, 许多区块链应用都有一定的业务逻辑, 这些逻辑可能依赖于事件的顺序.
目标 2. 平行链按顺序接收传入的跨链消息. 内部平行链可能根据它们自己的逻辑对消息进行延迟或重新排
序. 但是, 它们必须按照中继链给出的一致历史记录所确定的顺序接收消息. 平行链总是接收由头位于更早的中继
链块中的平行链块发送的消息.
目标 3. 平行链接收另一平行链发送的同一区块中所有的消息, 要么全部成功接收, 要么全部接收失败. 跨链
消息传递的原子性要求一系列操作要么全部执行, 要么全部不执行, 不会出现中间状态. 它在一致性维护、错误处