隨著平臺(tái)級(jí)應(yīng)用的普遍化，智能合約涉及的金額呈指數(shù)級(jí)別增長(zhǎng)瘟檩，智能合約的安全問(wèn)題也成為投資者和開(kāi)發(fā)者共同關(guān)注的焦點(diǎn)垛膝。今年以來(lái)有數(shù)個(gè)基于ERC-20的ICO項(xiàng)目因?yàn)橹悄芎霞s代碼出現(xiàn)漏洞而遭到黑客攻擊稽揭，導(dǎo)致投資者巨額的損失。為了防止類(lèi)似事件的發(fā)生党巾，交易所、錢(qián)包霜医、項(xiàng)目方等都在智能合約安全上加大投入齿拂，同時(shí)圍繞著智能合約安全的周邊生態(tài)成為目前投資的熱點(diǎn)。

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

作者：

節(jié)點(diǎn)研究中心??蔡晨曦 武怡 郎瀚威

ONE.TOP ?洪妙叢

支持機(jī)構(gòu)（排名不分先后）

金塔行情肴敛、星球日?qǐng)?bào)署海、金色財(cái)經(jīng)、babi財(cái)經(jīng)值朋、節(jié)點(diǎn)財(cái)經(jīng)

（本報(bào)告由ONE.TOPX節(jié)點(diǎn)研究中心聯(lián)合發(fā)布）

智能合約安全方面的措施總體來(lái)說(shuō)分為以上幾個(gè)大類(lèi)叹侄，合約開(kāi)發(fā)模板巩搏、合約審計(jì)昨登、智能合約語(yǔ)言設(shè)計(jì)和賞金獵人機(jī)制。

1）合約開(kāi)發(fā)模板如OpenZeppelin贯底、Etherparty等為標(biāo)準(zhǔn)化的合約提供經(jīng)過(guò)多次實(shí)戰(zhàn)驗(yàn)證的標(biāo)準(zhǔn)化模板丰辣，在節(jié)約時(shí)間同時(shí)保證合約安全性。

2）合約審計(jì)的方法又分為人工審計(jì)和機(jī)器輔助審計(jì)

3）機(jī)器輔助審計(jì)又分為規(guī)則驗(yàn)證禽捆、語(yǔ)義驗(yàn)證和形式化驗(yàn)證笙什，而形式化驗(yàn)證是本文關(guān)注的重點(diǎn)。

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

智能合約語(yǔ)言設(shè)計(jì)中胚想，許多公鏈平臺(tái)開(kāi)始采用Haskell或OCaml一類(lèi)的函數(shù)式語(yǔ)言琐凭，因?yàn)楹瘮?shù)式語(yǔ)言更為便于編寫(xiě)形式化驗(yàn)證方面的開(kāi)發(fā)者庫(kù)和工具。賞金獵人機(jī)制浊服，相對(duì)于前幾項(xiàng)措施统屈，更多是部署合約后發(fā)現(xiàn)漏洞的彌補(bǔ)機(jī)制。

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

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

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

目前為止炼幔，形式化驗(yàn)證主要應(yīng)用在軍工秋茫、航天等對(duì)系統(tǒng)安全非常高的領(lǐng)域，在消費(fèi)級(jí)軟件領(lǐng)域幾乎沒(méi)有應(yīng)用江掩。由于傳統(tǒng)互聯(lián)網(wǎng)應(yīng)用與區(qū)塊鏈應(yīng)用的運(yùn)行環(huán)境有著本質(zhì)的不同学辱，其開(kāi)發(fā)流程也應(yīng)當(dāng)相應(yīng)地進(jìn)行調(diào)整乘瓤，其中最關(guān)鍵點(diǎn)在于安全驗(yàn)證環(huán)節(jié)的投入比例。

在傳統(tǒng)互聯(lián)網(wǎng)應(yīng)用中策泣，由于普遍采用中心化服務(wù)器+客戶(hù)端的模型衙傀，如果應(yīng)用出現(xiàn)安全隱患只需要對(duì)服務(wù)器端代碼進(jìn)行修改就可以輕松排雷，并且服務(wù)器端可以對(duì)用戶(hù)數(shù)據(jù)進(jìn)行回滾以挽回用戶(hù)損失萨咕。因此统抬，傳統(tǒng)互聯(lián)網(wǎng)應(yīng)用開(kāi)發(fā)的過(guò)程較為注重快速迭代，以犧牲安全性換取效率和功能上的快速升級(jí)危队。

