TMT观察网_独特视角观察TMT行业

隨著平臺級應用的普遍化，智能合約涉及的金額呈指數級別增長，智能合約的安全問題也成為投資者和開發者共同關注的焦點。今年以來有數個基于ERC-20的ICO項目因為智能合約代碼出現漏洞而遭到黑客攻擊，導致投資者巨額的損失。為了防止類似事件的發生，交易所、錢包、項目方等都在智能合約安全上加大投入，同時圍繞著智能合約安全的周邊生態成為目前投資的熱點。

——————————————————

作者：

ONE.TOP  洪妙叢

節點研究中心  蔡晨曦 武怡 郎瀚威

支持機構（排名不分先后）

金塔行情、星球日報、金色財經、babi財經、節點財經

（本報告由ONE.TOPX節點研究中心聯合發布）

智能合約安全方面的措施總體來說分為以上幾個大類，合約開發模板、合約審計、智能合約語言設計和賞金獵人機制。

1）合約開發模板如OpenZeppelin、Etherparty等為標準化的合約提供經過多次實戰驗證的標準化模板，在節約時間同時保證合約安全性。

2）合約審計的方法又分為人工審計和機器輔助審計

3）機器輔助審計又分為規則驗證、語義驗證和形式化驗證，而形式化驗證是本文關注的重點。

引用自consensys 唐奕 《公鏈安全》

智能合約語言設計中，許多公鏈平臺開始采用Haskell或OCaml一類的函數式語言，因為函數式語言更為便于編寫形式化驗證方面的開發者庫和工具。賞金獵人機制，相對于前幾項措施，更多是部署合約后發現漏洞的彌補機制。

形式化驗證指的是用數學中的形式化方法對算法的性質進行證明或證偽。方法有兩種：

一種是模型檢驗，即把系統所有可能的狀態列出并進行一一檢驗，此種方法全自動化但只適合小型系統；

另一種是演繹驗證，首先把系統代碼標記成抽象數學模型，然后對定理進行證明，此種方法適合大型系統，但是需要首先人工將系統的運作方法轉換成驗證系統可以理解的語言。

目前為止，形式化驗證主要應用在軍工、航天等對系統安全非常高的領域，在消費級軟件領域幾乎沒有應用。由于傳統互聯網應用與區塊鏈應用的運行環境有著本質的不同，其開發流程也應當相應地進行調整，其中最關鍵點在于安全驗證環節的投入比例。

在傳統互聯網應用中，由于普遍采用中心化服務器+客戶端的模型，如果應用出現安全隱患只需要對服務器端代碼進行修改就可以輕松排雷，并且服務器端可以對用戶數據進行回滾以挽回用戶損失。因此，傳統互聯網應用開發的過程較為注重快速迭代，以犧牲安全性換取效率和功能上的快速升級。

在區塊鏈應用中，由于區塊鏈的不可篡改性，智能合約一旦上線并出現安全隱患，對用戶造成的損失是巨大且不可挽回的。一旦出現黑客事件，需要整個社區的共識才能回滾交易，所以每次遭受攻擊都回滾交易也是不現實的。因此，區塊鏈應用開發的過程需要用大量的測試和檢驗以獲取足夠的安全性，而反過來犧牲迭代的速度。

由于區塊鏈開發人員的稀缺，遠遠無法趕上智能合約數量的增長，人工審計智能合約是成本非常高昂的，因此機器輔助驗證是目前的必然趨勢。規則、語義驗證的實現，相對較為容易，技術門檻也較低，但是只能進行一些淺層的糾錯，不能深入程式的邏輯。因此，只有形式化驗證方法有希望真正提高智能合約審計的自動化程度。

目前區塊鏈產業中與形式化驗證相關的產品可以分為三類: Vaas平臺，公鏈，和語言。

Vaas平臺是直接面向開發者提供形式化驗證服務的平臺。目前Vaas類項目包括CertiKzecurify.ch、Runtime Verification等項目。目前，CertiK仍在募資階段，鏈安科技據稱已經有研發成功及獲得專利的產品，Securify.ch的測試版已經上線，而Runtime Verification已經在商業運營

與其它幾個項目不同，RuntimeVerification是基于EVM虛擬機二進制碼進行形式化驗證，而非針對智能合約本身用的高級語言，因此在安全性上又更進一步，避免了因編譯器編譯過程中可能產生的漏洞。

語言類產品一般為函數式語言的子語言，提供與智能合約形式化驗證相關的開發者庫和工具，目前有Imandra和Tezos等項目。

