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

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


                 区块链系统转移到另一个区块链系统, 使资产从源区块链中烧掉, 并在目标区块链上进行声明来在网络之间无缝
                 交换资产. Ding  等人  [43] 提出的  Lilac 支持并行资产锁定. 它用所有参与用户生成的多个子凭据替换了                 HTLC  中唯
                 一的资产解锁凭据, 并且该子凭据的序列被用作完整的资产解锁凭据. 用户只有在所有资产都被锁定时才能获得
                 完整的凭证, 且凭证构建过程与资产被锁定的顺序无关, 因此当用户并行锁定其资产时, 可以保证原子性.
                 Vishwakarma 等人  [44] 提出一种资产转移技术    CrossLedger, 他们使用了一种新的资产支持者选择           (AFS)、信任建
                 立  (TE) 和资产转移与确认     (ATC) 算法, 且满足不可否定性、不可链接性、保密性、原子性和互操作性. 这些跨链
                 协议都是通过测试和经验主义来证明其有效性, 缺乏严格、强力的保证. 本文利用形式化方法验证与分析                                  XCMP
                 跨链协议, 利用    Z  语言构建协议模型并利用基于严格数学证明的模型检测工具进行安全性分析, 针对发现的问题
                 在  Polkadot 平台的基础上提出扩展方案, 并再次通过形式化建模与分析为扩展方案的正确性和安全性提供严格的
                 保证.
                  7.2   区块链形式化
                    采用形式化技术对区块链系统或其内部机制进行精确建模和全面的安全性分析, 已成为确保系统安全性的关
                 键策略  [45−50] . 形式化技术用于验证基于区块链提出的方案或协议的安全性与可靠性. 例如, Dong                   等人  [51] 提出了一
                 种基于区块链的工业互联网无证书跨域认证机制, 并利用自动形式化验证工具                           Scyther 证明了该方案的安全性.
                 Afzaal 等人  [52] 提出了一种新的基于信任的区块链众包共识协议, 并利用模型检验技术对其进行形式化验证, 检查
                 属性是否满足或违反要求, 以确保协议的属性符合预定的安全标准. Wang                        等人  [53] 提出一种基于区块链     (BC-
                 based) 的可信传输系统, 并引入了一种结合区块链可信属性的                BC-based DH (Diffie-Hellman) 协议, 接着, 他们利用
                 自动验证形式化分析工具, 验证了传统            DH  协议所缺乏的保密性和完全前向保密性             (PFS). Wang  等人  [54] 提出了一
                 种用于生产资源形式化分析的模型数据驱动                 (DD) 框架, 该方法将形式建模阶段的时间成本降低了至少                  75%.
                    此外, 形式化技术可用于对现有的区块链协议进行安全性分析, 为开发人员发现并改进安全漏洞提供帮助.
                 Feng  等人  [55] 通过形式化  FIDO UAF  协议的安全假设和目标并在      ProVerif 中进行验证, 发现了两个对于安卓        FIDO
                 应用的实际攻击. Wei 等人      [22] 利用时间逻辑规范语言     TLA+形式化    IBC  跨链协议的   3  个主要组件, 并使用模型检
                 测工具   TLC  验证其重要的要求, 发现了其中的问题. Neupane 等人          [56] 对发布索赔、批准或拒绝索赔的过程中涉及
                 的链码进行形式化验证, 确保区块链中交易的安全可靠处理. Afzaal 等人                  [57] 使用过程分析工具包     (PAT) 对以太坊
                 2.0  核心的信标链的状态初始化、证明和最终确定检查点的过程进行了形式化验证, 提高人们对信标链的正确性
                 和可靠性的信心. 与上述工作相似, 本文利用             Z  语言提出  XCMP  协议的形式化模型, 通过描述其应满足的安全目
                 标并利用    Z/EVES  辅助工具分析其安全性. 在分析出协议存在的安全漏洞后, 本文针对发现的安全漏洞提出
                 E-XCMP  协议, 同时, 本文利用    Z  语言和  Scyther 工具对提出的协议进行安全性分析, 验证了           E-XCMP  的正确性.

                  8   总 结
                    为提升   XCMP  协议的安全性, 增强      Polkadot 网络的跨链能力, 本文采用      Z  语言的形式化方法, 对跨链通信协
                 议  XCMP  的安全性及可靠性进行验证和改进. 基于正在持续完善的                  XCMP  协议, 本文首先梳理了相关实体和协
                 议流程, 并总结提炼出      XCMP  的安全目标. 基于     Polkadot 平台, 本文对  XCMP  协议及其安全目标进行了        Z  语言的
                 形式化建模, 并使用支持       Z  语言的自动化验证工具        Z/EVES  来探测可能存在的错误, 最终识别出          3  个未满足的安
                 全目标. 接着, 针对    Z/EVES  发现的这些安全缺陷, 本文对       XCMP  协议的实体功能进行了扩展, 并引入了承诺机制、
                 监督机制和轮询机制, 提出了        E-XCMP  协议. 为了验证   E-XCMP  协议的实用性和有效性, 本文使用         Scyther 和  Z/EVES
                 对其进行了形式化建模和模型检测, 并进行安全分析. 结果表明, 本文提出的                       E-XCMP  协议解决了    3  个未满足的
                 安全目标, 添加了轮询检测、智能验证、超时重传等功能, 并证明了                     E-XCMP  协议满足机密性、认证性、完整性
                 和非否认性等多个安全属性, 能有效解决重放攻击、拒绝服务攻击、延迟攻击等问题. 通过本文提出的                                 E-XCMP
                 协议, Polkadot 网络的跨链功能将得到增强, 从而为构建更复杂、功能更丰富的去中心化应用提供了坚实的支撑.
                 本文基于   Z  语言的分析也证明了形式化方法在像跨链协议等复杂场景中的有效性. 在分析和建模过程中, 本文所
   181   182   183   184   185   186   187   188   189   190   191