微信服务号

微信订阅号

2025年7月13日 21:54 星期日
首页 > 过刊浏览>年第卷第期 >1-22. DOI:10.13328/j.cnki.jos.007356
PDF HTML阅读 XML下载 导出引用 引用提醒
区块链跨链协议IBC形式化分析
作者:
中图分类号:

TP311

基金项目:

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


Formal Analysis of Cross-chain Protocol IBC
Author:
  • WEI Qiu-Yang

    WEI Qiu-Yang

    Key Laboratory of System Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;Hangzhou Institute for Advanced Study, UCAS, Hangzhou 310024, China;University of Chinese Academy of Sciences, Beijing 100049, China
    在期刊界中查找
    在百度中查找
    在本站中查找
  • ZHAO Xu-Feng

    ZHAO Xu-Feng

    Key Laboratory of System Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;University of Chinese Academy of Sciences, Beijing 100049, China
    在期刊界中查找
    在百度中查找
    在本站中查找
  • ZHU Xue-Yang

    ZHU Xue-Yang

    Key Laboratory of System Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;University of Chinese Academy of Sciences, Beijing 100049, China
    在期刊界中查找
    在百度中查找
    在本站中查找
  • ZHANG Wen-Hui

    ZHANG Wen-Hui

    Key Laboratory of System Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;University of Chinese Academy of Sciences, Beijing 100049, China
    在期刊界中查找
    在百度中查找
    在本站中查找
  • LU Yi-Han

    LU Yi-Han

    Key Laboratory of System Software (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;State Key Laboratory of Computer Science (Institute of Software, Chinese Academy of Sciences), Beijing 100190, China;Hangzhou Institute for Advanced Study, UCAS, Hangzhou 310024, China;University of Chinese Academy of Sciences, Beijing 100049, China
    在期刊界中查找
    在百度中查找
    在本站中查找
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [44]
    • | |
  • 引证文献
    • | |
  • 文章评论
    摘要:

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

    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.

    参考文献
    [1] Zheng ZB, Xie SA, Dai HN, Chen XP, Wang HM. Blockchain challenges and opportunities: A survey. Int’l Journal of Web and Grid Services, 2018, 14(4): 352–375.
    [2] Nakamoto S. Bitcoin: A peer-to-peer electronic cash system. Satoshi Nakamoto Institute, 2008.
    [3] Wood G. Ethereum: A secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper, 2014, 151: 1–32.
    [4] Xie TC, Zhang JH, Cheng ZR, Zhang F, Zhang YP, Jia YZ, Boneh D, Song D. zkBridge: Trustless cross-chain bridges made practical. In: Proc. of the 2022 ACM SIGSAC Conf. on Computer and Communications Security. Los Angeles: ACM, 2022. 3003–3017. [doi: 10.1145/3548606.3560652]
    [5] Swan M. Blockchain: Blueprint for A New Economy. Sebastopol: O’Reilly Media, Inc., 2015.
    [6] Ou W, Huang SY, Zheng JJ, Zhang QL, Zeng G, Han WB. An overview on cross-chain: Mechanism, platforms, challenges and advances. Computer Networks, 2022, 218: 109378.
    [7] Gervais A, Karame GO, Wüst K, Glykantzis V, Ritzdorf H, Capkun S. On the security and performance of proof of work blockchains. In: Proc. of the 2016 ACM SIGSAC Conf. on Computer and Communications Security. Vienna: ACM, 2016. 3–16. [doi: 10.1145/2976749.2978341]
    [8] Nguyen CT, Hoang DT, Nguyen DN, Niyato D, Nguyen HT, Dutkiewicz E. Proof-of-stake consensus mechanisms for future blockchain networks: Fundamentals, applications and opportunities. IEEE Access, 2019, 7: 85727–85745.
    [9] Thomas S, Schwartz E. A protocol for interledger payments. 2015. https://interledger.org/interledger.pdf
    [10] Robinson P. Survey of crosschain communications protocols. Computer Networks, 2021, 200: 108488.
    [11] Aurora Labs. Rainbow bridge. https://rainbowbridge.app/transfer
    [12] Belchior R, Vasconcelos A, Guerreiro S, Correia M. A survey on blockchain interoperability: Past, present, and future trends. ACM Computing Surveys, 2022, 54(8): 168.
    [13] Kwon J, Buchman E. Cosmos whitepaper. A Network of Distributed Ledgers, 2019, 27: 1–32.
    [14] Goes C. The interblockchain communication protocol: An overview. arXiv:2006.15918, 2020.
    [15] Lee SS, Murashkin A, Derka M, Gorzny J. SoK: Not quite water under the bridge: Review of cross-chain bridge hacks. In: Proc. of the 2023 IEEE Int’l Conf. on Blockchain and Cryptocurrency (ICBC). Dubai: IEEE, 2023. 1–14. [doi: 10.1109/ICBC56567.2023.10174993]
    [16] Poly Network. Honour, exploit, and code: How we lost 610M dollar and got it back. 2021. https://medium.com/poly-network/honour-exploit-and-code-how-we-lost-610m-dollar-and-got-it-back-c4a7d0606267
    [17] Wormhole. Wormhole incident report. 2022. https://wormholecrypto.medium.com/wormhole-incident-report-02-02-22-ad9b8f21eec6
    [18] Basin D, Dreier J, Hirschi L, Radomirovic S, Sasse R, Stettler V. A formal analysis of 5G authentication. In: Proc. of the 2018 ACM SIGSAC Conf. on Computer and Communications Security. Toronto: ACM, 2018. 1383–1396. [doi: 10.1145/3243734.3243846]
    [19] Cosmos Network. Cosmos market capitalization. 2024. https://cosmos.network/ecosystem/tokens
    [20] Wei QY, Zhao XF, Zhu XY, Zhang WH. Formal analysis of IBC protocol. In: Proc. of the 31st Int’l Conf. on Network Protocols (ICNP). Reykjavik: IEEE, 2023. 1–11. [doi: 10.1109/ICNP59255.2023.10355573]
    [21] Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Boston: Addison-Wesley Longman Publishing Co. Inc., 2002.
    [22] Cao L, Song B. Blockchain cross-chain protocol and platform research and development. In: Proc. of the 2021 Int’l Conf. on Electronics, Circuits and Information Engineering (ECIE). Zhengzhou: IEEE, 2021. 264–269. [doi: 10.1109/ECIE52353.2021.00063]
    [23] Neha? Z, Bobot F, Tucci-Piergiovanni S, Delporte-Gallet C, Fauconnier H. A TLA+ formal proof of a cross-chain swap. In: Proc. of the 23rd Int’l Conf. on Distributed Computing and Networking. Delhi: ACM, 2022. 148–159. [doi: 10.1145/3491003.3491006]
    [24] Pillai B, Biswas K, Hóu Z, Muthukkumarasamy V. Burn-to-Claim: An asset transfer protocol for blockchain interoperability. Computer Networks, 2021, 200: 108495.
    [25] Pillai B, Hóu Z, Biswas K, Muthukkumarasamy V. Formal verification of the Burn-to-Claim protocol for blockchain interoperability. Journal of Latex Class Files, 2021, 14(8): 1–15.
    [26] Herlihy M, Liskov B, Shrira L. Cross-chain deals and adversarial commerce. Proc. of the VLDB Endowment, 2019, 13(2): 100–113.
    [27] Zhang JS, Gao JB, Li Y, Chen ZM, Guan Z, Chen Z. Xscope: Hunting for cross-chain bridge attacks. In: Proc. of the 37th IEEE/ACM Int’l Conf. on Automated Software Engineering. Rochester: ACM, 2022. 171. [doi: 10.1145/3551349.3559520]
    [28] Wood G. Polkadot: Vision for a heterogeneous multi-chain framework. White Paper, 2016, 21(2327): 4662.
    [29] Polkadot. Introduction to cross-consensus message format (XCM). 2024. https://wiki.polkadot.network/docs/learn-xcm
    [30] GitHub, Inc. IBC relayer in rust. 2024. https://github.com/informalsystems/hermes
    [31] Kobeissi N, Bhargavan K, Blanchet B. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In: Proc. of the 2017 IEEE European Symp. on Security and Privacy (EuroS&P). Paris: IEEE, 2017. 435–450. [doi: 10.1109/EuroSP.2017.38]
    [32] Zhang JJ, Yang L, Gao XM, Tang GG, Zhang JY, Wang Q. Formal analysis of QUIC handshake protocol using symbolic model checking. IEEE Access, 2021, 9: 14836–14848.
    [33] Prabhu S, Chou KY, Kheradmand A, Godfrey PB, Caesar M. Plankton: Scalable network configuration verification through model checking. In: Proc. of the 17th USENIX Symp. on Networked Systems Design and Implementation. Santa Clara: USENIX Association, 2020. 953–968.
    [34] Zhang YM, Xu H, Xue CJ, Kuo TW. Probabilistic analysis of network availability. In: Proc. of the 30th Int’l Conf. on Network Protocols (ICNP). Lexington: IEEE, 2022. 1–11. [doi: 10.1109/ICNP55882.2022.9940438]
    [35] Yin JQ, Zhu HB, Fei Y. Specifica?湩捯????卤???啲湩牦敩捣潡癴敩牯慮戠汯敦?潴灨瑥椠浚楡獢琠楰捲?却敯湣摯偬愠捷歩整瑨???ぁ火金??桯瑵瑲灮獡???杦椠瑃桯畭扰?捴潥浲?捓潣獩浥潮獣?椠扡据?椠獔獥畣敨獮?????戬爠?嬰??崬??椵琨?甩戺???渱挲??儳甲攳献琼楢潲渾?愳戶潝甠瑁?灨牴潡潲映?漬映?慡捨歯湯潲眠汅攮搠杆敯浲敭湡瑬???づ????档瑡瑴灩獯???杮楤琠桶略扲?捦潩浣?桴祩灯敮爠汯敦搠杍救牔?氠慰扲獯?祯畣楯?椠扩据?獐潬汵楳摃楡瑬礭?椮猠獗畩敲獥?????扐牥?孳??嵡??楃瑯?畭扵???湡捴????匬㈠??′儱甬攠猱琱椹漨渲?愺戠漱电琸?漓渱?挰欶渮漼睢汲放摛朳攷偝愠捋歵敫瑨???の????栬琠瑚灩獢???杶椠瑋栬甠打?捤潹浫?捶漠獒洬漠獒?楺扩据?楒献猠畖敥獲??ど???扩牯?嬠?て崠??楴瑳?畵扦???湆捔??卯潮浳敥瑮桳極湳朠?捲潯湴景畣獯楬渠杷?慴扨漠畔瑌???協が?????卡?????ふ????桡瑬琠灳獥???杮楧琮栠畉扮?挠潓浩?捨潡獶浹漠獒?椠扥捤?椠獉獮畦敯獲???ど?扳爠?孮?ㄠ嵃??楥瑲?略扴???渠捩????却づ????卥????卹潳浴敥?楳渮挠潃湨獡業猺琠敓湰捲楩敮獧??水?有???栮琠琷瀷猓???朠楛瑤桯畩戺?挼潰浤?捩漾猱洰漮猱?椰户振?椷猸猭申攭猰?????戴爴?嬭??崹??楰瑤?畩戾???湲挾?″??匠????却潨海敡?灴潥猠獓椬戠求敵?浨業獡瑮愠歅攬猠???の????栬琠瑍灩獬???杶楩瑣栠畚戬?捓潴浯?捬潫獯浶潳獫?椠扉挬?楗獩獤畤敥獲?????扡牭?ir A. Formal specification and model checking of the tendermint blockchain synchronization protocol (short paper). In: Proc. of the 2nd Workshop on Formal Methods for Blockchains. Los Angeles, 2020. 10: 1–10: 8. [doi: 10.4230/OASIcs.FMBC.2020.10]
    [39] Grundmann M, Hartenstein H. Verifying payment channels with TLA+. In: Proc. of the 2022 IEEE Int’l Conf. on Blockchain and Cryptocurrency (ICBC). Shanghai: IEEE, 2022. 1–3. [doi: 10.1109/ICBC54727.2022.9805487]
    [40] GitHub, Inc. Interchain Standards (ICS) for the Cosmos network & interchain ecosystem. 2020. https://github.com/cosmos/ibc
    [41] GitHub, Inc. Inter-Blockchain Communication Protocol (IBC) implementation in Golang. 2024. https://github.com/cosmos/ibc-go
    [42] GitHub, Inc. IBC in solidity. 2024. https://github.com/hyperledger-labs/yui-ibc-solidity
    [43] Back A, Corallo M, Dashjr L, Friedenbach M, Maxwell G, Miller A, Poelstra A, Timón J, Wuille P. Enabling blockchain innovations with pegged sidechains. 2024. https://blockstream.com/sidechains.pdf
    [44] GitHub, Inc. Public code of our formal analysis of IBC protocol. https://github.com/michwqy/ibc-tla
    [45] GitHub, Inc. TLA+ language support for Visual Studio Code. https://github.com/tlaplus/vscode-tlaplus
    [46] GitHub, Inc. ICS 03/04: Some questions about handshake. 2023. https://github.com/cosmos/ibc/issues/1001
    [47] GitHub,
    相似文献
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

魏秋阳,赵旭峰,朱雪阳,张文辉,卢奕函.区块链跨链协议IBC形式化分析.软件学报,,():1-22

复制
相关视频

分享
文章指标
  • 点击次数:410
  • 下载次数: 157
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2024-08-25
  • 最后修改日期:2024-10-14
  • 在线发布日期: 2025-05-14
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第20226571位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号