在區(qū)塊鏈應(yīng)用中聪建，由于區(qū)塊鏈的不可篡改性，智能合約一旦上線(xiàn)并出現(xiàn)安全隱患茫陆，對(duì)用戶(hù)造成的損失是巨大且不可挽回的金麸。一旦出現(xiàn)黑客事件，需要整個(gè)社區(qū)的共識(shí)才能回滾交易簿盅，所以每次遭受攻擊都回滾交易也是不現(xiàn)實(shí)的挥下。因此，區(qū)塊鏈應(yīng)用開(kāi)發(fā)的過(guò)程需要用大量的測(cè)試和檢驗(yàn)以獲取足夠的安全性桨醋，而反過(guò)來(lái)犧牲迭代的速度棚瘟。

由于區(qū)塊鏈開(kāi)發(fā)人員的稀缺，遠(yuǎn)遠(yuǎn)無(wú)法趕上智能合約數(shù)量的增長(zhǎng)喜最，人工審計(jì)智能合約是成本非常高昂的偎蘸，因此機(jī)器輔助驗(yàn)證是目前的必然趨勢(shì)。規(guī)則瞬内、語(yǔ)義驗(yàn)證的實(shí)現(xiàn)迷雪，相對(duì)較為容易，技術(shù)門(mén)檻也較低遂鹊，但是只能進(jìn)行一些淺層的糾錯(cuò)振乏，不能深入程式的邏輯。因此秉扑，只有形式化驗(yàn)證方法有希望真正提高智能合約審計(jì)的自動(dòng)化程度慧邮。

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

項(xiàng)目 名稱(chēng)?分類(lèi)?描述?創(chuàng)始團(tuán)隊(duì)背景

CertiK ????Vaas ????結(jié)合證明引擎和賞金獵人的綜合性安全驗(yàn)證平臺(tái) ????哥大/耶魯

Imandra????語(yǔ)言????OCaml子語(yǔ)言，專(zhuān)注于金融交易系統(tǒng)的形式化驗(yàn)證????倫敦金融城/英國(guó)劍橋

鏈安科技????Vaas????提供多個(gè)區(qū)塊鏈平臺(tái)驗(yàn)證工具秦躯，以及將合約代碼轉(zhuǎn)成定理的證明工具????電子科技大學(xué)

The Matrix????公鏈????基于AI輔助的形式驗(yàn)證以及動(dòng)態(tài)約束檢查????????清華/北大

Securify.ch ????Vaas ????一鍵對(duì)以太坊智能合約進(jìn)行形式化驗(yàn)證 ETH Zurich

Runtime Verification Vaas 使用自己開(kāi)發(fā)的K框架對(duì)虛擬機(jī)二進(jìn)制碼進(jìn)行形式化驗(yàn)證 ????UIUC

Tezos? ? 公鏈????用函數(shù)式編程語(yǔ)言Michelson作為智能合約語(yǔ)言忆谓，方便形式化驗(yàn)證? ? ? ?華爾街/R3

3.1 Vaas平臺(tái)

Vaas平臺(tái)是直接面向開(kāi)發(fā)者提供形式化驗(yàn)證服務(wù)的平臺(tái)。目前Vaas類(lèi)項(xiàng)目包括CertiKzecurify.ch踱承、Runtime Verification等項(xiàng)目倡缠。目前哨免，CertiK仍在募資階段，鏈安科技據(jù)稱(chēng)已經(jīng)有研發(fā)成功及獲得專(zhuān)利的產(chǎn)品昙沦，Securify.ch的測(cè)試版已經(jīng)上線(xiàn)琢唾，而Runtime Verification已經(jīng)在商業(yè)運(yùn)營(yíng)。

與其它幾個(gè)項(xiàng)目不同盾饮，RuntimeVerification是基于EVM虛擬機(jī)二進(jìn)制碼進(jìn)行形式化驗(yàn)證采桃，而非針對(duì)智能合約本身用的高級(jí)語(yǔ)言，因此在安全性上又更進(jìn)一步丘损，避免了因編譯器編譯過(guò)程中可能產(chǎn)生的漏洞普办。

3.2語(yǔ)言

語(yǔ)言類(lèi)產(chǎn)品一般為函數(shù)式語(yǔ)言的子語(yǔ)言，提供與智能合約形式化驗(yàn)證相關(guān)的開(kāi)發(fā)者庫(kù)和工具徘钥，目前有Imandra和Tezos等項(xiàng)目衔蹲。

