软件所在区块链跨链协议验证方面取得进展
文章来源： | 发布时间：2023-11-10 | 【打印】 【关闭】
近日，中国科学院软件研究所计算机科学国家重点实验室的研究论文Formal Analysis of IBC Protocol被网络协议方面的重要国际会议ICNP 2023接收 (the 31st IEEE International Conference on Network Protocols)。第一作者为硕士生魏秋阳，通讯作者为朱雪阳副研究员。论文首次形式化分析了区块链跨链通讯协议IBC（Inter-Blockchain Communication），发现了IBC协议存在的部分问题并提出了相应的修复建议。
随着区块链行业的迅速发展，异构而孤立的区块链系统之间迫切需求一种数据和功能的互操作性，这种需求最终促使了跨链技术的诞生。区块链跨链通讯协议为异构且相互独立的区块链系统之间的通用数据和信息的跨链交换提供支持。IBC协议是目前应用最为广泛的跨链通讯协议之一。在解决区块链系统间连接问题的同时，跨链技术也削弱了区块链系统的安全性，导致跨链项目存在一定的安全隐患。
基于IBC协议的跨链通讯框架图
为了提高跨链通讯协议的安全性和可靠性，论文使用规约语言TLA+对IBC协议核心层（transport, authentication, ordering (TAO) layer）部分进行了建模，并使用模型检测工具TLC进行验证。论文提取了官方文档和IBC协议实际使用中应当满足的性质作为验证目标，并对这些性质进行形式化说明，以帮助开发者和用户更好地理解IBC协议。同时，论文根据跨链通讯的特点，主要建模了连接握手、通道握手和数据包处理相关的实体和行为，以研究链上模块和链下中继不确定行为对链间安全的影响。论文也通过适当的安全假设和建模抽象使模型在保留核心语义的同时能够被高效验证。
通过对这些性质的验证，论文发现了IBC协议存在两类严重的逻辑错误：连接和通道握手可能由于未能分配标识符或匹配对方链端而无法完成；发送的数据可能因为不正确的通道设计和异常状态处理而无法正确接收或超时。通过对反例的分析和性质的精化，论文进一步探讨了造成问题的原因并给出相应的修复建议，以帮助开发者更好地设计和实现IBC协议。所有发现的问题和建议均反馈给协议开发者社区，其中大部分得到了确认。
IBC协议开发者社区：https://github.com/cosmos/ibc
论文下载：http://lcs.ios.ac.cn/~zxy/papers/c23icnp-wei.pdf
TLA+代码地址：https://github.com/michwqy/IBC-TLA
