【儀表網(wǎng) 研發(fā)快訊】近日，中國科學院軟件研究所計算機科學國家重點實驗室的科研人員，撰寫的題為Formal Analysis of IBC Protocol的研究論文，被網(wǎng)絡協(xié)議方面的重要國際會議ICNP 2023接收(the 31st IEEE International Conference on Network Protocols)。該研究首次形式化分析了區(qū)塊鏈跨鏈通訊協(xié)議IBC(Inter-Blockchain Communication)，發(fā)現(xiàn)了IBC協(xié)議存在的部分問題，并提出了相應的修復建議。
 

　　隨著區(qū)塊鏈行業(yè)的迅速發(fā)展，異構而孤立的區(qū)塊鏈系統(tǒng)之間亟需數(shù)據(jù)和功能的互操作性。這種需求最終促使跨鏈技術的誕生。區(qū)塊鏈跨鏈通訊協(xié)議為異構且相互獨立的區(qū)塊鏈系統(tǒng)之間的通用數(shù)據(jù)和信息的跨鏈交換提供支持。IBC協(xié)議是目前應用最為廣泛的跨鏈通訊協(xié)議之一。在解決區(qū)塊鏈系統(tǒng)間連接問題的同時，跨鏈技術削弱了區(qū)塊鏈系統(tǒng)的安全性，導致跨鏈項目存在一定的安全隱患。
 

　　為了提高跨鏈通訊協(xié)議的安全性和可靠性，該研究使用規(guī)約語言TLA+對IBC協(xié)議核心層(transport， authentication，ordering (TAO) layer)部分進行建模，并使用模型檢測工具TLC進行驗證。該工作提取了官方文檔和IBC協(xié)議實際使用中應當滿足的性質作為驗證目標，并對這些性質進行形式化說明，以幫助開發(fā)者和用戶更好地理解IBC協(xié)議。同時，該工作根據(jù)跨鏈通訊的特點，主要建模了連接握手、通道握手和數(shù)據(jù)包處理相關的實體和行為，以探究鏈上模塊和鏈下中繼不確定行為對鏈間安全的影響。該研究通過適當?shù)陌踩僭O和建模抽象使模型在保留核心語義的同時能夠被高效驗證。
 

　　通過對這些性質的驗證，研究發(fā)現(xiàn)IBC協(xié)議存在兩類嚴重的邏輯錯誤：連接和通道握手可能由于未能分配標識符或匹配對方鏈端而無法完成；發(fā)送的數(shù)據(jù)可能由于不正確的通道設計和異常狀態(tài)處理而無法正確接收或超時。通過對反例的分析和性質的精化，該研究進一步探討了造成問題的原因并給出相應的修復建議，以幫助開發(fā)者更好地設計和實現(xiàn)IBC協(xié)議。上述研究發(fā)現(xiàn)的所有問題和建議均反饋給協(xié)議開發(fā)者社區(qū)，且大部分得到了確認。
 

基于IBC協(xié)議的跨鏈通訊框架圖