其中，Imandra發(fā)布了一套開(kāi)源的以太坊虛擬機(jī)用ImandraML語(yǔ)言標(biāo)記的模型吏饿，并且專(zhuān)注于交易所等金融應(yīng)用場(chǎng)景的形式化驗(yàn)證踪危，用以確保金融交易的合法合規(guī)，據(jù)稱(chēng)相關(guān)技術(shù)已經(jīng)用于華爾街頂級(jí)投行的交易系統(tǒng)猪落。

3.3 公鏈

直接包含形式化驗(yàn)證引擎的公鏈產(chǎn)品目前只有The Matrix項(xiàng)目，特征是基于AI輔助的形式化驗(yàn)證及動(dòng)態(tài)約束的檢查畴博。AI是否對(duì)于形式化驗(yàn)證的自動(dòng)化帶來(lái)幫助在技術(shù)上仍是個(gè)未知數(shù)笨忌，因此這個(gè)項(xiàng)目也將成為這個(gè)領(lǐng)域的試金石。

Certik鏈安科技runtime?

verification

創(chuàng)始人邵忠俱病，耶魯大學(xué)計(jì)算機(jī)科學(xué)博士官疲；顧榮輝，哥倫比亞助理教授楊霞女士亮隙，電子科技大學(xué)副教授途凫、博士后Daejun Park，首爾國(guó)立大學(xué)計(jì)算機(jī)科學(xué)與工程學(xué)士學(xué)位和碩士學(xué)位溢吻，目前正在攻讀博士學(xué)位

核心團(tuán)隊(duì)核心成員來(lái)自哥倫比亞大學(xué)维费、耶魯大學(xué)和普林斯頓大學(xué)，專(zhuān)業(yè)背景都是計(jì)算機(jī)技術(shù)促王，團(tuán)隊(duì)技術(shù)實(shí)力強(qiáng)硬20多名來(lái)自海外知名高校和實(shí)驗(yàn)室(CSDS/耶魯/UCLA)留學(xué)經(jīng)歷的副教授犀盟、博士后、博士蝇狼、碩士組成核心團(tuán)隊(duì)成員大部分都有形式化驗(yàn)證方向的研究和學(xué)習(xí)經(jīng)歷

合作伙伴量子鏈阅畴、INT、菩提火幣網(wǎng)迅耘、OK資本贱枣、比原鏈监署、布比區(qū)塊鏈、云象區(qū)塊鏈NSF纽哥、NASA焦匈、Ethereum、Boeing

針對(duì)市場(chǎng)對(duì)基于以太坊上開(kāi)發(fā)的DAPP和系統(tǒng)進(jìn)行形式化驗(yàn)證對(duì)智能合約進(jìn)行形式化驗(yàn)證昵仅，支持以太坊和EOS致力于飛機(jī)缓熟，航天器和區(qū)塊鏈領(lǐng)域的軟件系統(tǒng)的安全性，可靠性和正確性

主要技術(shù)開(kāi)發(fā)了一個(gè)基于形式化驗(yàn)證的平臺(tái)摔笤，創(chuàng)新的使用了包括智能標(biāo)簽框架够滑、層級(jí)分解在內(nèi)的技術(shù)，幫助實(shí)現(xiàn)自動(dòng)化的形式化驗(yàn)證高度自動(dòng)化的智能合約安全審計(jì)平臺(tái)VaaS吕世，再以人工方式對(duì)智能合約代碼逐行復(fù)核彰触，保證審計(jì)質(zhì)量用自己研發(fā)的runtime驗(yàn)證技術(shù)對(duì)對(duì)智能合約進(jìn)行形式化驗(yàn)證工作

5.1

Certik

Certik是一個(gè)是形式化驗(yàn)證框架，經(jīng)過(guò)certik驗(yàn)證的智能合同命辖、DApp以及區(qū)塊鏈將會(huì)被附上證書(shū)形式的標(biāo)志况毅，來(lái)展示其正確性和安全性。Certik平臺(tái)提供的主要功能包括以下部分尔艇。

智能標(biāo)簽框架

