閃電網(wǎng)絡(luò)的概念富有創(chuàng)新和實驗性，不過可能導(dǎo)致用戶資金損失的 bug 仍有待發(fā)現(xiàn)。近日，一隊科研人員發(fā)布了對比特幣閃電網(wǎng)絡(luò)的形式化驗證結(jié)果。

這篇論文在由愛丁堡大學(xué)的安格洛斯·齊亞伊亞斯（Aggelos Kiayias）和奧弗依斯·利托斯（Orfeas Litos）發(fā)表。齊亞伊亞斯還是區(qū)塊鏈公司 IOHK 的首席科學(xué)家，這家公司為新生支付網(wǎng)絡(luò)的底層安全做出了許多貢獻(xiàn)。

迄今為止，閃電網(wǎng)絡(luò)尚未在數(shù)學(xué)上進(jìn)行過正式的安全測試，這一測試可以建立一個計算機(jī)系統(tǒng)在數(shù)學(xué)上的安全程度。這篇題為 “A Composable Security Treatment of the Lightning Network” 的論文認(rèn)為，如今閃電網(wǎng)絡(luò)已經(jīng)被用于保護(hù)至少 8500 萬美元的真實資金，但其代碼規(guī)范缺乏形式化驗證是一件 “極其嚴(yán)重的事”。

“因此，我們的措施詳細(xì)地描述了如何基于底層賬本上資產(chǎn)實現(xiàn)協(xié)議安全保證?！?論文解釋道。

他們所做的這個過程被稱作 “形式化驗證（formal security）”。這一方法在加密貨幣領(lǐng)域非常流行，而且有助于確定代碼的安全性。形式化安全并沒有被部署在每個加密項目上，因為部署 “形式化驗證” 需要高深的知識，部署成本很高。

堅實的規(guī)范

研究者結(jié)果是積極的，這表明為使支付系統(tǒng)正常工作而堆積在一起的底層加密技術(shù)是正確的。“系統(tǒng)所有的重要安全部分都是可靠的，這是意料之中的結(jié)果?！?利托斯告訴 CoinDsek。

這究竟意味著什么？利托斯和齊亞伊亞斯審查了閃電網(wǎng)絡(luò)的規(guī)范，每一款閃電網(wǎng)絡(luò)軟件都必須滿足這些規(guī)則，以向網(wǎng)絡(luò)的其他部分發(fā)起支付。

利托斯告訴 CoinDesk：“主要的結(jié)論是閃電網(wǎng)絡(luò)和比特幣一樣安全?！?/p>

為了得出這一結(jié)論，他們研究了構(gòu)成閃電網(wǎng)絡(luò)的密碼學(xué)。密碼學(xué)是由數(shù)學(xué)算法組成的，這些算法提供了網(wǎng)絡(luò)上的安全和隱私基礎(chǔ)。在閃電網(wǎng)絡(luò)中，密碼學(xué)是把支付系統(tǒng)黏在一起的膠水，最后的結(jié)果是允許一個人把比特幣轉(zhuǎn)賬給其他人。

因此，研究者們研究了閃電網(wǎng)絡(luò)底層不同的密碼學(xué)技術(shù)，包括數(shù)字簽名。這一技術(shù)對于比特幣而言，意味著比特幣只能被有著正確私鑰的用戶產(chǎn)出。

“閃電網(wǎng)絡(luò)用戶只可能在用于比特幣的數(shù)字簽名和哈希函數(shù)出錯時才可能會丟失資金。”利托斯說，“使用底層的真實賬戶允許我們精準(zhǔn)定位閃電網(wǎng)絡(luò)運行參數(shù)間的安全聯(lián)系。特別的，我們對 ‘閃電網(wǎng)絡(luò)用戶需要多久檢查一次區(qū)塊鏈，尤其是進(jìn)行連續(xù)多次交易時’ 這個問題給出了確切的答案?！?/p>

規(guī)格并非軟件

雖然形式化驗證是重要的一步，但它只存在于閃電網(wǎng)絡(luò)的藍(lán)圖上，尚未由開發(fā)者落實在任何一款軟件上。

雖然論文聲稱閃電網(wǎng)絡(luò) “和比特幣一樣安全”，這不意味著軟件本身也是安全的。這也許聽起來是微不足道的區(qū)別，但實際上區(qū)別極大。

有 3 款主要閃電網(wǎng)絡(luò)執(zhí)行了專家們的意見，分別是 Acinq’s Eclair、Blockstream’s c-lightning 和 Lightning Lab’s lnd。

“我們的分析基于形式化驗證，而不是實際執(zhí)行。因此，并不能排除各種實現(xiàn)中的錯誤，目前僅僅是排除了規(guī)范（specification）中的錯誤而已?！?利托斯表示。

利托斯提到，未來的形式化分析可能最終被用于研實際的代碼。

“理想情況下，通過對代碼進(jìn)行形式化驗證來證明其符合規(guī)范，會在系統(tǒng)中提升信任程度。但在那之前，我們?nèi)匀恍枰粋€機(jī)器可讀的規(guī)范版本。”
來源： CoinDesk中文?