區塊鏈時代，智慧型合約的安全性被無限放大，乙個小小的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做安全檢測，那麼這上億的損失就能被避免。
關於軟體形式化驗證
軟體開發中一般使用 測試 來找bug，這種方法只能找到bug，不能證明程式沒有bug。形式化驗證是用邏輯來驗證程式的可靠性，就是把一段程式用邏輯的方法證明一遍，證明它能得到預期的結果，沒有bug。一般這類研究主要應用於昂貴的航天器材的作業系統 危險的醫療裝置的程式之中。因為航天器材 醫療裝置牽扯到人...
區塊鏈智慧型合約及形式化驗證平台 VaaS 講解
2017年7月20號，parity 的多簽名錢包合約被曝漏洞，導致3200萬美元的數字貨幣被盜，甚至連 dao bec 這樣的著名專案市值也出現了一夜歸零的慘痛事件，而所有代幣都由智慧型合約生成，所以，毫無疑問，智慧型合約是區塊鏈生態安全中最重要的一環，越來越多的人逐漸意識到區塊鏈智慧型合約安全的重...
中國第一家區塊鏈形式化驗證公司獲種子輪投資
引言 創立於電子科大科技園軍事電子創新加速器的 成都鏈安科技 近日獲得分布式資本種子輪投資，是分布式資本唯一資助的中國第一家專門從事區塊鏈形式化驗證技術研發的公司 區塊鏈作為大資料時代計算機技術的新型應用模式，已經成為金融 軍事安全等科技領域具有劃時代意義的重要成果，將在建設世界現代化數字資訊體系中...