CertiK平臺(tái)應(yīng)用深度學(xué)習(xí)技術(shù)來(lái)構(gòu)建智能標(biāo)簽框架尔许，有了這個(gè)框架，大多數(shù)共享邏輯和屬性代碼（前置條件终娃，后置條件味廊，不變量等）都可以被自動(dòng)標(biāo)記，從而使得程序的邏輯棠耕，語(yǔ)義更加清晰和規(guī)范余佛，這樣驗(yàn)證的工作量就可以大大減少。

基于層的分解

這種技術(shù)揭示了分層設(shè)計(jì)模式的見(jiàn)解窍荧，并使得將復(fù)雜的證明任務(wù)分解為更小的任務(wù)成為可能辉巡，并在適當(dāng)?shù)某橄髮用骝?yàn)證它們中的每一個(gè)。

可插拔的驗(yàn)證引擎

提供開(kāi)放式的協(xié)議蕊退，更先進(jìn)算法的證明引擎可以自由插入這個(gè)系統(tǒng)郊楣。

機(jī)器可檢驗(yàn)的證明對(duì)象

構(gòu)建機(jī)械式的證明對(duì)象（或者反例），這些證明對(duì)象可以快速的被任何人檢驗(yàn)咕痛，同時(shí)作為驗(yàn)證程序的證書(shū)（機(jī)械式證明對(duì)象可直接作為證書(shū)痢甘，賞金獵人提供的證明對(duì)象，需要檢察官進(jìn)行人工檢驗(yàn)后才能作為證書(shū)茉贡。注：賞金獵人和檢察官后文會(huì)進(jìn)行描述塞栅。）

認(rèn)證的DAPP庫(kù)

為集成開(kāi)發(fā)環(huán)境提供了一系列認(rèn)證庫(kù)和插件，以便開(kāi)發(fā)出質(zhì)量更高的dapp，但是會(huì)花費(fèi)一些CTK放椰。

定制化的認(rèn)證服務(wù)

如果有高可靠性要求作烟，可以提供定制化的認(rèn)證服務(wù)，由驗(yàn)證領(lǐng)域的專(zhuān)家提供幫助并出具綜合報(bào)告砾医。

Certik平臺(tái)圍繞bug的檢測(cè)和修復(fù)建立了一個(gè)去中心化的生態(tài)拿撩，該生態(tài)由五個(gè)角色構(gòu)成，分別是客戶(hù)如蚜、賞金獵人压恒、檢查官、社區(qū)貢獻(xiàn)者以及開(kāi)發(fā)使用者错邦，該生態(tài)工運(yùn)行模式如下圖所示探赫。

該系統(tǒng)可以分為機(jī)械化部分和人工部分∏四兀客戶(hù)在certik平臺(tái)上提交dapp或者程序系統(tǒng)伦吠，平臺(tái)自動(dòng)為其添加智能標(biāo)簽，并自動(dòng)進(jìn)行分解魂拦，形成小模塊的證明任務(wù)毛仪，這個(gè)環(huán)節(jié)客戶(hù)需要消耗一定量的CTK。

分解完小模塊后芯勘，系統(tǒng)由兩種方式進(jìn)行驗(yàn)證箱靴，簡(jiǎn)單的證明任務(wù)可以由一些自動(dòng)驗(yàn)證器(例如SMT解算器)解決。除了平臺(tái)內(nèi)部自帶的驗(yàn)證器（證明引擎）借尿，CertiK平臺(tái)提供開(kāi)放協(xié)議刨晴，社區(qū)貢獻(xiàn)者可以將帶有更高級(jí)的求解算法的證明引擎自由地插入到該系統(tǒng)中，并獲得一些CTK獎(jiǎng)勵(lì)路翻。賞金獵人可以隨機(jī)使用他們的引擎，并進(jìn)行評(píng)估茄靠，優(yōu)秀的引擎將被社區(qū)研究和推廣茂契。

另一種驗(yàn)證方式針對(duì)較為復(fù)雜的證明任務(wù)。賞金獵人接到該任務(wù)后慨绳，構(gòu)建一個(gè)證明對(duì)象并進(jìn)行廣播掉冶，接著檢查官對(duì)證明對(duì)象進(jìn)行檢測(cè)，當(dāng)證明對(duì)象驗(yàn)證通過(guò)后脐雪，會(huì)被貼上證書(shū)的標(biāo)簽厌小，賞金獵人和檢查官分別獲得CTK獎(jiǎng)勵(lì)。

所有分解的證明任務(wù)被驗(yàn)證后战秋，CertiK平臺(tái)的后端將返回詳細(xì)而全面的評(píng)估報(bào)告璧亚。

