對話哥倫比亞大學教授——帶你深入了解形式化驗證技術

在智能合約框架下，事先檢查合約本身是否存在機制漏洞，是解決其安全問題的關鍵。

而形式化驗證（Formal Verification）正是用數學方法驗證程序的正確性，為智能合約和區塊鏈應用提供安全服務的技術。

9月2日晚8點，Unitimes成功舉辦第二期區塊鏈技術與應用AMA活動。我們有幸邀請到了CertiK聯合創始人、哥倫比亞大學教授顧榮輝為大家帶來了主題為“帶你深入了解形式化驗證技術”的分享。

本次AMA分為兩個環節：

• 固定問答環節

• 自由問答環節

固定問答——

顧教授從形式化驗證的概念說起，圖文并茂地介紹了CertiK是如何使用這項技術來為智能合約和區塊鏈應用保駕護航的。此外，他談到了CertiK團隊的情況及其社區建設的計劃。最后，顧教授還對形式化驗證技術的學習和研究者提出了寄語。

以下為具體內容：

顧：大家好，我是顧榮輝，現在是哥倫比亞大學CS助理教授。2011年本科畢業于清華大學，2016年博士畢業于耶魯大學。致力于軟件系統形式化驗證的研究，聯合創建了CertiK項目，致力于通過深度規范技術，構建可靠安全的區塊鏈生態。

CertiK的另一位聯合創始人邵中教授，是耶魯大學計算機系系主任、終身冠名教授，是形式化驗證領域的世界級專家。2016年，我和邵中教授一起設計并開發了首個經過完全驗證的并發操作系統內核CertiKOS。

CertiK有16位工程師，大多是之前Google、Facebook的資深工程師。我們目前有三位科研人員，我和邵教授在耶魯與哥大的實驗室也會為CertiK持續提供科研成果，光邵教授的實驗室就有20位左右的博士生、博士后以及訪問學者。

顧：簡而言之，“形式化驗證”就是通過數學的方法證明程序是“正確的”。這里的正確性，指的是，程序的實現，與程序員的設計或意圖（我們稱作規范）是相符的。

V神說過，所有程序的bug，都是由“程序的實現，與程序員的意圖之間有區別”導致的。形式化驗證，就是希望通過數學方法，證明沒有這種“區別”。

我這里舉一個例子：

假設左邊的是程序員的意圖，實現一個算(x+1)的平方。右邊是一段程序，完成了指定的計算。普通的安全測試，就是找幾個輸入，看看輸出是不是相符。例如：

比如x = 0, x= 1。

如果不相符，立刻就可以找到bug。可是即使所有測試都滿足，也未必說明是正確的。例如，下面這個錯誤的程序也滿足所有測試。

形式化驗證，是試圖證明，在所有情況下，兩者都相符，證明的過程如下：

先用數學上的“結合律”，然后提取公因式，然后交換律，再提取公因數，最后根據平方的定義，可證。

形式化驗證，看起來很cool，但是實際非常困難。之前大家普遍認為“一個像并發式操作系統內核那樣復雜的系統，是很難甚至無法完全形式化驗證的”。

2016年，在OSDI16（頂級計算機會議）上，我和邵中教授一起展示了CertiKOS，第一次讓大家確認并發式操作系統內核是可以被完全形式化證明的。

顧：首先，操作系統內核，可以被看做當前計算機系統的基礎，它的地位相當于區塊鏈世界的公鏈（或者虛擬機）。安全性的保證至關重要，傳統的安全測試無法滿足要求。

可是，對于多核的、并發的操作系統內核，因為太過復雜，之前一直無法通過數學的方法被完全證明。像我剛才所說，很多科學家認為“一個像并發式操作系統內核那樣復雜的系統，是很難甚至無法完全形式化驗證的”。

2015年我和邵中教授一起提出了“深度規范”的概念，大概的想法是“形式化驗證”的瓶頸，不是在“如何證明”，而是在“如何寫出好的意圖（或規范）”。

利用這套技術，我們可以把一個復雜系統（并發的，或者分布式的）進行解構、分層，從而更加自動化的進行證明。

我們利用深度規范，實現了CertiKOS，最后被部署到了一個未來機器人上。當時驗收方請來了由谷歌工程師組成的黑客團隊進行評測，給出的報告對CertiKOS的描述是“無懈可擊”。

