智慧合約：智能合約安全問題的AI解決方案

「一支穿雲箭，千軍萬馬來相見」。

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

1

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

智能合約的2個缺陷

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

• 智能合約不夠智能；

• 智能合約缺乏安全保障機制和安全工具。

區塊鏈2.0的核心是智能合約，而當黑客可以垂手可得地利用智能合約漏洞隨心所欲時，實質上至關於動搖了整個大廈的根基，所以形成數字貨幣市場的恐慌也在所不免。

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

咱們能夠將SMT漏洞概括爲一句話：利用加法的溢出漏洞，規避安全檢查從而得到鉅額收益。首先看看這段代碼，要害就在圖1中的206行：

 圖1 SMT漏洞代碼

Etherscan連接以下：

https://etherscan.io/tx/0x1abab4c8db9a30e703114528e31dee129a3a758f7f8abc3b6494aad3d304e43f

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

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漏洞代碼

合約代碼地址：https://etherscan.io/address/0xc5d105e63711398af9bbff092d4b6769c82f793d#code

黑客構造的攻擊以下，轉帳記錄以下：

https://etherscan.io/tx/0xad89ff16fd1ebe3a0a7cf4ed282302c06626c1af33221ebe0d3a470aba4a660f

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

由此看來，智能合約的安全性將會極大動搖整個區塊鏈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 李慶華

如下是咱們的社區介紹，歡迎各類合做、交流、學習：）