開(kāi)發(fā)使用者可以使用所有CertiK平臺(tái)的認(rèn)證庫(kù)和IDE插件， 構(gòu)建自己的DApp /系統(tǒng)脂信，這需要花費(fèi)一定的CTK癣蟋。

以下是certik的操作界面

打開(kāi) CertiK 的系統(tǒng)透硝，上傳要檢測(cè)的智能合約，按下檢測(cè)按鈕

檢測(cè)完畢后疯搅，CertiK 會(huì)提供這份智能合約的安全系數(shù)濒生，并告訴你哪一塊程序存在著錯(cuò)誤，并提供詳細(xì)的解決方案

5.2鏈安科技

提供幾種驗(yàn)證服務(wù)：

????第一個(gè)幔欧，安全審計(jì)

????第二個(gè)罪治，開(kāi)發(fā)、審計(jì)一條龍

????第三個(gè)礁蔗，合約開(kāi)發(fā)

其中安全審計(jì)模塊針對(duì)的漏洞包括代碼編程規(guī)范漏洞觉义、代碼邏輯漏洞、函數(shù)調(diào)用漏洞瘦麸、整型溢出漏洞谁撼、可重入攻擊漏洞、執(zhí)行順序依賴(lài)漏洞滋饲、時(shí)間戳依賴(lài)漏洞厉碟、平臺(tái)接口誤用漏洞。

鏈安CEO通過(guò)一個(gè)例子從數(shù)學(xué)原理上對(duì)形式化驗(yàn)證進(jìn)行了描述說(shuō)明屠缭。以近期頻發(fā)的溢出類(lèi)安全漏洞屬性檢查為例箍鼓，如檢查代碼

int8 c=a+b

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

首先款咖，對(duì)整數(shù)類(lèi)型建模，定義形式化規(guī)則：

Int8.repr: Z -> int8

該規(guī)則通過(guò)截取純數(shù)學(xué)整數(shù)（取值范圍從無(wú)窮小到無(wú)窮大）的低8位數(shù)值得到一個(gè)8位長(zhǎng)度的機(jī)器整數(shù)奄喂。然后寫(xiě)加法運(yùn)算的形式化規(guī)范铐殃，如下：

{a:int8,b:int8} //?

設(shè)置代碼執(zhí)行的前提條件，保證a和b的類(lèi)型是8位有符號(hào)機(jī)器整數(shù);

{c = a + b;} //?

加法運(yùn)算的源碼程序跨新；

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

設(shè)置代碼正確執(zhí)行的后置條件富腊。

其中，(int8.repr(a+b))描述域帐，是為了證明代碼的功能正確性是否滿(mǎn)足赘被，即需要證明源代碼是對(duì)a和b進(jìn)行求和而不是求差或任何其他運(yùn)算邏輯，并且將運(yùn)算結(jié)果轉(zhuǎn)換為int8類(lèi)型肖揣。此外民假，需要對(duì)是否溢出的安全屬性進(jìn)行證明，因此添加后置條件：

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

因?yàn)橐坏?/p>

a+b>int8.max_singed?

或

a+b

都將導(dǎo)致

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

最后龙优，根據(jù)前置條件證明代碼的執(zhí)行是否滿(mǎn)足上述后置條件羊异。如果產(chǎn)生一個(gè)不可證明結(jié)果，說(shuō)明程序功能不正確，或者存在溢出安全漏洞球化。然后根據(jù)證明結(jié)果秽晚，對(duì)源程序進(jìn)行分析修改，然后再重新證明筒愚，直到證明通過(guò)為止赴蝇。鏈安采用這種數(shù)學(xué)的證明方式將代碼形式化描述為公式，并對(duì)其進(jìn)行邏輯漏洞和安全漏洞證明巢掺，基于此原理句伶，實(shí)現(xiàn)了自動(dòng)化的驗(yàn)證工具，能夠方便陆淀、快速地驗(yàn)證出代碼的功能正確性和安全屬性考余。

5.3 runtime verification

RuntimeVerification Inc.是一家初創(chuàng)公司，通過(guò)使用自己研發(fā)的runtime驗(yàn)證技術(shù)致力于提高汽車(chē)轧苫，飛機(jī)楚堤，航天器和區(qū)塊鏈領(lǐng)域的軟件系統(tǒng)的安全性，可靠性和正確性含懊。從2001年開(kāi)始身冬，runtime verification就成為NASA的研究科學(xué)家。

