閃電網路的概念富有創新和實驗性，不過可能導致使用者資金損失的 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）中的錯誤而已。” 利托斯表示。

利托斯提到，未來的形式化分析可能最終被用於研實際的程式碼。“理想情況下，透過對程式碼進行形式化驗證來證明其符合規範，會在系統中提升信任程度。但在那之前，我們仍然需要一個機器可讀的規範版本。” 他表示。