“一支穿雲箭，千軍萬馬來相見”。

在經歷三個月“漫長熊市”後，從4月中旬開始，EOS的一個拉昇，形成了數字貨幣市場大牛市的壯觀景象。可是在美鏈BeautyChain（BEC）的智慧合約漏洞被黑客利用、隨意刷幣，SmartMesh（SMT）智慧合約再次爆出相同漏洞，並在OKex上出現大規模異常交易後，整個市場隨即進入大幅震盪的情形。在瞭解事情經過後，我們不禁要問，為何小小的漏洞會引發如此大的動靜？

1

智慧合約的技術缺陷和解決方案

智慧合約的2個缺陷

其實這件事情集中暴露了以以太坊為代表的區塊鏈2.0技術的兩個缺點：

• 智慧合約不夠智慧；

• 智慧合約缺少安全保障機制和安全工具。

區塊鏈2.0的核心是智慧合約，而當黑客能夠輕而易舉地利用智慧合約漏洞為所欲為時，實質上相當於動搖了整個大廈的根基，因此造成數字貨幣市場的恐慌也在所難免。

加法溢位漏洞：一個加法帶來的血案！

我們可以將SMT漏洞歸納為一句話：利用加法的溢位漏洞，規避安全檢查從而獲得鉅額收益。首先看看這段程式碼，要害就在圖1中的206行：

圖1 SMT漏洞程式碼

Etherscan連結如下：

而黑客的攻擊手法和成果如下：

Function: transferProxy(address _from, address _to, uint256 _value, uint256 _feeSmt, uint8 _v, bytes32 _r, bytes32 _s)
 


MethodID: 0xeb502d45

[0]:  000000000000000000000000df31a499a5a8358b74564f1e2214b31bb34eb46f（_from，轉賬轉入地址）
[1]:  000000000000000000000000df31a499a5a8358b74564f1e2214b31bb34eb46f（_to，轉賬轉出地址）
[2]:  8fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff（_value）
[3]:  7000000000000000000000000000000000000000000000000000000000000001（_value）
[4]:  000000000000000000000000000000000000000000000000000000000000001b（_v）
[5]:  87790587c256045860b8fe624e5807a658424fad18c2348460e40ecf10fc8799（_r）
 

[6]:  6c879b1e8a0a62f23b47aa57a3369d416dd783966bd1dda0394c04163a98d8d8（_s）

黑客獲得財富為：

可以發現黑客的balances[_To]憑空獲得了鉅額的財富，該數字在這一刻，超越了全球現有貨幣發行總量。美美的財富啊！但是帶來的後果就是smartmesh貨幣總量瞬間崩潰了。這筆財富瞬間超越了全部SMT限定總額。

SMT事件，可以簡單概括為一句話：“一個加法帶來的血案！”

乘法溢位漏洞：一個乘法引發的血案！

同樣，BEC的過程依然如此，圖2程式碼的257行，存在一個巨型整數乘法溢位問題：

圖2 BEC漏洞程式碼

黑客構造的攻擊如下，轉賬記錄如下：

瞬間，整個全世界都屬於這個黑客的了。又是“一個乘法引發的血案！”。

由此看來，智慧合約的安全性將會極大動搖整個區塊鏈2.0的根基。

目前的智慧合約，從使用者角度來講，實際上是一個無人值守、程式機械執行、具備自動擔保的應用程式，只是當特定的條件滿足時，能夠自動釋放和轉移資金。智慧合約從技術層面來講就是一種網路服務，是通過區塊鏈共識，完成特定的合約程式執行。由於是共識，區塊鏈上的任意智慧合約程式碼和狀態必然都要公開，都要經受歷史的考驗；而任何一個黑客都可以從容淡定地審視每一行可能被屠殺的程式碼，就像叢林社會中那些凶猛的獅子總是在草原深處遊蕩，但偶爾會看看這些可憐的羚羊（合約）。即使合約被黑客吃幹抹淨，這些可憐的資料還恥辱地掛在那裡，諸位看客們或憐憫、或嘲笑、或深深的嘆息，或許還有一兩個此間的少年來一句：“大丈夫當如是也！”。

我們知道，開原始碼大致每1000行就含有一個安全漏洞，表現最好的Linux kernel 2.6版本的安全bug率為每一千行程式碼0.127個。而智慧合約作為新生事物，對應的程式設計師沒有經過嚴苛訓練與考驗，其程式碼可靠性可想而知。我們對2018年1月到4月，以太坊全部部署的全部8000多個合約，其內部函式呼叫情況統計結果如表1所示。

