閃電網絡的概念富有創新和實驗性，不過可能導致用戶資金損失的 bug 仍有待發現。近日，一隊科研人員發布了對比特幣閃電網絡的形式化驗證結果
閃電網絡的概念富有創新和實驗性，不過可能導致用戶資金損失的 bug 仍有待發現。近日，一隊科研人員發布了對比特幣閃電網絡的形式化驗證結果。
這篇論文在由愛丁堡大學的安格洛斯·齊亞伊亞斯(Aggelos Kiayias)和奧弗依斯·利托斯(Orfeas Litos)發表。齊亞伊亞斯還是區塊鏈公司 IOHK 的首席科學家，這家公司為新生支付網絡的底層安全做出了許多貢獻。
迄今為止，閃電網絡尚未在數學上進行過正式的安全測試，這一測試可以建立一個計算機系統在數學上的安全程度。這篇題為 “A Composable Security Treatment of the Lightning Network” 的論文認為，如今閃電網絡已經被用于保護至少 8500 萬美元的真實資金，但其代碼規范缺乏形式化驗證是一件 “極其嚴重的事”。
“因此，我們的措施詳細地描述了如何基于底層賬本上資產實現協議安全保證。” 論文解釋道。
他們所做的這個過程被稱作 “形式化驗證(formal security)”。這一方法在加密貨幣領域非常流行，而且有助于確定代碼的安全性。形式化安全并沒有被部署在每個加密項目上，因為部署 “形式化驗證” 需要高深的知識，部署成本很高。
堅實的規范
研究者結果是積極的，這表明為使支付系統正常工作而堆積在一起的底層加密技術是正確的。“系統所有的重要安全部分都是可靠的，這是意料之中的結果。” 利托斯告訴 CoinDsek。
這究竟意味著什么?利托斯和齊亞伊亞斯審查了閃電網絡的規范，每一款閃電網絡軟件都必須滿足這些規則，以向網絡的其他部分發起支付。
利托斯告訴 CoinDesk：“主要的結論是閃電網絡和比特幣一樣安全。”
為了得出這一結論，他們研究了構成閃電網絡的密碼學。密碼學是由數學算法組成的，這些算法提供了網絡上的安全和隱私基礎。在閃電網絡中，密碼學是把支付系統黏在一起的膠水，最后的結果是允許一個人把比特幣轉賬給其他人。
因此，研究者們研究了閃電網絡底層不同的密碼學技術，包括數字簽名。這一技術對于比特幣而言，意味著比特幣只能被有著正確私鑰的用戶產出。
“閃電網絡用戶只可能在用于比特幣的數字簽名和哈希函數出錯時才可能會丟失資金。”利托斯說，“使用底層的真實賬戶允許我們精準定位閃電網絡運行參數間的安全聯系。特別的，我們對 ‘閃電網絡用戶需要多久檢查一次區塊鏈，尤其是進行連續多次交易時’ 這個問題給出了確切的答案。”
規格并非軟件
雖然形式化驗證是重要的一步，但它只存在于閃電網絡的藍圖上，尚未由開發者落實在任何一款軟件上。
雖然論文聲稱閃電網絡 “和比特幣一樣安全”，這不意味著軟件本身也是安全的。這也許聽起來是微不足道的區別，但實際上區別極大。
有 3 款主要閃電網絡執行了專家們的意見，分別是 Acinq’s Eclair、Blockstream’s c-lightning 和 Lightning Lab’s lnd。
“我們的分析基于形式化驗證，而不是實際執行。因此，并不能排除各種實現中的錯誤，目前僅僅是排除了規范(specification)中的錯誤而已。” 利托斯表示。
利托斯提到，未來的形式化分析可能最終被用于研實際的代碼。
“理想情況下，通過對代碼進行形式化驗證來證明其符合規范，會在系統中提升信任程度。但在那之前，我們仍然需要一個機器可讀的規范版本。” 他表示。（Alyssa Hertig）
