软件学报

作者：魏秋阳，赵旭峰，朱雪阳，张文辉，卢奕函

单位：魏秋阳，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;国科大杭州高等研究院, 浙江 杭州 310024;中国科学院大学, 北京 10004911,赵旭峰，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004902,朱雪阳，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004903,张文辉，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004904,卢奕函，基础软件与系统重点实验室 (中国科学院 软件研究所), 北京 100190;计算机科学国家重点实验室 (中国科学院 软件研究所), 北京 100190;国科大杭州高等研究院, 浙江 杭州 310024;中国科学院大学, 北京 10004905

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

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

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

来源：2025年第11期

《软件学报》期刊编辑部

查看软件学报杂志2025年第11期