近日，中國(guó)科學(xué)院軟件研究所計(jì)算機(jī)科學(xué)國(guó)家重點(diǎn)實(shí)驗(yàn)室的科研人員，撰寫的題為Formal Analysis of IBC Protocol的研究論文，被網(wǎng)絡(luò)協(xié)議方面的重要國(guó)際會(huì)議ICNP 2023接收（the 31st IEEE International Conference on Network Protocols）。該研究首次形式化分析了區(qū)塊鏈跨鏈通訊協(xié)議IBC（Inter-Blockchain Communication），發(fā)現(xiàn)了IBC協(xié)議存在的部分問(wèn)題，并提出了相應(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)間連接問(wèn)題的同時(shí)，跨鏈技術(shù)削弱了區(qū)塊鏈系統(tǒng)的安全性，導(dǎo)致跨鏈項(xiàng)目存在一定的安全隱患。
為了提高跨鏈通訊協(xié)議的安全性和可靠性，該研究使用規(guī)約語(yǔ)言TLA+對(duì)IBC協(xié)議核心層（transport， authentication，ordering (TAO) layer）部分進(jìn)行建模，并使用模型檢測(cè)工具TLC進(jìn)行驗(yàn)證。該工作提取了官方文檔和IBC協(xié)議實(shí)際使用中應(yīng)當(dāng)滿足的性質(zhì)作為驗(yàn)證目標(biāo)，并對(duì)這些性質(zhì)進(jìn)行形式化說(shuō)明，以幫助開發(fā)者和用戶更好地理解IBC協(xié)議。同時(shí)，該工作根據(jù)跨鏈通訊的特點(diǎn)，主要建模了連接握手、通道握手和數(shù)據(jù)包處理相關(guān)的實(shí)體和行為，以探究鏈上模塊和鏈下中繼不確定行為對(duì)鏈間安全的影響。該研究通過(guò)適當(dāng)?shù)陌踩僭O(shè)和建模抽象使模型在保留核心語(yǔ)義的同時(shí)能夠被高效驗(yàn)證。?
通過(guò)對(duì)這些性質(zhì)的驗(yàn)證，研究發(fā)現(xiàn)IBC協(xié)議存在兩類嚴(yán)重的邏輯錯(cuò)誤：連接和通道握手可能由于未能分配標(biāo)識(shí)符或匹配對(duì)方鏈端而無(wú)法完成；發(fā)送的數(shù)據(jù)可能由于不正確的通道設(shè)計(jì)和異常狀態(tài)處理而無(wú)法正確接收或超時(shí)。通過(guò)對(duì)反例的分析和性質(zhì)的精化，該研究進(jìn)一步探討了造成問(wèn)題的原因并給出相應(yīng)的修復(fù)建議，以幫助開發(fā)者更好地設(shè)計(jì)和實(shí)現(xiàn)IBC協(xié)議。上述研究發(fā)現(xiàn)的所有問(wèn)題和建議均反饋給協(xié)議開發(fā)者社區(qū)，且大部分得到了確認(rèn)。?
