区块链跨链协议IBC形式化分析

魏秋阳; 赵旭峰; 朱雪阳; 张文辉; 卢奕函

引用本文:	魏秋阳,赵旭峰,朱雪阳,张文辉,卢奕函.区块链跨链协议IBC形式化分析.软件学报,2025,36(11):4953-4974

【打印本页】【下载PDF全文】【查看/发表评论】【EndNote】【RefMan】【BibTex】

←前一篇|后一篇→

过刊浏览高级检索

本文已被：浏览 2028次下载 2262次	码上扫一扫！
分享到：微信更多字体:加大+\|默认\|缩小-
区块链跨链协议IBC形式化分析
魏秋阳^1,2,3,4, 赵旭峰^1,2,4, 朱雪阳^1,2,4, 张文辉^1,2,4, 卢奕函^1,2,3,4
1.基础软件与系统重点实验室 (中国科学院软件研究所), 北京 100190;2.计算机科学国家重点实验室 (中国科学院软件研究所), 北京 100190;3.国科大杭州高等研究院, 浙江杭州 310024;4.中国科学院大学, 北京 100049

摘要:

自从比特币诞生以来, 区块链技术在许多领域产生了重大的影响. 然而, 异构、孤立的区块链系统之间缺乏有效的通信机制, 限制了区块链生态的长远发展. 因此, 跨链技术迅速发展并成为了新的研究热点. 由于区块链的去中心化本质和跨链场景的复杂性, 跨链技术面临巨大的安全风险. IBC协议是目前最广泛使用的跨链通信协议之一. 对IBC协议进行形式化分析, 以期帮助开发者更可靠地设计和实现跨链技术. 使用基于时序逻辑的规约语言TLA+对IBC协议进行形式化建模, 并使用模型检测工具TLC验证IBC协议应满足的重要性质. 通过对验证结果深入分析, 发现一些影响数据包传输和代币转移正确性的重要问题, 并提出建议来消除相关安全风险. 这些问题已经向IBC开发者社区汇报, 其中大部分得到确认.

关键词: 区块链跨链 IBC协议形式化分析 TLA+

DOI：10.13328/j.cnki.jos.007356

分类号:TP311

基金项目:国家自然科学基金(62072443); 南方电网网络空间安全联合实验室资助项目(037800KC23090002)

Formal Analysis of Cross-chain Protocol IBC

WEI Qiu-Yang^1,2,3,4, ZHAO Xu-Feng^1,2,4, ZHU Xue-Yang^1,2,4, ZHANG Wen-Hui^1,2,4, LU Yi-Han^1,2,3,4

1.Key Laboratory of Systems Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;2.State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;3.Hangzhou Institute for Advanced Study, University of Chinese Academy of Sciences, Hangzhou 310024, China;4.University of Chinese Academy of Sciences, Beijing 100049, China

Abstract:

Since the advent of Bitcoin, blockchain technology has profoundly influenced numerous fields. However, the absence of effective communication mechanisms between heterogeneous and isolated blockchain systems has hindered the advancement and sustainable development of the blockchain ecosystem. In response, cross-chain technology has emerged as a rapidly evolving field and a focal point of research. The decentralized nature of blockchain, coupled with the complexity of cross-chain scenarios, introduces significant security challenges. This study proposes a formal analysis of the IBC (inter-blockchain communications) protocol, one of the most widely adopted cross-chain communication protocols, to assist developers in designing and implementing cross-chain technologies with enhanced security. The IBC protocol is formalized using TLA+, a temporal logic specification language, and its critical properties are verified through the model-checking tool TLC. An in-depth analysis of the verification results reveals several issues impacting the correctness of packet transmission and token transfer. Corresponding recommendations are proposed to mitigate these security risks. The findings have been reported to the IBC developer community, with most of them receiving acknowledgment.

Key words: blockchain cross-chain IBC (inter-blockchain communications) protocol formal analysis TLA+