其中，Imandra發布了一套開源的以太坊虛擬機用ImandraML語言標記的模型，并且專注于交易所等金融應用場景的形式化驗證，用以確保金融交易的合法合規，據稱相關技術已經用于華爾街頂級投行的交易系統。

直接包含形式化驗證引擎的公鏈產品目前只有The Matrix項目，特征是基于AI輔助的形式化驗證及動態約束的檢查。AI是否對于形式化驗證的自動化帶來幫助在技術上仍是個未知數，因此這個項目也將成為這個領域的試金石。

Certik是一個是形式化驗證框架，經過certik驗證的智能合同、DApp以及區塊鏈將會被附上證書形式的標志，來展示其正確性和安全性。Certik平臺提供的主要功能包括以下部分。

智能標簽框架

CertiK平臺應用深度學習技術來構建智能標簽框架，有了這個框架，大多數共享邏輯和屬性代碼（前置條件，后置條件，不變量等）都可以被自動標記，從而使得程序的邏輯，語義更加清晰和規范，這樣驗證的工作量就可以大大減少。

基于層的分解

這種技術揭示了分層設計模式的見解，并使得將復雜的證明任務分解為更小的任務成為可能，并在適當的抽象層面驗證它們中的每一個。

可插拔的驗證引擎

提供開放式的協議，更先進算法的證明引擎可以自由插入這個系統。

機器可檢驗的證明對象

構建機械式的證明對象（或者反例），這些證明對象可以快速的被任何人檢驗，同時作為驗證程序的證書（機械式證明對象可直接作為證書，賞金獵人提供的證明對象，需要檢察官進行人工檢驗后才能作為證書。注：賞金獵人和檢察官后文會進行描述。）

認證的DAPP庫

為集成開發環境提供了一系列認證庫和插件，以便開發出質量更高的dapp，但是會花費一些CTK。

定制化的認證服務

如果有高可靠性要求，可以提供定制化的認證服務，由驗證領域的專家提供幫助并出具綜合報告。

Certik平臺圍繞bug的檢測和修復建立了一個去中心化的生態，該生態由五個角色構成，分別是客戶、賞金獵人、檢查官、社區貢獻者以及開發使用者，該生態工運行模式如下圖所示。

該系統可以分為機械化部分和人工部分。客戶在certik平臺上提交dapp或者程序系統，平臺自動為其添加智能標簽，并自動進行分解，形成小模塊的證明任務，這個環節客戶需要消耗一定量的CTK。

分解完小模塊后，系統由兩種方式進行驗證，簡單的證明任務可以由一些自動驗證器(例如SMT解算器)解決。除了平臺內部自帶的驗證器（證明引擎），CertiK平臺提供開放協議，社區貢獻者可以將帶有更高級的求解算法的證明引擎自由地插入到該系統中，并獲得一些CTK獎勵。賞金獵人可以隨機使用他們的引擎，并進行評估，優秀的引擎將被社區研究和推廣。

另一種驗證方式針對較為復雜的證明任務。賞金獵人接到該任務后，構建一個證明對象并進行廣播，接著檢查官對證明對象進行檢測，當證明對象驗證通過后，會被貼上證書的標簽，賞金獵人和檢查官分別獲得CTK獎勵。

所有分解的證明任務被驗證后，CertiK平臺的后端將返回詳細而全面的評估報告。

開發使用者可以使用所有CertiK平臺的認證庫和IDE插件， 構建自己的DApp /系統，這需要花費一定的CTK。

以下是certik的操作界面

打開 CertiK 的系統，上傳要檢測的智能合約，按下檢測按鈕

檢測完畢后，CertiK 會提供這份智能合約的安全系數，并告訴你哪一塊程序存在著錯誤，并提供詳細的解決方案

提供幾種驗證服務：

?   第一個，安全審計

?   第二個，開發、審計一條龍

?   第三個，合約開發

其中安全審計模塊針對的漏洞包括代碼編程規范漏洞、代碼邏輯漏洞、函數調用漏洞、整型溢出漏洞、可重入攻擊漏洞、執行順序依賴漏洞、時間戳依賴漏洞、平臺接口誤用漏洞。

鏈安CEO通過一個例子從數學原理上對形式化驗證進行了描述說明。以近期頻發的溢出類安全漏洞屬性檢查為例，如檢查代碼

int8 c=a+b

是否存在溢出漏洞，下面展示對這行代碼的功能正確性和安全屬性的證明過程。

首先，對整數類型建模，定義形式化規則：

Int8.repr: Z -> int8