Runtime驗(yàn)證技術(shù)依賴(lài)于程序執(zhí)行不應(yīng)違反某些屬性的原理岔乔。其中一些屬性酥筝，如并發(fā)程序中缺少數(shù)據(jù)競(jìng)爭(zhēng)，具有通用性雏门，可以自動(dòng)檢查嘿歌。其他屬性，如專(zhuān)用庫(kù)的規(guī)格茁影，是針對(duì)特定應(yīng)用程序或用途定制的宙帝。Runtime驗(yàn)證技術(shù)可以自動(dòng)檢查通用屬性，不需要開(kāi)發(fā)輸入募闲，并且可以檢查開(kāi)發(fā)人員用形式化方式表達(dá)的任何定制屬性茄唐。

在區(qū)塊鏈方面，runtime公司主要對(duì)智能合約進(jìn)行形式化驗(yàn)證工作蝇更，驗(yàn)證步驟包括：

（1）形式化

根據(jù)智能合約所有者提供的非形式化規(guī)則，對(duì)智能合約的高級(jí)業(yè)務(wù)邏輯進(jìn)行形式化呼盆。

（2）確認(rèn)

形式化后的高級(jí)業(yè)務(wù)邏輯需要由智能合約的所有者確認(rèn)年扩，可能需要經(jīng)過(guò)多輪討論和修改，才能確保它能正確捕捉合同的預(yù)期行為访圃。

（3）提煉

通過(guò)多個(gè)步驟將形式化后的規(guī)則完善到虛擬機(jī)級(jí)別厨幻，以捕獲虛擬機(jī)特定的細(xì)節(jié)。最終的虛擬機(jī)級(jí)別規(guī)則的作用是確保在字節(jié)碼級(jí)別沒(méi)有意外發(fā)生，也就是說(shuō)况脆，只有在執(zhí)行字節(jié)碼時(shí)才會(huì)發(fā)生高級(jí)規(guī)則中指定的內(nèi)容饭宾。

（4）編譯和測(cè)試

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

（5）驗(yàn)證

最后看铆，對(duì)智能合約的虛擬機(jī)字節(jié)碼與虛擬機(jī)的規(guī)則進(jìn)行形式化驗(yàn)證，通過(guò)這樣的方式不用依賴(lài)編譯器的正確性盛末。同時(shí)弹惦，runtime使用自己研發(fā)的K-framework結(jié)構(gòu)演繹驗(yàn)證程序， 以達(dá)到嚴(yán)格推理虛擬機(jī)字節(jié)碼而不遺漏任何虛擬機(jī)怪癖的效果悄但。

6.1The

DAO

2016年6月17日棠隐，一名黑客在編碼上發(fā)現(xiàn)了漏洞，使得他可以從The Dao上抽走資金檐嚣。在攻擊的頭幾個(gè)小時(shí)助泽，360萬(wàn)的以太被轉(zhuǎn)出，在當(dāng)時(shí)價(jià)值相當(dāng)于七千萬(wàn)美元嚎京，今天則達(dá)到了21億美元嗡贺。黑客達(dá)成了他想要的破壞，退出了攻擊挖藏。

在此漏洞中暑刃，攻擊者能夠“請(qǐng)求”智能合同( DAO )多次返回以太，且都是在智能合約更新它的余額前進(jìn)行的膜眠。兩個(gè)主要問(wèn)題使它成為可能：一是在創(chuàng)建DAO智能合約時(shí)岩臣，編碼人員沒(méi)有考慮到遞歸調(diào)用的可能性；二是智能合約首先發(fā)送ETH資金宵膨，然后再更新內(nèi)部token余額架谎。

重要的是要了解這個(gè)bug不是來(lái)自以太坊本身，而是來(lái)自基于以太坊上的構(gòu)建應(yīng)用程序辟躏。為DAO編寫(xiě)的代碼有多個(gè)缺陷谷扣，遞歸調(diào)用的漏洞就是其中之一。

另外一種理解它的方式是比較捎琐。以太坊比作是互聯(lián)網(wǎng)会涎，基于以太坊的應(yīng)用比作是網(wǎng)站。也就是說(shuō)瑞凑，如果網(wǎng)站不運(yùn)行末秃，不意味著整個(gè)互聯(lián)網(wǎng)出問(wèn)題。它只能說(shuō)明網(wǎng)站有問(wèn)題籽御。

