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

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

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

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

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

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

在合約開(kāi)發(fā)前，開(kāi)發(fā)者應(yīng)進(jìn)行智能合約相關(guān)漏洞風(fēng)險(xiǎn)知識(shí)學(xué)習(xí)，了解最新的智能合約安全漏洞，避免開(kāi)發(fā)的合約中存在安全隱患。

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

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

01 智能合約形式化驗(yàn)證應(yīng)用狀況

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

形式化驗(yàn)證指的是用數(shù)學(xué)中的形式化方法對(duì)算法的性質(zhì)進(jìn)行證明或證偽。

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

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

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

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

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

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

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

“其實(shí)那個(gè)時(shí)候真的沒(méi)有太在意。不過(guò)我有一個(gè)朋友在搞區(qū)塊鏈，他跟我說(shuō)你搞形式化驗(yàn)證，能不能去驗(yàn)證一下智能合約的安全，比如針對(duì)Dao系統(tǒng)的安全事件。”楊霞回憶道，“我覺(jué)得挺有趣的就去試了一下。那時(shí)候我們還沒(méi)有自動(dòng)化的工具，只能靠人工進(jìn)行代碼的形式化描述，然后去證明。最后發(fā)現(xiàn)，形式化驗(yàn)證方法應(yīng)用于智能合約安全審計(jì)效果不錯(cuò)。”

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

目前，鏈安的VaaS平臺(tái)支持EOS和以太坊的智能合約的安全審計(jì)，VaaS也是全球第一個(gè)支持EOS的智能合約驗(yàn)證平臺(tái)。

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

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

形式化驗(yàn)證通過(guò)數(shù)學(xué)建模的方式，對(duì)合約進(jìn)行驗(yàn)證，發(fā)現(xiàn)合約的未知的潛在的風(fēng)險(xiǎn)。

因?yàn)槭怯脭?shù)學(xué)證明的方式去發(fā)現(xiàn)問(wèn)題，所以首先需要一個(gè)函數(shù)的詳細(xì)功能規(guī)范，形式化驗(yàn)證就依據(jù)這個(gè)功能規(guī)范去證明實(shí)際的代碼是不是和需求一致，如果是函數(shù)的規(guī)范足夠完整并且能夠清楚無(wú)歧義的表達(dá)，那么是可以發(fā)現(xiàn)針對(duì)這個(gè)被驗(yàn)證的函數(shù)之前沒(méi)有發(fā)現(xiàn)的問(wèn)題。

形式化的抽象可以從復(fù)雜的事物中抽離出本質(zhì)。舉個(gè)簡(jiǎn)單的例子，一個(gè)構(gòu)造復(fù)雜的中式?jīng)鐾ぃ?jīng)過(guò)形式化的方法抽象過(guò)后，可能只是一個(gè)分層的三角形，這就相當(dāng)于一個(gè)精簡(jiǎn)的解讀。

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

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

03 智能合約小白級(jí)漏洞居多

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

楊霞老師表示，就智能合約來(lái)講，80%都存在安全問(wèn)題。

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

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

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

這是一個(gè)很簡(jiǎn)單的邏輯，但是后果卻很嚴(yán)重。

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

其實(shí)，這些漏洞在智能合約正式開(kāi)始運(yùn)行之前，都是可以通過(guò)形式化驗(yàn)證的方式找出來(lái)的，并加以修復(fù)的。

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

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

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

第二，我們?cè)诩夹g(shù)上有優(yōu)勢(shì)，我們采用了嚴(yán)格的形式化驗(yàn)證的方法，為智能合約提供更加完備的安全審計(jì)。

第三，我們率先研發(fā)了自動(dòng)化的智能合約安全驗(yàn)證工具VaaS，在智能合約的審計(jì)過(guò)程中，我們通過(guò)自動(dòng)化工具VaaS和人工結(jié)合的方法比全人工的安全審計(jì)方式更準(zhǔn)確、更高效。

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

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

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

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