該規則通過截取純數學整數（取值范圍從無窮小到無窮大）的低8位數值得到一個8位長度的機器整數。然后寫加法運算的形式化規范，如下：

{a:int8,b:int8} //

設置代碼執行的前提條件，保證a和b的類型是8位有符號機器整數;

{c = a + b;} //

加法運算的源碼程序；

{(int8.repr(a+b)) /\ ((Int8.repr (a+b)) = (a+b))} ; //

設置代碼正確執行的后置條件。

其中，(int8.repr(a+b))描述，是為了證明代碼的功能正確性是否滿足，即需要證明源代碼是對a和b進行求和而不是求差或任何其他運算邏輯，并且將運算結果轉換為int8類型。此外，需要對是否溢出的安全屬性進行證明，因此添加后置條件：

((Int8.repr (a+b)) = (a+b))

因為一旦

a+b>int8.max_singed

或

a+b<int8.min_signed

都將導致

(Int8.repr (a+b)) ≠ (a+b)

最后，根據前置條件證明代碼的執行是否滿足上述后置條件。如果產生一個不可證明結果，說明程序功能不正確，或者存在溢出安全漏洞。然后根據證明結果，對源程序進行分析修改，然后再重新證明，直到證明通過為止。鏈安采用這種數學的證明方式將代碼形式化描述為公式，并對其進行邏輯漏洞和安全漏洞證明，基于此原理，實現了自動化的驗證工具，能夠方便、快速地驗證出代碼的功能正確性和安全屬性。

RuntimeVerification Inc.是一家初創公司，通過使用自己研發的runtime驗證技術致力于提高汽車，飛機，航天器和區塊鏈領域的軟件系統的安全性，可靠性和正確性。從2001年開始，runtime verification就成為NASA的研究科學家。

Runtime驗證技術依賴于程序執行不應違反某些屬性的原理。其中一些屬性，如并發程序中缺少數據競爭，具有通用性，可以自動檢查。 其他屬性，如專用庫的規格，是針對特定應用程序或用途定制的。Runtime驗證技術可以自動檢查通用屬性，不需要開發輸入，并且可以檢查開發人員用形式化方式表達的任何定制屬性。

在區塊鏈方面，runtime公司主要對智能合約進行形式化驗證工作，驗證步驟包括：

（1）形式化

根據智能合約所有者提供的非形式化規則，對智能合約的高級業務邏輯進行形式化。

（2）確認

形式化后的高級業務邏輯需要由智能合約的所有者確認，可能需要經過多輪討論和修改，才能確保它能正確捕捉合同的預期行為。

（3）提煉

通過多個步驟將形式化后的規則完善到虛擬機級別，以捕獲虛擬機特定的細節。最終的虛擬機級別規則的作用是確保在字節碼級別沒有意外發生，也就是說，只有在執行字節碼時才會發生高級規則中指定的內容。

（4）編譯和測試

使用與部署合同相同的編譯器版本，將智能合約從其高級代碼編譯為生成的虛擬機低級代碼。

（5）驗證

最后，對智能合約的虛擬機字節碼與虛擬機的規則進行形式化驗證，通過這樣的方式不用依賴編譯器的正確性。同時，runtime使用自己研發的K-framework結構演繹驗證程序， 以達到嚴格推理虛擬機字節碼而不遺漏任何虛擬機怪癖的效果。

2016年6月17日，一名黑客在編碼上發現了漏洞，使得他可以從The Dao上抽走資金。在攻擊的頭幾個小時，360萬的以太被轉出，在當時價值相當于七千萬美元，今天則達到了21億美元。黑客達成了他想要的破壞，退出了攻擊。

在此漏洞中，攻擊者能夠“請求”智能合同( DAO )多次返回以太，且都是在智能合約更新它的余額前進行的。兩個主要問題使它成為可能：一是在創建DAO智能合約時，編碼人員沒有考慮到遞歸調用的可能性；二是智能合約首先發送ETH資金，然后再更新內部token余額。

重要的是要了解這個bug不是來自以太坊本身，而是來自基于以太坊上的構建應用程序。為DAO編寫的代碼有多個缺陷，遞歸調用的漏洞就是其中之一。

另外一種理解它的方式是比較。以太坊比作是互聯網，基于以太坊的應用比作是網站。也就是說，如果網站不運行，不意味著整個互聯網出問題。它只能說明網站有問題。

黑客出于未知的原因停止從TheDAO抽取資金，盡管他可以繼續這么做。以太坊社區和團隊很快就控制了局面，并提出了多項應對攻擊的建議。

