Page 162 - 《软件学报》2026年第6期
P. 162

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


                    跨链消息传递      (XCMP) 是  Polkadot 协议的一个子集. 它定义了在除了共享中继链的安全之外没有其他的信任
                 假设的情况下, 消息如何得以在平行链之间传递, 具有跨链消息传递、去中心化、可扩展性等优点, 是                               Polkadot 跨
                 链系统的核心.
                  1.2   Pedersen  承诺
                    Pedersen  承诺  [28] 是构建在椭圆曲线密码学基础之上, 利用椭圆曲线上的点和群运算来实现. Pedersen                 承诺的
                 核心思想是允许一个用户         (承诺者) 对一个数值进行承诺, 而这个承诺在某个未来时间之前是不可打开的, 即外界
                 无法知道承诺的具体内容. 同时, 承诺者也无法在不被发现的情况下改变承诺的内容. Pedersen                       承诺的核心公式为:

                                                       C = r×G +v×H,
                 其中, C  是生成的承诺值, G    和  H  是特定椭圆曲线上的生成点, r 是盲因子, 即一个随机选择的数, 用于提供隐藏性.
                 v 是原始信息, 即承诺者想要隐藏的数据.
                    Pedersen  承诺具有同态性、隐藏性和绑定性这           3  个核心性质. 其中, Pedersen  承诺的同态性使得可以在不解
                 密的情况下对加密数据进行操作. 而隐藏性和绑定性基于离散对数问题的困难性假设. 隐藏性确保承诺值不会泄
                 露任何关于消息      v 的信息, 绑定性则确保承诺者无法在不被发现的情况下更改消息                     v. 这些特性使得    Pedersen  承
                 诺在区块链和数字货币中被广泛应用.
                  1.3   Z  语言
                    在本文中, 主要使用      Z  语言进行形式化建模. Z     语言  [29−33] 是一种形式化描述语言, 它以经典集合论和一阶谓词
                 逻辑为基础, 提供了一种称为模式的结构, 以此描述一个规格说明的状态空间和操作. Z                         语言采用严格的数学理论,
                 从而产生简明、精确、无歧义且可证明的规格说明. 该语言的关键思想是把软件开发中的需求规格说明阶段和软
                 件设计阶段分开, 采用忽略过程而强调功能描述的操作抽象, 旨在帮助开发人员和用户找出规格说明的不一致、
                 不完整之处, 更安全地设计和实现软件和协议等技术. Z                语言的核心构造是       Z  模式, 包括状态模式和操作模式两种
                 类型. 状态模式用于定义系统某部分的状态空间及其约束, 而操作模式则用于描述系统某部分的行为特征, 通过对
                 比操作前后的状态值来定义操作的特性.
                    Z  规格说明是   Z  语言的形式化表达方式, 用于精确描述和建模软件系统的行为与结构. 它由一系列模式                          (称为
                 “scheme”) 组成, 每个模式定义一个抽象对象或操作, 并用谓词判定描述给出新的对象或操作的语义约束. 在                            Z  语
                 言的模式中, “?”和“!”分别表示输入和输出. 由于           Z  语言是基于集合论的, 其支持的数据类型均为集合, 如               Z 表示
                 整数集合,   P 表示其后跟随的集合的幂集, “↔”用于描述集合之间的关系, “→”表示从一个集合映射到另一个集合
                 的函数, seq  表示特殊函数类型序列. Z      语言的模式可以被视为抽象数据集合并通过类似于逻辑运算符的各种运算
                 符进行操作, 从而组合成新的         Z  模式, 新的  Z  模式继承原模式的一切属性和约束. 通过            Include、and  等可以实现
                 不同模式之间的关联和新模式的产生, 如 Include S          表明该模式包含模式        S, 即包含模式   S  的声明和谓词约束, 用于
                 从简单的模式组合出更为复杂的模式; S and T           表明该模式是模式      S  和模式  T  的交集, 即包含模式    S  和模式  T  的声
                 明且同时满足二者的谓词约束.
                  1.4   Z/EVES  工具
                    在本文中, 主要使用      Z/EVES  辅助工具编写    Z  语言并进行编写、验证和分析. 目前存在的支持               Z  语言的工具
                 和解析器包括     Z/EVES [27] 、ProofPower [34] 等, 用于帮助开发人员编写、分析和验证     Z  语言规格. Z/EVES  是一款专
                 为  Z  语言开发设计的辅助工具, 它提供了一个集成开发环境                (IDE), 支持语法高亮, 方便用户编写和修改           Z  语言,
                 同时内置自动推理机制, 检查规格的自洽性和完整性, 通过模型检查技术, 验证规格是否满足指定的性质, 找出潜
                 在的错误. Z/EVES 具有强大的交互式定理证明功能和广泛的应用场景. 它能够处理复杂的逻辑推导, 并支持用户
                 通过命令手动完成复杂证明. 此外, Z/EVES 的自动证明能力也可以加快验证过程, 对于简单目标的验证非常有效.
                    Z/EVES  提供了一个结构化界面, 用于验证形式化规范的正确性与完备性. 每个段落被赋予两个状态. 第                            1  列
                 显示语法和语义检查结果, “?”表示暂未检查, “Y”表示没有错误, “N”表示存在错误. 第                   2  列反映证明状态, “?”表示
                 没有成功检查, “N”表示存在未证明的目标, “Y”表示所有关联目标都已证明.
   157   158   159   160   161   162   163   164   165   166   167