可以看到，加減乘除採用安全函式的合約只佔少數，實現轉賬功能的基本每個合約都有。從大概率上講，黑客的好日子還在後頭，數字貨幣市場出現安全動盪的情況，一定比大姨媽還要準時。目前的以太坊只是一個記錄 DApp 執行結果的區塊鏈，本身並沒有提供加密貨幣複式記賬所需的UXTO模型。以太坊自身的以太幣也是通過balance 來表示賬號餘額，這實質就是最原始的古代單式記賬方法。而看過類似《天下糧倉》電視劇的，都知道這種基於財務做賬的難於發覺之處。

那麼我們要怎樣才能改變這一現狀呢？魯迅先生講過：“真的猛士敢於直面慘淡的人生”，作為區塊鏈的從業者，我們堅定的認為智慧合約是一個跨越時代的思想，但現有的實現方式的確需要改變。

智慧合約面臨的3個挑戰

現有的智慧合約需要解決三個問題：

• 安全性問題；

• 可靠性問題；

• 易用性問題。

可靠性問題與易用性問題，我們可以依託人工智慧以及其他相關技術解決，本文重點談談安全性怎麼解決。

智慧合約的解決方案——智慧合約

要想真正解決智慧合約的安全性問題，就必須設計一套完整的綜合防護體系，並能不斷完善，具體包括：

• 事前防護：程式碼編寫過程中的規範化與程式碼釋出的漏洞檢測；

• 事中驗證：在智慧合約虛擬機器中完成程式碼的執行與動態安全檢測；

• 事後彌補：對智慧合約執行結果進行審計，確保執行不會出現偏差，執行結果在可信範疇。利益關聯方能夠及時發起申述，並進行裁決。

我們將這種支援具備完整安全防護體系的智慧合約稱為智慧合約。

如果BEC與SMT採用智慧合約的方式部署，將得到多重防護，從而獲得多次“上天再給我一次重來的機會”。典型的機會包括：

• 程式碼定型與釋出時的驗證與檢查。無論設計者是否願意，每個釋出的程式碼將接受自動規則驗證檢查，從而確保靜態程式碼審查通過，那些典型的溢位漏洞規則將無處藏身；

• 節點在執行合約中的動態驗證。該動態驗證將涵蓋本合約、關聯合約的驗證，並對執行過程中的狀態進行審查，從而實現各種執行漏洞進行彌補，即使黑客造出漏洞，各個合約執行者也會嚴密審視，並掛起可以執行操作；

• 合約執行完畢的合理性判斷。合約執行完畢的結果將通過一定的規則進行評判，同時引入人工智慧，對合約執行的合理區間進行分析，從而決定最終的結果輸出；例如對賬目進行復式審查或更高維度進行審查；

• 相關利益方的申訴機制與自動判決技術。在智慧合約部署的節點上，每個節點都內建基於規則的判決機制以及人工智慧稽核機制，支援自動投票表決，從而保證一定的機會挽回損失。

實際上，智慧合約必須由以下幾類技術，才能完成基礎框架：

• 基於規則知識庫的語法檢查

• 基於語義分析的交易模型識別與安全檢查

• 基於AI的形式驗證的智慧合約安全性檢查

• 基於深度神經網路的動態驗證和安全性優化

2

MATRIX智慧合約的先進技術實現

MATRIX是區塊鏈+人工智慧技術的倡導者和領導者，團隊擁有AI科學家鄧仰東教授、晶片科學家時昕博士和CTO李慶華等大量專業人才，在人工智慧與區塊鏈基礎鏈研究上，做出了大量的基礎性研究工作，並取得了大量突破性進展和技術專利；在MATRIX的共識演算法上創新性地使用了“蟲洞網路”來保證MATRIX在未來可以支撐百萬級TPS的商業級應用的同時還能保障系統的安全性。

智慧合約則是MATRIX另外一個重要特性。下面將簡單從技術實現的角度介紹MATRIX在智慧合約上的研究進展，並給出當前智慧合約各種缺陷的對策。

基於規則知識庫的語法檢查

核心原理是將原始編碼檔案，通過內建編譯工具，將對合約構建一棵基於BNF正規化基礎上的抽象語法樹（AST），通過該語法抽象樹，便可以對合約內容展開語法識別，進行簡單的合約安全識別。目前建議按照遞迴下降分析的方法，對語法抽象樹進行基於知識規則庫的檢查，從而確定是否存在安全隱患。

雖然一般的智慧合約描述均為圖靈完備，在抽象語法樹可以表現為多樣性，但很容易發現：安全的智慧合約實際應該是一個典型的閉合自洽描述，具備有限狀態空間或確保能夠檢測終止的有限狀態機。因此可以通過檢測的語法抽象樹的平衡和閉合性，確定智慧合約是否具備基本安全性。