顧：CertiK的目標是構建完全可信的區塊鏈生態，我們正在做的事情有如下幾件：

1）最簡單的，我們可以幫助項目方，驗證智能合約，保證安全性。

2）其次，我們正在開發一套新的智能合約語言，DeepSea。在9月8日香港舉行ETHIS上，我們的首席科學家Vilhelm Sj?berg會第一次展示這個語言。DeepSea可以幫助開發者開發更加安全高效的智能合約，并且通過我們設計的被完全驗證過的編譯器，被編譯成bytecode的過程，也是正確的。

3）我們可以與公鏈合作，保證公鏈生態的健康發展。比如我們和NEO、星云鏈、量子鏈、本體、ICON、Waves等的合作。以星云鏈為例子，他們開發了一套基于Javascript的智能合約語言，我們幫他們也實現了一個形式化驗證框架。

4）與交易所的合作。大家可能知道，我們是幣安孵化的。同時已經與各大交易所進行了安全合作，比如火幣、OKEx、Fcoin、Gate、KuCoin、幣信等。

顧：絕大部分的智能合約都可以被安全驗證，因為相對而言，它的執行模型比較簡單。CertiK曾經率先發現了很多智能合約的問題。

上面這個圖，是利用CertiK的引擎檢測出EduCoin的Bug。之前我們還發布了關于美鏈等的Bug檢測的消息。

昨天，我們發布了CertiK的第一代自動驗證引擎（CASE），可以自動掃描并定位智能合約里的漏洞。

顧：自動引擎CASE，會首先根據智能合約的類型、代碼、注釋等信息，自動生成標簽“label”，這個過程，我們叫做“smart labeling”。然后CertiK會將這套標簽轉化成“規范（specification）”。

CertiK會利用形式化驗證技術，試圖證明規范與實現之間是相符的。任何不符之處，都會以bug的形式，爆出。這套系統化是完全自動化的，可以為企業級客戶進行24小時不間斷的掃描，從而提前發出安全預警。

但是自動掃描的安全保證，是要弱于有人工干預的形式化驗證的。在目前CertiK的半自動驗證服務中，我們會請專家為智能合約“手寫”規范，這個規范更加詳細，更加全面，更加可靠。剩下的所有工作仍然是全自動的。

當然在找到問題后，我們的專家也會與客戶溝通，幫助他們修復漏洞。

顧：這個問題很好。剛才我提到的，大概的想法是“形式化驗證”的瓶頸，不是在“如何證明”，而是在“如何寫出好的意圖（或規范）”。

基于這個研究，2015年我和邵中教授一起提出了“深度規范”的概念。目前這個概念已經被廣泛學習、討論。目前DeepSpec社區，除了耶魯大學和哥大。還包括普林斯頓、賓大、MIT等。

已經舉辦了三次workshop，兩次暑期學校。上次暑期學校，V神也有邀請來講課，大家討論了深度規范與以太坊結合的可能性。

深度規范最強大的地方，是可以幫我們證明“復雜系統的正確性”，尤其是“并發式的或者分布式的”。這類系統之前被認為是很難證明的。比如區塊鏈的公鏈，就是一個典型的復雜，分布式系統。

2016年，在OSDI16（頂級計算機會議）上，我和邵中教授一起展示了用深度規范（DeepSpec）構建的CertiKOS，第一次讓大家確認并發式操作系統內核是可以被完全形式化證明的。兩年過去了，我們的科研團隊仍然是唯一擁有這項技術的。

我們認為，區塊鏈系統，比如EVM，是至少與并發式操作系統內核同等復雜，甚至是更加復雜的。所以，相比較于其他團隊（包括其他頂級科研單位比如MIT、普林斯頓等），CertiK可能是距離這個目標最近的。

顧：我們競爭對手有如下幾類：

1) 傳統的安全公司，這類公司對區塊鏈安全有一定的保障能力，尤其是超級節點等（傳統安全擅長的范疇）。可是無法滿足區塊鏈時代新的要求。

2) 其他提供形式化驗證服務的公司。根據我剛才的描述，其實大家可以看出來，形式化驗證的局限性很大，目前可以證明并發式或者分布式復雜系統的團隊，只有CertiK，這個在學術界都是比較公認的。所以其他競爭公司，對我們的影響比較小。

