在公鏈領域，儘管以太坊的技術非常強悍，但對於智慧型合約的漏洞，也似乎力不從心。之前有來自新加坡和英國的幾位研究者指出：以太坊上超3.4萬個以太坊智慧型合約可能存在容易被攻擊的漏洞。以太坊的智慧型合約有漏洞，早已不是什麼新聞。所謂智慧型合約，其實就是一串**，這串**與其他軟體**並沒有什麼顯著的區別。只是這些**很多時候都和「錢」有關係，所以一旦這些**存在漏洞，被攻擊以後將會產生巨大損失。
2016 年 5 月，the dao遭受到了黑客利用遞迴呼叫以太坊傳送漏洞的攻擊，造成巨大損失。
2017 年 7 月 19 日， parity wallet 的多重簽名錢包（「multi-sig」）**中存在的漏洞被黑客所利用，持有 eth 大額餘額的三個錢包賬戶已被入侵。
2023年4月22日，bec 智慧型合約批量轉賬函式中有一行**存在 bug，導致了溢位漏洞。黑客利用這一漏洞攻擊美鏈的智慧型合約，成功生成並轉出了數以億計巨大數量的bec token。
2023年5月，攻擊者利用以太坊節點鑑權缺陷，惡意呼叫介面盜取代幣，持續時間長達兩年，單被盜的且還未轉出的以太幣價值就高達現價 2 千萬美金，還有代幣種類 164 種，總價值難以估計。
上面僅僅是部分舉例，相信這些因智慧型合約漏洞被攻擊的案例不是第乙個，也不會是最後乙個。這不得不讓人們生疑，為何號稱安全的區塊鏈，怎麼在黑客面前如此不堪一擊。說好的價值網際網路呢？說好的安全性呢？
智慧型合約，安全漏洞是大問題
也許有人會說，這些智慧型合約都是第三方開發者弄出來的漏洞，和底層公鏈有什麼關係？這就好比一條商業街，商業街上面的商戶被盜了，這條商業街的管理者說，是你商戶自己家的防盜門不好，關我商業街屁事？可是如果一條商業街上，商戶動輒就會發生偷盜失竊的事情，還有商戶和使用者來嗎？如果沒有了商戶和使用者，這條商業街還開不開呢？
從區塊鏈發展來看，區塊鏈之所以能從位元幣的「炒幣」特徵中抽離出來，很大一部分原因是「智慧型合約」讓人們看到了區塊鏈的技術價值和應用價值。但就目前而言，區塊鏈的真實應用沒普及起來，但智慧型合約的漏洞事件倒是先流行起來了。
由於這些智慧型合約，很多都是和資金有關。所以黑客更喜歡尋找這些智慧型合約的漏洞，通過攻擊進行獲利。如果智慧型合約的漏洞問題無法得到很大的改善，談及區塊鏈的技術應用純屬空中樓閣。沒有人敢把真正有價值的東西，放置在乙個沒有太多安全保障的「價值網際網路」上。
智慧型合約漏洞，該如何應對？
其實，智慧型合約安全漏洞頻現並非偶然，當前數字貨幣市場魚龍混雜，智慧型合約缺乏有效的監管，缺少安全審計流程，其**安全性與邏輯漏洞僅靠開發人員人工審核，難免存在隱患和漏洞。因此，部署智慧型合約之前，必須要對其進行全面深入的**安全審計，盡可能消除漏洞、降低風險。
在對這些智慧型合約進行安全審計中，形式化驗證是經常被提及的一種方法。所謂形式化驗證，就是指根據某個或某些形式化規範或屬性，使用數學的方法證明其正確性或非正確性。最早是在硬體上開始普及的。當年intel的pentium cpu浮點運算單元出錯(fdiv bug)，數以萬計的cpu不得不**和替換，給intel造成了巨大損失。
從那之後，intel開始在其晶元設計中廣泛採用形式化方法。計算機硬體巨頭如ibm，amd， nvidia等等也都是形式化方法的使用者。我國的玉兔號月球車控制系統和我國第乙個自主研發的空間飛行器嵌入式實時作業系統spaceos，也都是通過形式化方法驗證其正確性。
形式化驗證，如何幫助檢查智慧型合約漏洞？
舉個例子來說，對於一段智慧型合約程式，我們可以從它所有可能的輸入 (例如函式引數的組合) 和初始狀態 (例如狀態變數初始值的組合) 出發，根據每條語句的語義，逐句推導出程式的所有可能的結束狀態 (例如合約執行結束後的狀態變數的值和產生的 event log)，並檢查合約的所有輸入、初始狀態、結束狀態的組合是否都和形式化規範保持一致。
這有點類似於柯南破案那樣，一步步地推演。只不過，這裡所有的定義都是通過嚴格的數學語言描述，推導和檢查也是嚴格的數學推導和證明。根據待驗證的系統及其形式化規範的複雜程度，推導和證明即可以手工構造，也可能可以由機器自動產生。
在實踐中，推導和證明無法進行下去往往意味著設計和實現中存在不符合規範的 bug。通過分析推導和證明卡殼的位置和原因，可以定位出 bug 在設計和實現中的具體位置和成因。這樣的方法，讓數字資產領域中中嚴格意義上的規避錯誤、避免損失成為可能。
形式化驗證，並未萬能
不過，這種形式化驗證（formal verification）與程式測試（testing）是兩碼事。程式測試能證明錯誤的存在,但不能證明錯誤不存在。舉例說明：2023年，澳大利亞的科學家使用形式化方法對工業級作業系統sel4微核心進行了完整功能性驗證，驗證方式同時以形式化驗證和程式測試兩種方式分別展開，驗證的結果是：形式化方法共發現460多個bug，而程式測試只發現了16個bug。
不過需要注意的是：程式測試是在「真實」環境裡進行的，形式化驗證只是數學層面，在「真實」環境中的測試是形式化驗證無法取代的。也就是說，即便經過了形式化驗證，也並不能說明智慧型合約就不會出現漏洞了。
只要是人編寫的**，就會有漏洞。形式化驗證只能幫助開發者，用數學的方法來驗證能驗證的部分，對於不能驗證的部分，形式化驗證也解決不了問題。所以，智慧型合約的安全問題，依舊任重而道遠。
區塊鏈裡的智慧型合約安全
在我寫這遍文章的時候，距離eos曝出漏洞已經有三天時間，區塊鏈行業熱點來的快去的也快，每每出現安全相關問題，都會給整個行業帶來 自從我開始關注區塊鏈行業以來，安全事故有增無減，交易平台 智慧型合約 共識機制等等都成了安全事故的中心。智慧型合約本質是一段執行在區塊鏈網路中的 它完成使用者所賦予的業務邏...
solidity編寫智慧型合約的安全漏洞問題（一）
回顧 3 個底層呼叫call delegatecall callcode 和 3 個轉幣函式call.value send transfer call call 用於 solidity 進行外部呼叫，例如呼叫外部合約函式.call bytes4 keccak somefunc params para...
三星研究院 發現騰訊的「阿喀琉斯之踵」，網際網路營銷
中國主要網際網路企業2009銷售額 百萬美元 及過去四年股價波動 中國網際網路行業發展可分為跑馬圈地 大浪淘沙 移動網際網路三個階段。這一階段的中國網際網路企業發展，以 燒錢 和 跑馬圈地 為特點，各企業尚未找到合理的盈利模式，只是以ebay amazon yahoo等公司為藍本進行複製。網際網路企...