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

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

根据表 2 可知, 现有协议不满足目标 3、目标 7 和目标 10 这 3 条形式化安全目标. 下面展示了针对这 3 个安
全目标所编写的定理, 并对其进行了形式化验证. 这些定理的验证结果进一步佐证了表 2 的结论, 即现有 XCMP
协议未能满足这些安全目标.
(1) 目标 3: 完整接收消息
针对目标 3 编写的定理在 Z/EVES 中的验证结果如图 3 所示. 根据验证结果显示, 现有的 XCMP 协议无法满
足目标 3. 违反安全目标 3 表明, 由于缺乏完备周到的异常消息检测和处理机制, 而导致接收消息形成平行链块的
完整性和安全性无法保证. 以一次消息发送为例, 平行链 S 为发送链, 平行链 D 为接收链, 平行链 S 的收集者收集
整理交易数据, 打包成候选区块 M 并放入出口队列. 候选区块中的交易消息 Mi 按顺序从出口队列发送, 经过平行
链 S 和平行链 D 的单向通道, 由平行链 D 以中继链给出的一致历史记录所确定的顺序接收消息, 并放入自己的入
口队列中, 以待被打包进区块. 若一切顺利, 平行链 D 的收集者将队列中的跨链消息 Mi 打包进区块, 同时每个跨
链消息 Mi 会执行平行链 D 上相应的智能合约, 完成跨链数据共享传递. 然而在非理想情况下, 跨链消息 Mi 可能
会在发送过程中遭遇恶意篡改、丢失或重放等问题, 导致平行链 D 接收到的消息与平行链 S 发送的消息不一致.
这种情况违反了协议的安全性和完整性要求, 可能导致系统状态不一致, 进而引发跨链操作错误. 例如, 如果平行
链 D 未能接收到所有相关消息, 可能会出现资产转移失败、重复转移或丢失等问题, 从而影响系统的可靠性和数
据完整性. 确保消息的完整接收是维护系统一致性和完整性的关键, 缺乏有效的完整接收机制将使得重放攻击等
威胁得以实施, 造成系统状态混乱, 并可能导致操作错误或重复.

图 3 目标 3 定理验证结果

(2) 目标 7: 公平消息接收
针对目标 7 编写的定理在 Z/EVES 中的验证结果如图 4 所示. 根据验证结果, 现有的 XCMP 协议无法满足目
标 7. 为了保证发送平行链永远不会无限期地等待他们的消息被看到, 接收平行链需要在各个发送平行链之间公
平地接收消息. 然而, 现有的轮询并未说明具体的选择机制, 且缺乏严密的检测机制以保证平行链遵循轮询机制,
这可能会导致某一发送平行链的消息长期无法得到响应, 跨链消息将永远堆积在入口队列, 跨链消息传递无法进
行. 除此之外, 攻击者可能会实施拒绝服务攻击, 通过发送大量垃圾消息来使有效消息的处理延迟或被阻塞.

图 4 目标 7 定理验证结果

(3) 目标 10: 消息持久化
针对目标 10 编写的定理在 Z/EVES 中的验证结果如图 5 所示. 验证结果显示, 现有的 XCMP 协议无法满足