黑客出于未知的原因停止從TheDAO抽取資金练慕，盡管他可以繼續(xù)這么做惰匙。以太坊社區(qū)和團(tuán)隊(duì)很快就控制了局面，并提出了多項(xiàng)應(yīng)對(duì)攻擊的建議铃将。

然而项鬼，這些資金被存入一個(gè)賬戶(hù)，有一個(gè)28天鎖定期劲阎，黑客無(wú)法轉(zhuǎn)走绘盟。為了退還損失的錢(qián)，以太坊通過(guò)硬分叉把被黑資金退還到原所有者的賬戶(hù)上哪工。退還匯率是1 ETH兌100 DAO 奥此，與首次公開(kāi)發(fā)行時(shí)的匯率相同。

毫無(wú)意外雁比，黑客攻擊意味著DAO的終結(jié)稚虎。很多以太坊用戶(hù)質(zhì)疑硬分叉違反區(qū)塊鏈的基本信條。更糟糕的是偎捎，2016年9月5日蠢终，Poloniex交易所下架了DAO token，Kraken在2016年12月也下架了DAO token茴她。

與美國(guó)證券交易委員會(huì)(SEC)2017年7月25日發(fā)布的報(bào)告相比寻拂，以上的這些問(wèn)題都相形見(jiàn)絀。它提到：

“由一個(gè)名為“DAO”的“虛擬”組織提供和出售的代幣是證券丈牢，因此受聯(lián)邦證券法的約束祭钉。報(bào)告確認(rèn)，發(fā)行基于區(qū)塊鏈技術(shù)的證券發(fā)行者必須登記此類(lèi)證券的發(fā)行和銷(xiāo)售己沛，除非有有效的豁免慌核。參與未注冊(cè)發(fā)行的證券的人也可能要對(duì)違反證券法的行為負(fù)責(zé)∩昴幔”

換句話(huà)說(shuō)垮卓，TheDAO的發(fā)行與首次公開(kāi)發(fā)行(IPO)一樣，受到同樣監(jiān)管原則的約束师幕。按照SEC觀點(diǎn)粟按，DAO違反了聯(lián)邦證券法，所有投資者也一樣霹粥。

6.2 EDU

區(qū)塊鏈項(xiàng)目EDU智能合約中存在漏洞灭将。在一個(gè)名為transferFrom 函數(shù)中，缺少 Safemath 驗(yàn)證后控，利用溢出攻擊可以讓攻擊者從任何一個(gè) EDU 余額不為 0 的賬號(hào)內(nèi)向另外一個(gè)賬號(hào)轉(zhuǎn)出 任意數(shù)量的EDU Token宗侦。

由于目前EDU在火幣pro上線(xiàn)，黑客利用漏洞累積向火幣轉(zhuǎn)入了超過(guò)20億枚EDU忆蚀。這也導(dǎo)致了EDU的價(jià)格崩盤(pán)矾利。

7.1

Sentinel Protocol

韓國(guó)團(tuán)隊(duì)，基于ICON的第二個(gè)項(xiàng)目馋袜。項(xiàng)目目的是要?jiǎng)?chuàng)建一個(gè)去中心化的聲譽(yù)系統(tǒng)男旗，通過(guò)集體智能和人工智能相結(jié)合，將所有數(shù)字貨幣的粘片欣鳖，黑客信息察皇，可疑錢(qián)包地址等各種信息記錄在區(qū)塊鏈上。

7.2 Atonomi

要成為世界上第一個(gè)分布式物聯(lián)網(wǎng)安全協(xié)議泽台。

Atonomi利用區(qū)塊鏈上的特性與經(jīng)濟(jì)激勵(lì)什荣，利用Token注冊(cè)和驗(yàn)證評(píng)估系統(tǒng)，構(gòu)建出一個(gè)物聯(lián)網(wǎng)設(shè)備的認(rèn)證與信譽(yù)數(shù)據(jù)庫(kù)怀酷，保證每一臺(tái)加入網(wǎng)絡(luò)的設(shè)備稻爬，都擁有良好的信譽(yù)。同時(shí)蜕依，應(yīng)用母公司Centri的技術(shù)（Centri是傳統(tǒng)互聯(lián)網(wǎng)的安全公司桅锄，擁有多項(xiàng)安全方面的技術(shù)專(zhuān)利，并與很多互聯(lián)網(wǎng)大公司是合作伙伴）給設(shè)備加密样眠，確保數(shù)據(jù)隱私并阻止它被黑客利用來(lái)連接到別的物聯(lián)網(wǎng)設(shè)備友瘤。同時(shí)Atonomi的Token也像IOTA一樣支持設(shè)備之間的微支付需要。

