我是顧榮輝，哥倫比亞大學(xué)計(jì)算機(jī)科學(xué)系助理教授，CertiK聯(lián)合創(chuàng)始人。很多朋友曾問我這些問題——或許在座的很多人也經(jīng)常被問起：比特幣的價(jià)值在哪里？以太坊的價(jià)值在哪里？為什么區(qū)塊鏈如此受歡迎？

我認(rèn)為，答案在一個(gè)詞中：信任。

區(qū)塊鏈生態(tài)建立在信任之上。有些人稱其為“共識(shí)”，有些人稱其為“信仰”。

然而，由于一些程序漏洞，搭建這些區(qū)塊鏈生態(tài)的代碼是脆弱且難以被完全信賴的。

一旦漏洞被黑客所利用，所造成的不僅是數(shù)字資產(chǎn)的損失，更是信任的崩塌。對(duì)一個(gè)健康的去中心化社區(qū)的發(fā)展十分不利。

在過去的幾年間，我們見到了很多黑客利用這些系統(tǒng)漏洞，價(jià)值十幾億以上美金的數(shù)字貨幣被盜。

區(qū)塊鏈生態(tài)系統(tǒng)比我們想象的還要脆弱，智能合約安全問題不容小覷。

那么，我們?cè)撛鯓颖苊膺@些程序漏洞？有沒有任何解決方案？比如說，是否可以寄希望于程序測(cè)試、白帽黑客？

很遺憾，答案或許是：不。

Edsger Dijskstra曾說過：測(cè)試可以被用來證明漏洞的存在，但并不能證明程序不存在漏洞。

白帽黑客和程序測(cè)試方法確實(shí)非常有用，并且被行業(yè)所需要。然而遺憾的是，他們由于自身的局限性，無(wú)法滿足區(qū)塊鏈所有的安全需求。

那么我們還能做些什么？

在座的你們也許已經(jīng)知道答案——形式化驗(yàn)證才是最終的解決方案。

根據(jù) NSF 2016的報(bào)告顯示，為了達(dá)到程序系統(tǒng)的絕對(duì)安全，形式化驗(yàn)證是唯一值得信賴的方法。

通過形式化驗(yàn)證，我們使用數(shù)學(xué)模型去驗(yàn)證代碼確實(shí)符合給定的規(guī)范。

你們心里或許會(huì)有這個(gè)疑問：形式化驗(yàn)證的概念已經(jīng)被提出了數(shù)十年之久。既然這么厲害，為什么這個(gè)方法還沒有被廣泛應(yīng)用？為什么如今的代碼中還是有這么多的程序漏洞？

——在大多數(shù)的實(shí)際案例中，完全的形式化證明的實(shí)現(xiàn)非常困難。

2015年，耶魯大學(xué)計(jì)算機(jī)科學(xué)系主任邵中教授和我提出了“深度規(guī)范”的概念，我們發(fā)現(xiàn)，形式化驗(yàn)證真正的瓶頸并不在“如何去證明”，而是在“如何更好地表達(dá)程序設(shè)計(jì)的意圖（或規(guī)范）”。

“深度規(guī)范”最強(qiáng)大的地方是可以證明“復(fù)雜系統(tǒng)的正確性” ，這類系統(tǒng)在之前被認(rèn)為是很難證明的。

區(qū)塊鏈的公鏈就是一個(gè)典型的復(fù)雜的分布式系統(tǒng)。

利用這套技術(shù)，我們可以把一個(gè)復(fù)雜系統(tǒng)（并發(fā)的或者分布式的）進(jìn)行分層、整合，實(shí)現(xiàn)完備的智能合約驗(yàn)證。

目前，“深度規(guī)范”的概念已經(jīng)被廣泛學(xué)習(xí)和討論。除了耶魯大學(xué)和哥倫比亞大學(xué)，還包括來自普林斯頓大學(xué)，賓夕法尼亞大學(xué)，麻省理工大學(xué)等高校的學(xué)者。已經(jīng)舉辦了三次深度規(guī)范學(xué)術(shù)研討會(huì)和兩次暑期學(xué)校。

在2016年，我們利用“深度規(guī)范”實(shí)現(xiàn)了CertiKOS——世界第一個(gè)被完全驗(yàn)證了的并發(fā)式操作系統(tǒng)內(nèi)核。這個(gè)系統(tǒng)已經(jīng)被部署到了未來機(jī)器人Landshark等對(duì)安全要求非常高的領(lǐng)域，當(dāng)時(shí)驗(yàn)收方請(qǐng)來了由谷歌工程師組成的黑客團(tuán)隊(duì)進(jìn)行評(píng)測(cè)，其報(bào)告評(píng)價(jià)CertiKOS是“無(wú)懈可擊”的。

在2017年，我們開始將這個(gè)技術(shù)運(yùn)用到區(qū)塊鏈領(lǐng)域中。軟件安全公司CertiK應(yīng)運(yùn)而生。

