隨著平臺(tái)級(jí)應(yīng)用的普遍化，智能合約涉及的金額呈指數(shù)級(jí)別增長(zhǎng)，智能合約的安全問題也成為投資者和開發(fā)者共同關(guān)注的焦點(diǎn)。今年以來有數(shù)個(gè)基于ERC-20的ICO項(xiàng)目因?yàn)橹悄芎霞s代碼出現(xiàn)漏洞而遭到黑客攻擊，導(dǎo)致投資者巨額的損失。為了防止類似事件的發(fā)生，交易所、錢包、項(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ā)布）

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

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

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

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

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

智能合約語言設(shè)計(jì)中，許多公鏈平臺(tái)開始采用Haskell或OCaml一類的函數(shù)式語言，因?yàn)楹瘮?shù)式語言更為便于編寫形式化驗(yàn)證方面的開發(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àn)證主要應(yīng)用在軍工、航天等對(duì)系統(tǒng)安全非常高的領(lǐng)域，在消費(fèi)級(jí)軟件領(lǐng)域幾乎沒有應(yīng)用。由于傳統(tǒng)互聯(lián)網(wǎng)應(yīng)用與區(qū)塊鏈應(yīng)用的運(yùn)行環(huán)境有著本質(zhì)的不同，其開發(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ù)器+客戶端的模型，如果應(yīng)用出現(xiàn)安全隱患只需要對(duì)服務(wù)器端代碼進(jìn)行修改就可以輕松排雷，并且服務(wù)器端可以對(duì)用戶數(shù)據(jù)進(jìn)行回滾以挽回用戶損失。因此，傳統(tǒng)互聯(lián)網(wǎng)應(yīng)用開發(fā)的過程較為注重快速迭代，以犧牲安全性換取效率和功能上的快速升級(jí)。

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

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

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

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

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

Imandra????語言????OCaml子語言，專注于金融交易系統(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 使用自己開發(fā)的K框架對(duì)虛擬機(jī)二進(jìn)制碼進(jìn)行形式化驗(yàn)證 ????UIUC

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

3.1 Vaas平臺(tái)

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

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

3.2語言

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

其中，Imandra發(fā)布了一套開源的以太坊虛擬機(jī)用ImandraML語言標(biāo)記的模型，并且專注于交易所等金融應(yīng)用場(chǎng)景的形式化驗(yàn)證，用以確保金融交易的合法合規(guī)，據(jù)稱相關(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)化帶來幫助在技術(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ì)核心成員來自哥倫比亞大學(xué)、耶魯大學(xué)和普林斯頓大學(xué)，專業(yè)背景都是計(jì)算機(jī)技術(shù)，團(tuán)隊(duì)技術(shù)實(shí)力強(qiáng)硬20多名來自海外知名高校和實(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ì)基于以太坊上開發(fā)的DAPP和系統(tǒng)進(jìn)行形式化驗(yàn)證對(duì)智能合約進(jìn)行形式化驗(yàn)證，支持以太坊和EOS致力于飛機(jī)，航天器和區(qū)塊鏈領(lǐng)域的軟件系統(tǒng)的安全性，可靠性和正確性

主要技術(shù)開發(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)過certik驗(yàn)證的智能合同、DApp以及區(qū)塊鏈將會(huì)被附上證書形式的標(biāo)志，來展示其正確性和安全性。Certik平臺(tái)提供的主要功能包括以下部分。

智能標(biāo)簽框架

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

基于層的分解

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

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

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

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

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

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

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

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

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

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

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

分解完小模塊后，系統(tǒng)由兩種方式進(jìn)行驗(yàn)證，簡(jiǎn)單的證明任務(wù)可以由一些自動(dòng)驗(yàn)證器(例如SMT解算器)解決。除了平臺(tái)內(nèi)部自帶的驗(yàn)證器（證明引擎），CertiK平臺(tá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)證通過后，會(huì)被貼上證書的標(biāo)簽，賞金獵人和檢查官分別獲得CTK獎(jiǎng)勵(lì)。

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

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

以下是certik的操作界面

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

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

5.2鏈安科技

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

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

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

????第三個(gè)，合約開發(fā)

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

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

int8 c=a+b

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

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

Int8.repr: Z -> int8

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

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

設(shè)置代碼執(zhí)行的前提條件，保證a和b的類型是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))描述，是為了證明代碼的功能正確性是否滿足，即需要證明源代碼是對(duì)a和b進(jìn)行求和而不是求差或任何其他運(yùn)算邏輯，并且將運(yùn)算結(jié)果轉(zhuǎn)換為int8類型。此外，需要對(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í)行是否滿足上述后置條件。如果產(chǎn)生一個(gè)不可證明結(jié)果，說明程序功能不正確，或者存在溢出安全漏洞。然后根據(jù)證明結(jié)果，對(duì)源程序進(jìn)行分析修改，然后再重新證明，直到證明通過為止。鏈安采用這種數(shù)學(xué)的證明方式將代碼形式化描述為公式，并對(duì)其進(jìn)行邏輯漏洞和安全漏洞證明，基于此原理，實(shí)現(xiàn)了自動(dòng)化的驗(yàn)證工具，能夠方便、快速地驗(yàn)證出代碼的功能正確性和安全屬性。

