區塊鏈時代 形式化驗證的應用

2022-08-05 12:18:10 字數 1132 閱讀 3362

區塊鏈時代,智慧合約的安全性被無限放大,一個小小的bug就能導致上億美元的損失。美鏈(bec)近日被爆出安全漏洞,被黑客用以太坊erc-20智慧合約中batchoverflow漏洞攻擊,引發**閃崩,當日幣價幾乎歸0。除了美鏈,據英國和新加坡的研究人員統計,超過34000個智慧合約都有可被利用的安全隱患。

智慧合約的安全問題頻頻亮紅燈,黑客簡單的一串數字就能套利千萬,讓人血本無歸。想要保證智慧合約能夠100%的正確,只有形式化驗證(formal verification)可以確保這些漏洞完全被檢測。具體的方式我們用美鏈來**一下。

美鏈到底出了什麼安全漏洞?

美鏈這個安全漏洞其實非常簡單!美鏈智慧合約中一個batchtransfer函式, 主要目的是實現bec token的批量轉賬: 將固定整數數量(_value) 轉賬到一批接收賬號的陣列裡 (_receivers). 為了實現這樣的批量轉賬, bec的開發人員, 首先計算需要轉賬的總金額, 計算的公式是:

總金額 (amount) = 需要給每個接收方轉賬的額度(_value) x 總共需要轉賬的賬戶個數 (_cnt)

然後在確保傳送方擁有足夠的餘額後, 給每個接收方傳送轉賬的額度.

但是, 出了什麼問題呢?

在計算 amount = _value x _cnt 的過程中, 開發人員並沒有考慮到256位整數資料溢位的可能性,因此黑客們, 依靠這個漏洞, 成功的餘額不足的情況下, 依然從賬戶中轉走了總計2²⁵⁶個bec token。  

用形式化驗證方法輕鬆檢測漏洞

事後看來好像美鏈這個安全漏洞看起來是個愚蠢的錯誤,但是類似bec的安全漏洞其實很容易忽略,而智慧合約上一個小的程式上的疏忽,就能導致上千萬甚至上億的損失。

自動化的形式化驗證平臺很可能能幫助檢測和避免類似的錯誤。來看看certik的自動化形式化驗證平臺是如何做到的。

將這段**提交到certik的驗證引擎,新增幾個標籤,certik的自動化驗證引擎能夠輕易的檢測到bec的溢位錯誤。certik的形式化驗證引擎能夠處理這些標籤並且能夠根據標籤來檢查**實現的正確性。如果美鏈的智慧合約提交之前能夠被certik做安全檢測,那麼這上億的損失就能被避免。