成都鏈安科技CEO楊霞：80%的智能合約都存在安全漏洞

騰訊安全日前發(fā)布的報告顯示，與加密數(shù)字貨幣有關的黑客攻擊事件，從 2013年到2018年上半年增加了約五倍，全年預計增加10倍左右。其中，僅今年上半年，黑客對加密數(shù)字貨幣的攻擊，就已經(jīng)造成了20億美元的直接損失。

基于區(qū)塊鏈加密數(shù)字貨幣引發(fā)的安全問題，來源于區(qū)塊鏈自身機制安全、生態(tài)安全和使用者安全三個方面。在區(qū)塊鏈自身機制安全方面，智能合約的安全性至關重要。

據(jù)鏈安方面的數(shù)據(jù)顯示，2011年至2018年，由智能合約安全事件導致的經(jīng)濟損失達12.4億美元。目前，由智能合約安全事件導致的經(jīng)濟損失已經(jīng)超越交易所，位列第一。

智能合約作為執(zhí)行合約條款的計算機交易協(xié)議，對所有用戶都開放，導致了內部存在的安全漏洞也隨之公開暴露在黑客面前。

而且，智能合約一旦上傳即公開且不可更改，因此現(xiàn)在的區(qū)塊鏈項目，對于安全性的需求更加迫切。因此，在智能合約正式開始運行之前進行安全審計就顯得尤為重要。

鏈安科技創(chuàng)始人兼CEO楊霞表示，從目前研究來看，80%的智能合約都存在安全漏洞。在合約開發(fā)前、開發(fā)過程中和編寫完成后，整個項目周期都要保證智能合約的安全性。

在合約開發(fā)前，開發(fā)者應進行智能合約相關漏洞風險知識學習，了解最新的智能合約安全漏洞，避免開發(fā)的合約中存在安全隱患。

在開發(fā)過程中，Remix-IDE、truffle等編譯工具會對合約中不符合最新規(guī)范的代碼提出告警，開發(fā)者需要對告警引起重視，強烈建議開發(fā)者更改自己的代碼，以消除編譯過程中的告警。

在合約編寫完成后，需要對合約功能的完整性和安全性進行測試，確保合約邏輯實現(xiàn)與設計相符，確保無安全風險；最后，可以尋找專業(yè)的智能合約審計團隊進行合約審計，最大程度地減少安全隱患。

01 智能合約形式化驗證應用狀況

2016年9月1日，萬向區(qū)塊鏈實驗室肖風在為《區(qū)塊鏈革命》作序時曾寫道：“The Dao”事件提醒我們，應該有一個能對智能合約進行事先檢驗的科學方法，但這方面最先進的技術如形式化驗證，目前還處于理論研究階段。”可是如今形式化驗證已經(jīng)被正式用于智能合約的檢驗中了，這就是技術的進步。

形式化驗證指的是用數(shù)學中的形式化方法對算法的性質進行證明或證偽。

據(jù)了解，一般來講，方法有兩種：

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

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

目前區(qū)塊鏈產(chǎn)業(yè)中與形式化驗證相關的產(chǎn)品可以分為三類:  VaaS平臺，公鏈和語言。

目前，主要從事智能合約形式化認證的區(qū)塊鏈安全公司主要有7家，分別是成都鏈安科技、Imandra、Certik、The Matrix、Securify.ch、Runtime Verification和Tezos。其中，從事VaaS形式化驗證平臺研發(fā)的有四家，分別是：成都鏈安科技、Certik、Securify.ch和Runtime Verification。

其中，鏈安的特色在于：提供多個區(qū)塊鏈平臺驗證工具，而不是單一地為以太坊或者EOS提供智能合約形式化驗證。

楊霞是2016年才開始接觸區(qū)塊鏈的，正趕上了著名的以太坊The Dao事件，在此之前，楊霞老師一直專注于為航空航天、軍事領域提供形式化驗證服務。

“其實那個時候真的沒有太在意。不過我有一個朋友在搞區(qū)塊鏈，他跟我說你搞形式化驗證，能不能去驗證一下智能合約的安全，比如針對Dao系統(tǒng)的安全事件?！睏钕蓟貞浀溃拔矣X得挺有趣的就去試了一下。那時候我們還沒有自動化的工具，只能靠人工進行代碼的形式化描述，然后去證明。最后發(fā)現(xiàn)，形式化驗證方法應用于智能合約安全審計效果不錯?！?/p>

也許當時選擇將形式化驗證應用于區(qū)塊鏈智能合約的審計是一個偶然的機遇，但是，通過楊霞和她的團隊經(jīng)過一年半左右的潛心研究研發(fā)出了自動化的智能合約安全驗證平臺VaaS。

目前，鏈安的VaaS平臺支持EOS和以太坊的智能合約的安全審計，VaaS也是全球第一個支持EOS的智能合約驗證平臺。

02 形式化方法像一套完備的法律