上圖是運(yùn)用“深度規(guī)范”保護(hù)智能合約的例子：對(duì)于非常復(fù)雜的智能合約，（比如像我們的穩(wěn)定幣客戶TrueUSD的合約）我們首先用標(biāo)簽的形式寫下合約的規(guī)范，（部分規(guī)范也可以被自動(dòng)生成）。之后，我們將將復(fù)雜的智能合約拆分為較小的可驗(yàn)證的模塊，在不同的抽象層進(jìn)行證明。最后，我們將經(jīng)過證明的模塊合并到一起，生成整個(gè)合約正確性的證書。

上圖是CertiK如何檢測(cè)到美鏈（BEC）的智能合約漏洞的例子。我們先用標(biāo)簽的方式把規(guī)范添加到智能合約中。一旦某個(gè)模塊的驗(yàn)證失敗，該模塊的程序漏洞——也就是V神所說過的“程序?qū)崿F(xiàn)與程序員意圖之間的區(qū)別”——就能被檢測(cè)出來。

同時(shí)，我們的技術(shù)也可以找到觸發(fā)程序漏洞的方法，當(dāng)所有程序漏洞被修復(fù)并通過驗(yàn)證后，CertiK即可生成智能合約“不存在漏洞”的證明。

這個(gè)“不存在漏洞”的證明，是其他比如程序測(cè)試和白帽黑客技術(shù)無(wú)法實(shí)現(xiàn)的。

我之前提到過，有些規(guī)范（或標(biāo)簽）是可以被自動(dòng)生成的。這項(xiàng)技術(shù)叫做“智能標(biāo)簽”，由CertiK團(tuán)隊(duì)獨(dú)立研發(fā)而成。

基于“智能標(biāo)簽”技術(shù)，CertiK在幾個(gè)月之前發(fā)布了安全漏洞掃描引擎CASE。

CASE可以掃描已部署在區(qū)塊鏈系統(tǒng)中的智能合約。通過智能標(biāo)簽技術(shù)生成合約規(guī)范，并對(duì)合約進(jìn)行安全驗(yàn)證。

在最近一次耗時(shí)數(shù)小時(shí)的掃描中，我們發(fā)現(xiàn)，幣值前500的智能合約中有超過50個(gè)智能合約存在安全漏洞，包括3種高危漏洞，2種中危漏洞，和11種低危漏洞，涉及到的總幣值高達(dá)四千萬(wàn)美金。

從2018年五月開始，我們開始了和NEO的合作，共同為NEO的生態(tài)系統(tǒng)建立形式化驗(yàn)證平臺(tái)，這個(gè)項(xiàng)目目前已經(jīng)如期啟動(dòng)，并且預(yù)計(jì)會(huì)在今年陸續(xù)發(fā)布相關(guān)產(chǎn)品和資料。

我們?cè)诖蠹s一年前上線了代碼安全驗(yàn)證服務(wù)。迄今，我們完成了超過160份代碼安全審計(jì)，累計(jì)大約九萬(wàn)行代碼。守護(hù)了價(jià)值超過12億美金的數(shù)字資產(chǎn)。

一年來，我們的服務(wù)已經(jīng)被區(qū)塊鏈領(lǐng)域的主流機(jī)構(gòu)所承認(rèn)和采納——CertiK是唯一同時(shí)被幣安、火幣、OKEx等全球主流交易所所認(rèn)證的安全服務(wù)商，也是全球頂級(jí)公鏈平臺(tái)如NEO、Waves、本體、ICON、Qtum、Quarkchain的安全合作伙伴。

同時(shí)，我們也為諸多業(yè)內(nèi)知名項(xiàng)目如Crypto.com，TrueUSD，Celer，IoTex等提供了安全審計(jì)、定制化安全防御、滲透測(cè)試等一站式安全解決方案。

現(xiàn)在讓我們把目光放到一個(gè)新的研究項(xiàng)目上——DeepSEA Blockchain。

我們已經(jīng)討論了如何檢測(cè)已部署合約的程序漏洞，而更加重要的問題是：我們是否可以從最開始直接開發(fā)出沒有程序漏洞的，可完全被信賴的智能合約？

為了探索這個(gè)問題的答案，我們開始了DeepSEA項(xiàng)目。

我們計(jì)劃引入DeepSEA函數(shù)式編程語(yǔ)言，并為包括IBM超級(jí)賬本、EVM等平臺(tái)提供無(wú)漏洞的DeepSEA編譯器。

——也就是說，如果源代碼是正確的，那么被編譯之后的機(jī)器碼也是正確的。

同時(shí)，我們可以從DeepSEA源代碼中將程序規(guī)范導(dǎo)入Coq證明輔助器，然后在Coq中對(duì)程序進(jìn)行手動(dòng)或者半自動(dòng)證明。

DeepSEA Blockchain項(xiàng)目致力于構(gòu)建跨平臺(tái)的，可信賴的智能合約框架，由CertiK，哥倫比亞大學(xué)和耶魯大學(xué)共同合作推進(jìn)。我們已經(jīng)獲得了來自IBM、以太坊基金會(huì)和Qtum基金會(huì)的科研獎(jiǎng)金，也誠(chéng)摯地希望可以得到更多社區(qū)的支持，幫助我們將該框架理念發(fā)展到下一個(gè)階段。