然而，這些資金被存入一個賬戶，有一個28天鎖定期，黑客無法轉走。為了退還損失的錢，以太坊通過硬分叉把被黑資金退還到原所有者的賬戶上。退還匯率是1 ETH兌100 DAO ，與首次公開發行時的匯率相同。

毫無意外，黑客攻擊意味著DAO的終結。很多以太坊用戶質疑硬分叉違反區塊鏈的基本信條。更糟糕的是，2016年9月5日，Poloniex交易所下架了DAO token，Kraken在2016年12月也下架了DAO token。

與美國證券交易委員會(SEC)2017年7月25日發布的報告相比，以上的這些問題都相形見絀。它提到：

“由一個名為“DAO”的“虛擬”組織提供和出售的代幣是證券，因此受聯邦證券法的約束。報告確認，發行基于區塊鏈技術的證券發行者必須登記此類證券的發行和銷售，除非有有效的豁免。參與未注冊發行的證券的人也可能要對違反證券法的行為負責。”

換句話說，TheDAO的發行與首次公開發行(IPO)一樣，受到同樣監管原則的約束。按照SEC觀點，DAO違反了聯邦證券法，所有投資者也一樣。

區塊鏈項目EDU智能合約中存在漏洞。在一個名為transferFrom 函數中，缺少 Safemath 驗證，利用溢出攻擊可以讓攻擊者從任何一個 EDU 余額不為 0 的賬號內向另外一個賬號轉出 任意數量的EDU Token。

由于目前EDU在火幣pro上線，黑客利用漏洞累積向火幣轉入了超過20億枚EDU。這也導致了EDU的價格崩盤。

韓國團隊，基于ICON的第二個項目。項目目的是要創建一個去中心化的聲譽系統，通過集體智能和人工智能相結合，將所有數字貨幣的粘片，黑客信息，可疑錢包地址等各種信息記錄在區塊鏈上。

要成為世界上第一個分布式物聯網安全協議。

Atonomi利用區塊鏈上的特性與經濟激勵，利用Token注冊和驗證評估系統，構建出一個物聯網設備的認證與信譽數據庫，保證每一臺加入網絡的設備，都擁有良好的信譽。同時，應用母公司Centri的技術（Centri是傳統互聯網的安全公司，擁有多項安全方面的技術專利，并與很多互聯網大公司是合作伙伴）給設備加密，確保數據隱私并阻止它被黑客利用來連接到別的物聯網設備。同時Atonomi的Token也像IOTA一樣支持設備之間的微支付需要。

嚴格意義來講，Gladius并不是一個保護區塊鏈的項目，而是一個利用區塊鏈技術，來保護傳統互聯網的項目。

Gladius是利用存儲和流量的經濟激勵，來創建基于區塊鏈的分布式CDN，從而實現DDoS攻擊的分散保護，同時創建一個大型流量池，處理不斷出現的DDOS請求，提供比傳統DDOS防護更加經濟和高效的方式。

Gladius的桌面客戶端允許用戶租用計算機空余的帶寬，并為提供者獎勵代幣，代幣可以購買區塊鏈服務，也可以用于開發，有點變向挖礦的意思。

正如一家公司的財務報表需要審計一樣，智能合約，同樣需要審計，有了審計，這些類似漏洞發生的概率，可以被大幅度降低。

簡單說來，Quantstamp就是這樣一個區塊鏈智能合約的審計類項目，讓智能合約變得更加安全。當然了，和像四大會計事務這樣的中心化組織不一樣，咱們是去中心化的。

Polyswarm 第一個去中心化的殺毒軟件市場

去中心化正是區塊鏈的看家本領，Polyswarm是世界上第一個嘗試用區塊鏈來改變這個市場的。他們設計的系統里有4種角色。

用戶（EndUsers）報告可能染毒的文件信息，并在平臺上懸賞，得到及時而準確的安全信息。

安全專家（Experts）通過分析病毒信息來決定這是否是一個病毒來賺取獎勵。

由于智能合約形式化驗證目前尚處于起步階段，目前項目大多還沒有落地。展望相關行業需求，相關的投資邏輯如下。

目前為止，造成嚴重后果的漏洞大多來自錢包、ICO募資等金融領域應用的合約，而這類合約邏輯較為標準化，相對較容易用形式化驗證的方式進行查驗。因此，專注于金融領域的形式化驗證產品更有潛力。

許多新的公鏈項目，如Aeternity、Tezos等都采取了函數式語言作為智能合約的編程語言，目的在于方便形式化驗證工具的開發。因此，在選擇公鏈項目上，函數式語言是首選。