被問到如何向技術小白解釋形式化認證，楊霞表示“形式化方法就像一套完備的法律，規(guī)定了每個角色能做什么和不能做什么，并對角色之間的關系進行界定。類似于社會系統(tǒng)架構對不同角色進行分類，在承認個體天性的同時，使系統(tǒng)的復雜程度降低了多個維度?！?/strong>

形式化驗證通過數(shù)學建模的方式，對合約進行驗證，發(fā)現(xiàn)合約的未知的潛在的風險。

因為是用數(shù)學證明的方式去發(fā)現(xiàn)問題，所以首先需要一個函數(shù)的詳細功能規(guī)范，形式化驗證就依據(jù)這個功能規(guī)范去證明實際的代碼是不是和需求一致，如果是函數(shù)的規(guī)范足夠完整并且能夠清楚無歧義的表達，那么是可以發(fā)現(xiàn)針對這個被驗證的函數(shù)之前沒有發(fā)現(xiàn)的問題。

形式化的抽象可以從復雜的事物中抽離出本質。舉個簡單的例子，一個構造復雜的中式?jīng)鐾?，?jīng)過形式化的方法抽象過后，可能只是一個分層的三角形，這就相當于一個精簡的解讀。

在驗證安全之后，通過使用可執(zhí)行模型，將較高級別的抽象模型轉換為較低級別的代碼。形式化方法使智能合約的生成和執(zhí)行有了規(guī)范性約束，保證了合約的可信性，使智能合約的生產(chǎn)過程和執(zhí)行效果得到了保障。

據(jù)楊霞表示，目前，理論上講，形式化認證可以找出所有已知的和未知的智能合約安全漏洞。而實際操作中，形式化工具可以查出80%的常規(guī)漏洞，對于部分結合業(yè)務邏輯的漏洞，還需要人工復核。

03 智能合約小白級漏洞居多

區(qū)塊鏈行業(yè)的安全漏洞是不斷涌現(xiàn)的，尤其是涉及到“錢”的安全漏洞，可以使人們的數(shù)字資產(chǎn)瞬時歸零。目前，隨著漏洞不斷被挖出，很多數(shù)字資產(chǎn)投資者也陷入到了恐慌之中。

楊霞老師表示，就智能合約來講，80%都存在安全問題。

就目前看來，智能合約中還是小白級的錯誤居多，包括一些造成巨額財產(chǎn)損失的漏洞。

舉個例子，2018年4 月 22 日 13 時左右BEC智能合約被爆出的整數(shù)溢出漏洞，黑客能無限印幣，在一次交易中，也就那么幾秒鐘的事情，黑客就“無中生有”地給兩個賬戶轉了天文數(shù)字般的BEC幣，而原賬戶一分BEC幣都沒損失。一行代碼就造成了60多億人民幣的損失。

整數(shù)溢出就像是水輪車。往里面加水，加滿之后，繼續(xù)加水，水輪車將會失衡并轉動，此時水將會被全部倒出來，并重新盛水。當變量累加到超過自身容量范圍時，將會溢出，歸零。而黑客也是利用了這一點，把運算前的數(shù)值作為轉賬金額，把運算后溢出的0作為檢測條件，從而實現(xiàn)繞過。

這是一個很簡單的邏輯，但是后果卻很嚴重。

同樣，之前爆出來的以太坊平臺的漏洞，短地址攻擊，以及拒絕服務攻擊等等的漏洞的邏輯也都很簡單，但是這些漏洞都造成了人們數(shù)字資產(chǎn)的巨大損失。

其實，這些漏洞在智能合約正式開始運行之前，都是可以通過形式化驗證的方式找出來的，并加以修復的。

鏈安采用數(shù)學的證明方式將代碼形式化描述為公式，并對其進行邏輯漏洞和安全漏洞證明，基于此原理，實現(xiàn)了自動化的驗證工具，能夠方便、快速地驗證出代碼的功能正確性和安全屬性。

楊霞老師表示，目前，成都鏈安科技的優(yōu)勢集中體現(xiàn)在三個方面：

第一，我們專注只做智能合約的安全。

第二，我們在技術上有優(yōu)勢，我們采用了嚴格的形式化驗證的方法，為智能合約提供更加完備的安全審計。

第三，我們率先研發(fā)了自動化的智能合約安全驗證工具VaaS，在智能合約的審計過程中，我們通過自動化工具VaaS和人工結合的方法比全人工的安全審計方式更準確、更高效。

對于未來區(qū)塊鏈安全的走向，楊霞老師表示，安全是一個持續(xù)完善的過程，沒有絕對的安全，越是復雜的軟件系統(tǒng)，出現(xiàn)安全事件的概率越高。

為了避免安全事件的發(fā)生，最好的辦法就是提高軟件開發(fā)人員的安全意識，并對智能合約在部署之前進行全面的安全審計。

我們要理智地看待區(qū)塊鏈技術的漏洞，區(qū)塊鏈作為一個新興技術，出現(xiàn)安全事件是可以理解的，不能因噎廢食。

【本文為投資家網(wǎng)原創(chuàng)文章，轉載或內容合作請聯(lián)系投資家網(wǎng)，違規(guī)轉載，法律必究。】