软件所在区块链跨链协议验证方面取得进展

近日，中国科学院软件研究所计算机科学国家重点实验室的科研人员，撰写的题为Formal Analysis of IBC Protocol的研究论文，被网络协议方面的重要国际会议ICNP 2023接收（the 31st IEEE International Conference on Network Protocols）。该研究首次形式化分析了区块链跨链通讯协议IBC（Inter-Blockchain Communication），发现了IBC协议存在的部分问题，并提出了相应的修复建议。 

随着区块链行业的迅速发展，异构而孤立的区块链系统之间亟需数据和功能的互操作性。这种需求最终促使跨链技术的诞生。区块链跨链通讯协议为异构且相互独立的区块链系统之间的通用数据和信息的跨链交换提供支持。IBC协议是目前应用最为广泛的跨链通讯协议之一。在解决区块链系统间连接问题的同时，跨链技术削弱了区块链系统的安全性，导致跨链项目存在一定的安全隐患。

为了提高跨链通讯协议的安全性和可靠性，该研究使用规约语言TLA+对IBC协议核心层（transport， authentication，ordering (TAO) layer）部分进行建模，并使用模型检测工具TLC进行验证。该工作提取了官方文档和IBC协议实际使用中应当满足的性质作为验证目标，并对这些性质进行形式化说明，以帮助开发者和用户更好地理解IBC协议。同时，该工作根据跨链通讯的特点，主要建模了连接握手、通道握手和数据包处理相关的实体和行为，以探究链上模块和链下中继不确定行为对链间安全的影响。该研究通过适当的安全假设和建模抽象使模型在保留核心语义的同时能够被高效验证。 

通过对这些性质的验证，研究发现IBC协议存在两类严重的逻辑错误：连接和通道握手可能由于未能分配标识符或匹配对方链端而无法完成；发送的数据可能由于不正确的通道设计和异常状态处理而无法正确接收或超时。通过对反例的分析和性质的精化，该研究进一步探讨了造成问题的原因并给出相应的修复建议，以帮助开发者更好地设计和实现IBC协议。上述研究发现的所有问题和建议均反馈给协议开发者社区，且大部分得到了确认。 

论文链接  

基于IBC协议的跨链通讯框架图