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

我認為，答案在一個詞中：信任。

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

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

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

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

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

那么，我們該怎樣避免這些程序漏洞？有沒有任何解決方案？比如說，是否可以寄希望于程序測試、白帽黑客？

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

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

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

那么我們還能做些什么？

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

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

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

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

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

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

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

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

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

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

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

在2017年，我們開始將這個技術運用到區(qū)塊鏈領域中。軟件安全公司CertiK應運而生。

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

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

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

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

我之前提到過，有些規(guī)范（或標簽）是可以被自動生成的。這項技術叫做“智能標簽”，由CertiK團隊獨立研發(fā)而成。

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

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

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

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

我們在大約一年前上線了代碼安全驗證服務。迄今，我們完成了超過160份代碼安全審計，累計大約九萬行代碼。守護了價值超過12億美金的數(shù)字資產(chǎn)。

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

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

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

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

為了探索這個問題的答案，我們開始了DeepSEA項目。

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

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

同時，我們可以從DeepSEA源代碼中將程序規(guī)范導入Coq證明輔助器，然后在Coq中對程序進行手動或者半自動證明。

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