顧：我這里簡要介紹一下，首先我們之前已經建設了深度規范社區，已經初具規模，并且都是由各大國際名校的博士生構成的，這個也是CertiK開發社區的主要貢獻者。

其次，我們在與各大公鏈、交易所、礦池進行合作。我們的合作機構有交易所（幣安Labs、OK、KuCoin、Gate等），加密貨幣基金（FBG、節點、Kenetic、NGC、SigNum等），傳統VC（光速中國、經緯中國、丹華等），礦主（比特大陸、嘉楠耘智旗下基金等），以及各大公鏈平臺（NEO、星云鏈、量子鏈、本體、ICON、Waves等）。這也是我們構建社區的重要一環。

顧：區塊鏈世界堅信“Code is Law”以及“In math, we trust”，但是代碼本身，是會有bug的，很多時候是“不可信”的。希望大家可以擁抱形式化驗證，擁抱深度規范技術，真正地去構建“可信代碼”。

自由問答——

固定問答環節結束后，參與此次AMA的成員可以自由提問。以下為Unitimes從群成員的提問中精選的幾個問答：

顧：DeepSea首先會幫開發者避免犯一些低級錯誤。但是功能正確性，還是需要進行單獨的驗證。不過DeepSea開發的智能合約，CertiK可以更加簡單快速的驗證。

顧：這個問題很好。傳統軟件項目，相對而言都比較復雜，形式化驗證難度很高，很多對安全的要求卻沒那么高，大家可以注意到CertiKOS是2016年才開發出來的技術，是很新的技術。在傳統軟件領域，我們已經開始與無人車進行合作。

顧：很好的問題。目前形式化驗證，包括深度規范，主要的目的是“證明代碼沒有bug”，在這個過程中，可以順帶找到系統的漏洞。它的目標與傳統安全領域的“找bug”不同。但是我們確實沒辦法自動修復bug，只能提供觸發漏洞的方式，以及代碼定位，幫助開發者修復bug。

顧：我們首先需要知道（或者定義）這個函數的前置條件，比如x的范圍等。然后定義函數的后置條件，比如y與x的關系以及y應該滿足的性質（比如永遠不可能為0等）。最后證明在前置條件符合的情況下，后置條件滿足。

顧：1) 是的，對于不同的需求需要有不同的規范描述。我們有一套智能寫規范的系統，目前可以用于像智能合約這種簡單的程序。對于復雜系統，還是需要專家來書寫規范。當有了規范，引擎是用來證明代碼滿足規范的。2) 會的，我們會推出第三方庫。目前應該是會先推出DeepSea的第三方驗證庫。

顧：這個問題很好，現在的安全驗證成本確實更高。CertiK的引擎是完全自動化的，這已經減少了很多人力成本。目前CertiK絕大部分的人力成本，是手工書寫“規范”。這也是為什么我們一直在致力于自動化的輔助添加標簽，再把標簽轉化為規范的技術。希望可以大大減少人力成本。

顧：我覺得潛在的安全危險，還是在“公鏈的安全”上。現在大部分的公司都是在關注“智能合約的安全”，說實話，是因為簡單，門檻低。但是公鏈局限性或者是安全性，是更大的挑戰。

顧：CertiK的很多產品都會陸續開源。比如我們的深度規范技術系列，不僅很多都開源了，我們還開了課程（在耶魯），甚至是公開課（暑期學校）。DeepSea也會馬上開源。我們智能合約的驗證引擎，會在適當的時候開源。

顧：一是公鏈提供的編程語言，Solidity確實還是有很多不足。很多公鏈都在嘗試。但是需要注意的一點是編譯器，這些高級語言的編譯器是否是安全的呢？這也是我們再大力推廣的。

二公鏈的實現本身。很多公鏈確實很復雜，雖然經過了很多測試，但也很難保證完全的正確性。這點需要進一步的驗證。很多公鏈上的實現，比如plasma，設計上是跨越了多層抽象層，相對較為復雜。這塊的安全驗證需要重視。最后是局限性，比如如何更好的實現“隨機數”。

顧：好問題，函數式語言的優勢在于，不容易犯低級錯誤，以及更加容易被安全驗證。DeepSea也是函數式語言，所以我們也可以為這些公鏈提供服務。