2018.06.27
pdf高清下載鏈接：https://pan.baidu.com/s/1PWd1v4ENXloJTyI3Osilhg 密碼：arv3
pdf下載：
PBS8Vv3v734ZKFFBFyduDPJl0ZLQ3iGYIyDfBaAL.pdf
引言
隨著平臺級應用的普遍化，智能合約涉及的金額呈指數級別增長，智能合約的安全問題也成為投資者和開發者共同關注的焦點。今年以來有數個基於ERC-20的艾希歐項目因為智能合約代碼出現漏洞而遭到黑客攻擊，導致投資者鉅額的損失。為了防止類似事件的發生，交易所、錢包、項目方等都在智能合約安全上加大投入，同時圍繞著智能合約安全的周邊生態成為目前投資的熱點。
作者
節點研究中心 蔡晨曦 武怡 郎瀚威
ONE.TOP 洪妙叢
支持機構（排名不分先後）
金色財經、BlockMasterMail、babi財經、金塔行情、星球日報、節點財經
（本報告由ONE.TOP X節點研究中心聯合發佈）
1 區塊鏈安全領域分類——智能合約安全的分類
智能合約安全方面的措施總體來說分為以下幾個大類，合約開發模板、合約審計、智能合約語言設計和賞金獵人機制。
1）合約開發模板如OpenZeppelin、Etherparty等為標準化的合約提供經過多次實戰驗證的標準化模板，在節約時間同時保證合約安全性。
2）合約審計的方法又分為人工審計和機器輔助審計
3）機器輔助審計又分為規則驗證、語義驗證和形式化驗證，而形式化驗證是本文關注的重點
引用自consensys 唐奕 《公鏈安全》
智能合約語言設計中，許多公鏈平臺開始採用Haskell或OCaml一類的函數式語言，因為函數式語言更為便於編寫形式化驗證方面的開發者庫和工具。賞金獵人機制，相對於前幾項措施，更多是部署合約後發現漏洞的彌補機制。
形式化驗證指的是用數學中的形式化方法對算法的性質進行證明或證偽。方法有兩種：
一種是模型檢驗，即把系統所有可能的狀態列出並進行一一檢驗，此種方法全自動化但只適合小型系統；
另一種是演繹驗證，首先把系統代碼標記成抽象數學模型，然後對定理進行證明，此種方法適合大型系統，但是需要首先人工將系統的運作方法轉換成驗證系統可以理解的語言。
2 為什麼關注形式化驗證
目前為止，形式化驗證主要應用在軍工、航天等對系統安全非常高的領域，在消費級軟件領域幾乎沒有應用。由於傳統互聯網應用與區塊鏈應用的運行環境有著本質的不同，其開發流程也應當相應地進行調整，其中最關鍵點在於安全驗證環節的投入比例。
在傳統互聯網應用中，由於普遍採用中心化服務器+客戶端的模型，如果應用出現安全隱患只需要對服務器端代碼進行修改就可以輕鬆排雷，並且服務器端可以對用戶數據進行回滾以挽回用戶損失。因此，傳統互聯網應用開發的過程較為注重快速迭代，以犧牲安全性換取效率和功能上的快速升級。
在區塊鏈應用中，由於區塊鏈的不可篡改性，智能合約一旦上線並出現安全隱患，對用戶造成的損失是巨大且不可挽回的。一旦出現黑客事件，需要整個社區的共識才能回滾交易，所以每次遭受攻擊都回滾交易也是不現實的。因此，區塊鏈應用開發的過程需要用大量的測試和檢驗以獲取足夠的安全性，而反過來犧牲迭代的速度。
由於區塊鏈開發人員的稀缺，遠遠無法趕上智能合約數量的增長，人工審計智能合約是成本非常高昂的，因此機器輔助驗證是目前的必然趨勢。規則、語義驗證的實現，相對較為容易，技術門檻也較低，但是隻能進行一些淺層的糾錯，不能深入程式的邏輯。因此，只有形式化驗證方法有希望真正提高智能合約審計的自動化程度。
3 目前市場上的形式化驗證相關產品
目前區塊鏈產業中與形式化驗證相關的產品可以分為三類: Vaas平臺，公鏈，和語言。
項目名稱
分類
描述
創始團隊背景
CertiK
Vaas
結合證明引擎和賞金獵人的綜合性安全驗證平臺
哥大/耶魯
Imandra
語言
OCaml子語言，專注於金融交易系統的形式化驗證
倫敦金融城/英國劍橋
鏈安科技
Vaas
提供多個區塊鏈平臺驗證工具，以及將合約代碼轉成定理的證明工具
電子科技大學
The Matrix
公鏈
基於AI輔助的形式驗證以及動態約束檢查
清華/北大
Securify.ch
Vaas
一鍵對以太坊智能合約進行形式化驗證
ETH Zurich
Runtime Verification
Vaas
使用自己開發的K框架對虛擬機二進制碼進行形式化驗證
UIUC
Tezos
語言
採用函數式編程語言Michelson作為智能合約語言，方便形式化驗證
華爾街/R3
3.1 Vaas平臺
Vaas平臺是直接面向開發者提供形式化驗證服務的平臺。目前Vaas類項目包括CertiKzecurify.ch、Runtime Verification等項目。目前，CertiK仍在募資階段，鏈安科技據稱已經有研發成功及獲得專利的產品，Securify.ch的測試版已經上線，而Runtime Verification已經在商業運營。
與其它幾個項目不同，Runtime Verification是基於EVM虛擬機二進制碼進行形式化驗證，而非針對智能合約本身用的高級語言，因此在安全性上又更進一步，避免了因編譯器編譯過程中可能產生的漏洞。
3.2 語言
語言類產品一般為函數式語言的子語言，提供與智能合約形式化驗證相關的開發者庫和工具，目前有Imandra和Tezos等項目。
其中，Imandra發佈了一套開源的以太坊虛擬機用ImandraML語言標記的模型，並且專注於交易所等金融應用場景的形式化驗證，用以確保金融交易的合法合規，據稱相關技術已經用於華爾街頂級投行的交易系統。
3.3 公鏈
直接包含形式化驗證引擎的公鏈產品目前只有The Matrix項目，特徵是基於AI輔助的形式化驗證及動態約束的檢查。AI是否對於形式化驗證的自動化帶來幫助在技術上仍是個未知數，因此這個項目也將成為這個領域的試金石。
4 詳細對比
Certik
鏈安科技
runtime verification
創始人
邵忠，耶魯大學計算機科學博士；顧榮輝，哥倫比亞助理教授
楊霞女士，電子科技大學副教授、博士後
Daejun Park，首爾國立大學計算機科學與工程學士學位和碩士學位，目前正在攻讀博士學位
核心團隊
核心成員來自哥倫比亞大學、耶魯大學和普林斯頓大學，專業背景都是計算機技術，團隊技術實力強硬
20多名來自海外知名高校和實驗室(CSDS/耶魯/UCLA)留學經歷的副教授、博士後、博士、碩士組成
核心團隊成員大部分都有形式化驗證方向的研究和學習經歷
合作伙伴
量子鏈、INT、菩提
火幣網、OK資本、比原鏈、布比區塊鏈、雲象區塊鏈
NSF、NASA、Ethereum、Boeing
針對市場
對基於以太坊上開發的DAPP和系統進行形式化驗證
對智能合約進行形式化驗證，支持以太坊和EOS
致力於飛機，航天器和區塊鏈領域的軟件系統的安全性，可靠性和正確性
主要技術
開發了一個基於形式化驗證的平臺，創新的使用了包括智能標籤框架、層級分解在內的技術，幫助實現自動化的形式化驗證
高度自動化的智能合約安全審計平臺VaaS，再以人工方式對智能合約代碼逐行復核，保證審計質量
用自己研發的runtime驗證技術對對智能合約進行形式化驗證工作
5 產品簡介
5.1 Certik
Certik是一個是形式化驗證框架，經過certik驗證的智能合同、DApp以及區塊鏈將會被附上證書形式的標誌，來展示其正確性和安全性。Certik平臺提供的主要功能包括以下部分。
智能標籤框架
CertiK平臺應用深度學習技術來構建智能標籤框架，有了這個框架，大多數共享邏輯和屬性代碼（前置條件，後置條件，不變量等）都可以被自動標記，從而使得程序的邏輯，語義更加清晰和規範，這樣驗證的工作量就可以大大減少。
基於層的分解
這種技術揭示了分層設計模式的見解，並使得將複雜的證明任務分解為更小的任務成為可能，並在適當的抽象層面驗證它們中的每一個。
可插拔的驗證引擎
提供開放式的協議，更先進算法的證明引擎可以自由插入這個系統。
機器可檢驗的證明對象
構建機械式的證明對象（或者反例），這些證明對象可以快速的被任何人檢驗，同時作為驗證程序的證書（機械式證明對象可直接作為證書，賞金獵人提供的證明對象，需要檢察官進行人工檢驗後才能作為證書。注：賞金獵人和檢察官後文會進行描述。）
認證的DAPP庫
為集成開發環境提供了一系列認證庫和插件，以便開發出質量更高的dapp，但是會花費一些CTK。
定製化的認證服務
如果有高可靠性要求，可以提供定製化的認證服務，由驗證領域的專家提供幫助並出具綜合報告。
Certik平臺圍繞bug的檢測和修復建立了一個多中心化的生態，該生態由五個角色構成，分別是客戶、賞金獵人、檢查官、社區貢獻者以及開發使用者，該生態工運行模式如下圖所示。
該系統可以分為機械化部分和人工部分。客戶在certik平臺上提交dapp或者程序系統，平臺自動為其添加智能標籤，並自動進行分解，形成小模塊的證明任務，這個環節客戶需要消耗一定量的CTK。
分解完小模塊後，系統由兩種方式進行驗證，簡單的證明任務可以由一些自動驗證器(例如SMT解算器)解決。除了平臺內部自帶的驗證器（證明引擎），CertiK平臺提供開放協議，社區貢獻者可以將帶有更高級的求解算法的證明引擎自由地插入到該系統中，並獲得一些CTK獎勵。賞金獵人可以隨機使用他們的引擎，並進行評估，優秀的引擎將被社區研究和推廣。
另一種驗證方式針對較為複雜的證明任務。賞金獵人接到該任務後，構建一個證明對象並進行廣播，接著檢查官對證明對象進行檢測，當證明對象驗證通過後，會被貼上證書的標籤，賞金獵人和檢查官分別獲得CTK獎勵。
所有分解的證明任務被驗證後，CertiK平臺的後端將返回詳細而全面的評估報告。
開發使用者可以使用所有CertiK平臺的認證庫和IDE插件， 構建自己的DApp /系統，這需要花費一定的CTK。
打開 CertiK 的系統，上傳要檢測的智能合約，按下檢測按鈕。
檢測完畢後， CertiK 會提供這份智能合約的安全係數，並告訴你哪一塊程序存在著錯誤，並提供詳細的解決方案。
5.2 鏈安科技
提供幾種驗證服務：
• 第一個，安全審計
• 第二個，開發、審計一條龍
• 第三個，合約開發
其中安全審計模塊針對的漏洞包括代碼編程規範漏洞、代碼邏輯漏洞、函數調用漏洞、整型溢出漏洞、可重入攻擊漏洞、執行順序依賴漏洞、時間戳依賴漏洞、平臺接口誤用漏洞。
鏈安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)。
最後，根據前置條件證明代碼的執行是否滿足上述後置條件。如果產生一個不可證明結果，說明程序功能不正確，或者存在溢出安全漏洞。然後根據證明結果，對源程序進行分析修改，然後再重新證明，直到證明通過為止。鏈安採用這種數學的證明方式將代碼形式化描述為公式，並對其進行邏輯漏洞和安全漏洞證明，基於此原理，實現了自動化的驗證工具，能夠方便、快速地驗證出代碼的功能正確性和安全屬性。
6 智能合約的重大漏洞例舉
6.1 TheDAO
2016年6月17日，一名黑客在編碼上發現了漏洞，使得他可以從The Dao上抽走資金。在攻擊的頭幾個小時，360萬的以太被轉出，在當時價值相當於七千萬美元，今天則達到了21億美元。黑客達成了他想要的破壞，退出了攻擊。
在此漏洞中，攻擊者能夠“請求”智能合同( DAO )多次返回以太，且都是在智能合約更新它的餘額前進行的。兩個主要問題使它成為可能：一是在創建DAO智能合約時，編碼人員沒有考慮到遞歸調用的可能性；二是智能合約首先發送ETH資金，然後再更新內部token餘額。
重要的是要了解這個bug不是來自以太坊本身，而是來自基於以太坊上的構建應用程序。為DAO編寫的代碼有多個缺陷，遞歸調用的漏洞就是其中之一。
另外一種理解它的方式是比較。以太坊比作是互聯網，基於以太坊的應用比作是網站。也就是說，如果網站不運行，不意味著整個互聯網出問題。它只能說明網站有問題。
7其他常見安全類項目介紹
7.1 Sentinel Protocol
韓國團隊，基於ICON的第二個項目。項目目的是要創建一個多中心化的聲譽系統，通過集體智能和人工智能相結合，將所有數字貨幣的粘片，黑客信息，可疑錢包地址等各種信息記錄在區塊鏈上。
