近日，中國科學院軟件研究所計算機科學國家重點實驗室的科研人員，撰寫的題為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協議。上述研究發現的所有問題和建議均反饋給協議開發者社區，且大部分得到了確認。?
