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

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

接着, 在上述工具和安全目标的指导下, 对 XCMP 协议进行了系统的建模, 从而为后续的安全分析提供了坚实依据.
4.1 协议建模
在本节中, 将首先进行模式定义, 然后基于此进行操作定义, 以系统性地完成对 XCMP 协议的建模.
4.1.1 模式定义
(1) 基本类型
在建模中, 首先定义了 XCMP 协议中涉及的基本类型, 包括 Parachain (平行链)、DOT (数字货币)、string (字
符串类型) 以及 Block (区块).
[Parachain, DOT, string, Block]
这些基本类型构成了消息和状态的基础. 在此基础上, 消息类型被进一步定义, 包括以下关键组成部分. 具体
见代码 1 和代码 2.
● S, D: Parachain 源平行链 S 和目标平行链 D, 明确消息的起点和目的地.
● CCdata: string 跨链数据完整记录和传递跨链消息中的所有必要操作信息.
● timestamp: Z 时间戳记录了消息的生成时间.
● size: Z 消息大小.
● metadata: Metadata 元数据中包括消息的哈希值 (messageHash)、源平行链和目标平行链的标识.
代码 1. Metadata.

messageHash: string
S, D: Parachain

代码 2. Message.

S: Parachain
D: Parachain
CCdata: string
timestamp: Z
size: Z
metadata: Metadata
size≤maxMessageSize
metadata.messageHash=Hash(S, D, CCdata, timestamp)
Metadata.S=S
Metadata.D=D

(2) 平行链状态模式
平行链状态通过 ParachainState 模式进行描述, 具体如代码 3, 包括以下两个部分.
● ingressQueue: seq Message 入口队列用于存储接收到的消息, 等待处理.
● egressQueue: seq Message 出口队列存储待发送的消息, 准备发送至目标平行链.
代码 3. ParachainState.

ingressQueue: seq Message
egressQueue: seq Message
∀ m:Message | m ∈ ran ingressQueue ∨ m ∈ ran egressQueue
· m.size≤maxMessageSize