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

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

區塊鏈生態建立在信任之上。有些人稱其為“共識”，有些人稱其為“信仰”。

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

一旦漏洞被黑客所利用，所造成的不僅是數字資產的損失，更是信任的崩塌。對一個健康的去中心化社區的發展十分不利。

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

區塊鏈生態系統比我們想象的還要脆弱，智能合約安全問題不容小覷。

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

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

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

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

那么我們還能做些什么？

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

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

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

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

——在大多數的實際案例中，完全的形式化證明的實現非常困難。

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

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

區塊鏈的公鏈就是一個典型的復雜的分布式系統。

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

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

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

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

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

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

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

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

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

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

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

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

從2018年五月開始，我們開始了和NEO的合作，共同為NEO的生態系統建立形式化驗證平臺，這個項目目前已經如期啟動，并且預計會在今年陸續發布相關產品和資料。

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

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

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

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

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

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

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

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

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

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