典型的例子包括：

• 對所有的條件選擇語句進行完備性補足，防止由於條件不完善導致合約執行缺陷的；

• 對所有public成員與函式進行引用物件分析，確定合約對外暴露的危險等級。

• 交易步驟完備性檢查，確定每個合約交易方的條件動作描述完備。

基於語義分析的交易模型識別與安全檢查

基於語法的安全檢查規則僅能靜態識別合約缺陷，而基於語義分析的交易模型識別與安全檢查，則主要通過上下文相關審查，確定智慧合約中不滿足規則或者不安全的操作。目前支援的安全檢查包括：

• 型別檢查，具體包括檢查合約中需要對外暴露的物件與方法，審查其動作的必要性以及潛在的缺陷。

• 控制流檢查，具體包括檢查合約中各種選擇分支或者針對ORACLE的處理是否完備，並確定合約被呼叫時，是否存在其他異常處理等。

• 一致性檢查，具體包括同一個合約條件，出現在不同的選擇組合中；各種分支出現組合覆蓋等，避免由於分散式執行出現由於礦工呼叫順序不同，導致的合約異常。

通過上述靜態語義分析，能夠基本排除由於人為書寫智慧合約帶來的各種表層的邏輯缺陷，但尚不能解決動態執行過程中出現的各種邏輯問題。這些問題包括：

• 書寫程式碼不精確、不完備導致的合約組合條件情況處理的缺失；

• 個人合約設計目的與真實編寫程式碼之間存在較多的差異；

• 由於合約執行採用分散式執行，各個節點對程式碼的執行順序存在差異，導致當本合約出現異常時，其他合約能夠呼叫或更改本合約的各種狀態，出現各種非安全性問題。

MATRIX的核心是人工智慧輔助計算，各個層級上均內建AI能力，因此在合約驗證上，採用基於AI輔助的形式驗證以及動態約束檢查的方法，解決上述安全問題。其核心思想包括：

• 利用模式匹配獲得使用者真實需求約束：基於語義分析形成的合規語法抽象樹進行基礎模式匹配，獲得使用者可能的交易基礎模型。該方法能夠以靜態手段獲得大部分語法抽象分支的區域性匹配。MATRIX根據具體的匹配度，確認候選模型或模型組合，從而根據模型新增交易約束與交易斷言。

• 對靜態語義分析形成的抽象樹，按照MATRIX的AI引擎——貝葉斯分類器進行模型分類，確定樹中的各段分支屬於對應的類屬。而在MATRIX中，針對每個交易類屬，均具備對應的靜態與動態約束。

• 根據模式匹配結果和人工智慧分類結果，獲得當前合約的全部靜態與動態約束，基於該約束即可生成合約程式碼的斷言，並基於該結果進行形式驗證和動態驗證。

對於模型匹配失敗或者分類失敗的合約，MATRIX將提出不可靠安全告警，並在執行過程中進行更嚴苛的邊界檢查。

MATRIX支援Bytecode級別的語義審查，核心還是進行反彙編，然後生產語法抽象樹，然後進行利用AI進行語法樹匹配。

基於AI的形式驗證的智慧合約安全性檢查

MATRIX使用形式驗證技術對智慧合約的安全性進行自動化檢查。其中，形式驗證模型使用F*函式程式語言（functional programming language）建立，該語言整合了Z3 SMT求解工具，擁有豐富的型別和條件檢查功能，已經被用於多種軟體和加密程式的驗證。

圖3 智慧合約的形式驗證

智慧合約形式驗證流程圖如圖3。形式驗證工具鏈能夠處理原始碼級的智慧合約，其中原始碼被翻譯為等效的F*函式程式；也能夠處理編譯為位元組碼的智慧合約，此時需要對位元組碼進行反編譯，同樣形成等效的F*函式程式。Matrix區塊鏈平臺的智慧合約語法結構以及相應函式程式語法結構如圖4。對於使用者自行編寫的智慧合約，我們還可以對原始碼模型和編譯程式碼模型進行等效檢查，從而發現編譯器的錯誤或者不良副作用。

在建立基於函式程式語言的模型之後，形式驗證的基本手段是針對模型定義需要滿足的安全屬性（即property，例如對send()函式的返回值是否進行了檢查），然後使用定理證明工具或可滿足性工具尋找是否存在反例使得以上條件不成立。然而，即使對專業智慧合約程式設計師來說準確定義完備的安全屬性集合都是極端困難的事情，對一般使用者來說則幾乎是不可能的。

