智慧合約——解決智能合約安全問題的宙斯盾！

接收程序員的技術早餐

作者｜李慶華

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

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

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

智能合約的 2 個缺陷

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

智能合約不夠智能；

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

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

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

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

圖 1 SMT 漏洞代碼

Etherscan 鏈接如下：

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

黑客獲得財富為：

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

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

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

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

圖 2 BEC 漏洞代碼

合約代碼地址：

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

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

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

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

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

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

表1 以太坊智能合約函數調用情況統計

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

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

智能合約面臨的 3 個挑戰

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

安全性問題；

可靠行問題；

易用性問題。

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

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

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

事前防護：代碼編寫過程中的規範化與代碼發布的漏洞檢測；

事中驗證：在智能合約虛擬機中完成代碼的執行與動態安全檢測；

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

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

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

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

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

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

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

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

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

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

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

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

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 列出以太坊智能合約在高級編程語言、位元組碼和區塊鏈三個層次上的脆弱性、當前主要的攻擊方式以及相應脆弱性在受到攻擊時表現出的特徵。

表2.以太坊智能合約的脆弱性

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

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

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

基於 GAN 的安全驗證

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

圖 5. 智能合約代碼生成

圖 5 的智能合約代碼生成流程使用基於遞歸神經網路的代碼生成工具把腳本轉換為智能合約代碼，其中的遞歸神經網路需要使用現有智能合約程序及其輸入和輸出結果作為訓練樣本。

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

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

（1）交易合約順序攻擊

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

（2）基於時間戳依賴的攻擊

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

（3）誤操作異常和可重入攻擊

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

結束語

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

作者介紹

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

喜歡這篇文章嗎？立刻分享出去讓更多人知道吧！