5.3 runtime verification

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

Runtime驗(yàn)證技術(shù)依賴于程序執(zhí)行不應(yīng)違反某些屬性的原理。其中一些屬性，如并發(fā)程序中缺少數(shù)據(jù)競(jìng)爭(zhēng)，具有通用性，可以自動(dòng)檢查。其他屬性，如專用庫(kù)的規(guī)格，是針對(duì)特定應(yīng)用程序或用途定制的。Runtime驗(yàn)證技術(shù)可以自動(dòng)檢查通用屬性，不需要開發(fā)輸入，并且可以檢查開發(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)過多輪討論和修改，才能確保它能正確捕捉合同的預(yù)期行為。

（3）提煉

通過多個(gè)步驟將形式化后的規(guī)則完善到虛擬機(jī)級(jí)別，以捕獲虛擬機(jī)特定的細(xì)節(jié)。最終的虛擬機(jī)級(jí)別規(guī)則的作用是確保在字節(jié)碼級(jí)別沒有意外發(fā)生，也就是說，只有在執(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)證，通過這樣的方式不用依賴編譯器的正確性。同時(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萬的以太被轉(zhuǎn)出，在當(dāng)時(shí)價(jià)值相當(dāng)于七千萬美元，今天則達(dá)到了21億美元。黑客達(dá)成了他想要的破壞，退出了攻擊。

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

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

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

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

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

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

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

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

換句話說，TheDAO的發(fā)行與首次公開發(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上線，黑客利用漏洞累積向火幣轉(zhuǎn)入了超過20億枚EDU。這也導(dǎo)致了EDU的價(jià)格崩盤。

7.1

Sentinel Protocol

韓國(guó)團(tuán)隊(duì)，基于ICON的第二個(gè)項(xiàng)目。項(xiàng)目目的是要?jiǎng)?chuàng)建一個(gè)去中心化的聲譽(yù)系統(tǒng)，通過集體智能和人工智能相結(jié)合，將所有數(shù)字貨幣的粘片，黑客信息，可疑錢包地址等各種信息記錄在區(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ù)專利，并與很多互聯(lián)網(wǎng)大公司是合作伙伴）給設(shè)備加密，確保數(shù)據(jù)隱私并阻止它被黑客利用來連接到別的物聯(lián)網(wǎng)設(shè)備。同時(shí)Atonomi的Token也像IOTA一樣支持設(shè)備之間的微支付需要。

7.3 Gladius

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

Gladius是利用存儲(chǔ)和流量的經(jīng)濟(jì)激勵(lì)，來創(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的桌面客戶端允許用戶租用計(jì)算機(jī)空余的帶寬，并為提供者獎(jiǎng)勵(lì)代幣，代幣可以購(gòu)買區(qū)塊鏈服務(wù)，也可以用于開發(fā)，有點(diǎn)變向挖礦的意思。

7.4 Quantstamp

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

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

7.5 POLYSWARM

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

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

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

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

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

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

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

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

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