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

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

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

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

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