MATRIX的一個關鍵特色是使用人工智慧方法自動識別程式語義並發現其中的典型模式，從而根據模式自行產生為了滿足安全要求而需要的屬性。當用戶提供智慧合約程式碼或編譯後的執行程式碼後，MATRIX的AI引擎將自動完成程式碼的區域性相似性匹配和全域性相似性匹配，從而推測程式碼的行為模型。根據AI獲得行為模型，生成對應的形式驗證約束，從而進行深層次的行為驗證，實現程式碼安全性。

由於使用函式程式程式語言作為內部驗證的形式化表徵，MATRIX還可以對Ethereum現有開源合約進行模式挖掘。這些模式可以表現為語義或者結構（以及兩者的組合）的形式，前者一般是特定語法和函式特徵，後者則是語法結構特徵。

基於深度神經網路的動態驗證和安全性優化

表2列出以太坊智慧合約在高階程式語言、位元組碼和區塊鏈三個層次上的脆弱性、當前主要的攻擊方式以及相應脆弱性在受到攻擊時表現出的特徵。

為解決上述問題，MATRIX準備開發兩類安全工具，以解決上述問題，具體包括：

• 基於對抗網路的安全驗證；

• 基於分散式併發的動態模型驗證。

基於GAN的安全驗證

怎樣設計在充滿不確定性的分散式環境下仍然能夠正確、安全執行的智慧合約程式碼呢？Matrix平臺只需要使用者以指令碼語言方式說明合約意圖（輸入、輸出和交易條件等），然後使用基於神經網路的程式碼生成技術把指令碼轉換為智慧合約程式碼，如下所示。繼而採用類似對抗網路的方法，即一方面使用程式碼生成網路產生黑客程式碼極其攻擊條件，一方面對現有程式碼進行變型和優化，同時在模擬區塊鏈網路上對上述程式碼進行對抗和效能評估，直至產生足夠安全的智慧合約程式碼。

圖4. 智慧合約程式碼生成

圖4的智慧合約程式碼生成流程使用基於遞迴神經網路的程式碼生成工具把指令碼轉換為智慧合約程式碼，其中的遞迴神經網路需要使用現有智慧合約程式及其輸入和輸出結果作為訓練樣本。

基於分散式併發的動態模型驗證

智慧合約的攻擊手段和防護手段在前面已經詳細論述，MATRIX還提供了基於分散式併發的動態模型驗證，對如下的手段進行防護：

交易合約順序攻擊

出現合約順序攻擊的本質是智慧合約的執行是非同步的，且可以動態更改。即使合約本身是靜態安全情況下，也無法防止此類動態攻擊，除非合約本身設計為動態不可更改。對於MATRIX智慧合約，則通過AI的動態保護，包括對礦工執行合約集的進行整體關聯性審查，通過環路發現，找出基於此類的關聯合約交易。另外，MATRIX提供基於多節點執行的非同步模擬器，通過對設立多個節點（當前為5個節點）採用亂序併發方式，非同步執行合約，通過對每個執行序列的觀察，確定是否出現異常來排除交易合約順序攻擊。

基於時間戳依賴的攻擊

時間戳依賴的本質是礦工自主權過大，因此MATRIX通過AI動態審查時間戳依賴或者隨機數依賴，可以避免在合約中出現相應的依賴行為。MATRIX還額外設計了二階段隨機數機制和對應的智慧選舉方案解決。

誤操作異常和可重入攻擊

上述攻擊實際上是合約呼叫過程中，觸發異常狀態。MATRIX將通過深度學習，找出此類行為特徵的編碼方式，獲得類似黑客作案手法的碼本特徵庫，並進行程式碼庫靜態與動態審查。其中動態審查則是基於形式驗證中的約束，動態生產特徵向量，並針對性的測試發現缺陷。

3

結束語

而且隨著市場競爭的激烈，各種需求急劇變化，每種新技術的生命週期很短。站在區塊鏈行業發展的角度看，數字合約是一個“激流世界”，下一刻沒有人知道會發生什麼。但我們知道，對付“激流世界”的核心手段就是在變化的世界中找出不變的東西，從而從容面對時刻發生的挑戰，而基於人工智慧和經過傳統金融考驗的安全風控方法——智慧合約，正是核心解決之道。

作者介紹：國內頂級晶片設計專家，擁有多項晶片專利，他作為主設計師，設計了國內第一款WiFi晶片。同時作為總工團隊成員和基帶專案總工程師，設計了中國首個大型水面艦艇的通訊排程指揮系統。個人主導設計了多款量產商用晶片，並多次獲得省部級科學技術獎勵。著有《通訊IC設計》一書，京東同類書籍銷售排行榜第一名，被北郵等一流高校採取為研究生晶片設計課程的教材。

本文作者：MATRIX CTO 李慶華

以下是我們的社群介紹，歡迎各種合作、交流、學習：）