7.3 Gladius

嚴(yán)格意義來(lái)講檐束，Gladius并不是一個(gè)保護(hù)區(qū)塊鏈的項(xiàng)目辫秧，而是一個(gè)利用區(qū)塊鏈技術(shù)，來(lái)保護(hù)傳統(tǒng)互聯(lián)網(wǎng)的項(xiàng)目被丧。

Gladius是利用存儲(chǔ)和流量的經(jīng)濟(jì)激勵(lì)盟戏，來(lái)創(chuàng)建基于區(qū)塊鏈的分布式CDN，從而實(shí)現(xiàn)DDoS攻擊的分散保護(hù)晚碾，同時(shí)創(chuàng)建一個(gè)大型流量池抓半，處理不斷出現(xiàn)的DDOS請(qǐng)求，提供比傳統(tǒng)DDOS防護(hù)更加經(jīng)濟(jì)和高效的方式格嘁。

Gladius的桌面客戶(hù)端允許用戶(hù)租用計(jì)算機(jī)空余的帶寬笛求，并為提供者獎(jiǎng)勵(lì)代幣，代幣可以購(gòu)買(mǎi)區(qū)塊鏈服務(wù)糕簿，也可以用于開(kāi)發(fā)探入，有點(diǎn)變向挖礦的意思。

7.4 Quantstamp

正如一家公司的財(cái)務(wù)報(bào)表需要審計(jì)一樣懂诗，智能合約蜂嗽，同樣需要審計(jì)，有了審計(jì)殃恒，這些類(lèi)似漏洞發(fā)生的概率植旧，可以被大幅度降低辱揭。

簡(jiǎn)單說(shuō)來(lái)，Quantstamp就是這樣一個(gè)區(qū)塊鏈智能合約的審計(jì)類(lèi)項(xiàng)目病附，讓智能合約變得更加安全问窃。當(dāng)然了，和像四大會(huì)計(jì)事務(wù)這樣的中心化組織不一樣完沪，咱們是去中心化的域庇。

7.5 POLYSWARM

Polyswarm 第一個(gè)去中心化的殺毒軟件市場(chǎng)

去中心化正是區(qū)塊鏈的看家本領(lǐng)，Polyswarm是世界上第一個(gè)嘗試用區(qū)塊鏈來(lái)改變這個(gè)市場(chǎng)的覆积。他們?cè)O(shè)計(jì)的系統(tǒng)里有4種角色听皿。

用戶(hù)（EndUsers）報(bào)告可能染毒的文件信息，并在平臺(tái)上懸賞宽档，得到及時(shí)而準(zhǔn)確的安全信息尉姨。

安全專(zhuān)家（Experts）通過(guò)分析病毒信息來(lái)決定這是否是一個(gè)病毒來(lái)賺取獎(jiǎng)勵(lì)。

由于智能合約形式化驗(yàn)證目前尚處于起步階段雌贱，目前項(xiàng)目大多還沒(méi)有落地啊送。展望相關(guān)行業(yè)需求，相關(guān)的投資邏輯如下欣孤。

8.1 金融領(lǐng)域細(xì)分首先落地

目前為止馋没，造成嚴(yán)重后果的漏洞大多來(lái)自錢(qián)包、ICO募資等金融領(lǐng)域應(yīng)用的合約降传，而這類(lèi)合約邏輯較為標(biāo)準(zhǔn)化篷朵，相對(duì)較容易用形式化驗(yàn)證的方式進(jìn)行查驗(yàn)。因此婆排，專(zhuān)注于金融領(lǐng)域的形式化驗(yàn)證產(chǎn)品更有潛力声旺。

8.2 函數(shù)式語(yǔ)言長(zhǎng)期來(lái)看是趨勢(shì)

許多新的公鏈項(xiàng)目，如Aeternity段只、Tezos等都采取了函數(shù)式語(yǔ)言作為智能合約的編程語(yǔ)言腮猖，目的在于方便形式化驗(yàn)證工具的開(kāi)發(fā)。因此赞枕，在選擇公鏈項(xiàng)目上澈缺，函數(shù)式語(yǔ)言是首選。