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

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

● 元数据中的消息哈希值 (messageHash) 与根据跨链消息 M 计算出的哈希值一致.
如果存在满足上述条件的元数据, 则验证通过. Collator D 将队列中的消息打包成区块并执行相应的操作.

代码 9. ValidateMessage.
ΞRelaychainState
M?: Message
Block, Block': seq Message

∃ metadata: Metadata
· metadata ∈ ran metadatas
∧ metadata.S=M?.S

∧ metadata.D=M?.D
∧ metadata.messageHash
=Hash(M?.S, M?.D, M?.CCdata, M?.timestamp)
∧ 〈M?〉
⇒Block'=Block
(5) 区块验证模式 (ValidateBlock)
在区块验证模式中, 执行完相应的操作后, 平行链 D 的收集者将区块提交给验证者验证, 验证通过后, 该区块
被添加到中继链尾部, 完成跨链消息的传递和处理. 具体如代码 10 所示.
代码 10. ValidateBlock.

ΔRelaychainState
Block?: seq Message

Blocktest(Block?)
⇒validatedBlocks'=validatedBlocks ∧ 〈Block?〉

4.2 安全分析
在对现有 XCMP 协议进行形式化建模后, 本文定义了一系列形式化安全目标, 以确保跨链消息传递的正确性
和可靠性. 这些目标旨在规范协议行为, 确保消息的顺序、完整性、公平性和持久性, 为协议的设计与验证提供明
确指导, 并帮助识别潜在问题. 本文依据这 10 个安全目标进行了详尽的验证, 并通过 Z 语言建模检验协议在关键
安全目标上的符合性. 表 2 列出了 XCMP 协议在这些目标上的满足情况, √表示满足, ×表示不满足.

表 2 安全目标的形式化结果

序号 安全目标 形式化结果
目标1 平行链的跨链消息按顺序到达另一平行链 √
目标2 平行链按顺序接收传入的跨链消息 √
目标3 平行链接收另一平行链发送的同一区块中所有的消息, 要么全部成功接收, 要么全部接收失败 ×
目标4 跨链消息不会传递到中继链 √
目标5 跨链消息的大小将受到字节数限制 √
目标6 创建通道是启动跨链消息传递队列的前提 √
目标7 收件人将在各个发件人之间公平地接收消息 ×
目标8 到达的消息是在发送链的最终确定的记录中发送的 √
目标9 消息的发送和接收的状态是一致的 √
目标10 任何区块的任何传出消息需要保证可用1天左右 ×