TMT观察网_独特视角观察TMT行业

尋找軟件世界的圣杯

對很多沒聽說過「形式化驗證」的人，你可能暫時沒辦法理解它背后一些很美的東西。

沒關系，今天我想用一個故事向你們介紹這種美。如果你覺得有意思的話，可能也會順帶理解區塊鏈美的地方在哪。

 1 

對我來說，形式化驗證是在追尋計算機領域里的圣杯。它要解決的問題，是怎么保證軟件里沒有 bug 。你肯定會很驚訝，軟件有 bug 這件事幾乎是一定的。只要涉及到復雜代碼，就很難避免出錯。

怎么保證它沒有 bug 呢？

從計算機出現開始就有很多人在研究這個問題，但一直沒人能給出答案。所以，它是一個圣杯。就像一本誰都沒看過的武林秘籍。

我大概是 05 年開始搞這個東西的。形式化驗證是一個非常小眾的研究方向。當時我在安徽的中國科學技術大學里，我們實驗室想招研究生，非常難招。因為同學們都跑去研究人工智能了。而形式化驗證他們很多人壓根就沒聽說過。

但最近兩年，這個非常冷門的研究方向突然火了。主要還是因為區塊鏈橫空出世，吸引了很多人進來研究。就像密碼學跟著區塊鏈火起來一樣。以太坊創始人 V 神一定程度上也助推了「形式化驗證」的發展。

那么，到底什么是形式化驗證？

我們都知道，代碼和程序是邏輯性很強的東西。既然邏輯性很強，那我們當然也可以用邏輯來推理它，論證這個軟件到底安不安全、有沒有 bug。只不過平常我們所理解的“推理”，可能都是在自己的大腦里進行的。像柯南破案那樣，一步步地推演。但現在我們需要把這個推理的過程，用更嚴謹、更標準的數學和數理邏輯的方式表達出來，讓計算機能夠看懂——這個東西就叫形式化驗證。

 2 

為什么形式化驗證會非常小眾？

除了因為本身在尋找圣杯外，還有一個原因是它對技術門檻的要求比較高。

如果你想研究形式化驗證，首先需要先弄懂這套邏輯系統的“語言”。人們平常溝通的時候，講話用的是自然語言和文字，很直接，很簡單，彼此也很容易聽懂。但邏輯語言全部都是符號。你必須先弄懂符號是什么意思。然后，你還要理解怎么把你平常說的話，用這些符號表達出來。這個東西是最花時間的。

一般一個 PHD 剛入門，需要先花上很長的時間，不斷看東西，培養這種用符號表達的感覺。像小時候剛開始學造句一樣。等你會造句了，最后一步才是開始寫作文。也就是把整個推理的邏輯論證出來。“推理”本身又會涉及到很多理論深度的東西。所以總結起來，它對門檻的要求確實比較高。

我研究這個東西十幾年了。我是 01 年在科大讀研，05 開始研究，07 年 PHD 畢業，然后留在科大當老師。讀研的時候，最開始一段時期做的是網絡研究，后來才做的形式化驗證。做了之后我發現，形式化驗證里面有很多特別美的東西。它背后有很多特別美的數學理論。但很少有人能觸及到這種美。因為你在觸及到這種美之前，需要花費非常多的時間來琢磨。

這點感覺跟區塊鏈挺像的。區塊鏈初看很簡單，但是你深入研究，反復去做、去試驗，花上一些時間，你才能慢慢領略到區塊鏈背后美妙的地方在哪。

 3 

當時研究形式化驗證，我最大的苦惱是一直沒能找到合適的應用場景。

我們嘗試過很多方向的應用，大多數是操作系統內核的驗證，包括很多實時性的內核，比如工業控制、醫療設備、專用芯片這些東西。

我們還嘗試過存儲芯片方面的應用。閃存芯片上有一層很薄的軟件，這層軟件非常關鍵，不能有 bug，因為它要用來確保存儲和讀取時候不會出錯。你平常用 u 盤如果沒有在操作系統里退出直接硬拔出來，它就有可能會觸及到這層軟件的 bug，導致數據丟失。

我們希望把形式化驗證那套東西拿過來用，確保這些軟件代碼里沒有 bug。這些應用場景的代碼量比較短又足夠復雜，所以適合拿來做驗證。

只有代碼足夠復雜才值得做形式化驗證，如果代碼太簡單就不需要了，你讓程序員肉眼看一下就能判斷有沒有 bug 了。

但即使是這樣，我們仍然覺得形式化驗證在工業應用上的性價比很低。因為工程的變化速度太快了，理論距離實際使用，其實還是有不少的差距。

 4 

這個讓人苦惱的現象一直持續到 16 年。那時我開始研究區塊鏈的底層技術。

我看了比特幣和以太坊。當以太坊出現后，智能合約冒出水面。我很敏銳地察覺到，這里面其實有一些很適合我們的新機會。智能合約是形式化驗證非常理想的一個應用場景。

我馬上就和一位朋友商量，要不要一起出來干這件事：用形式化驗證的方式搞區塊鏈安全。那個朋友之前在 360 工作，他跟我說，要干，不干你將來一定后悔。他本身也有連續創業的經驗，所以我當時就決定：出來創業。

于是今年 4 月份，我們拿了一點錢，就組建了一個團隊開始搞。這個團隊也是以我之前在中科大的幾個學弟為主，還有一些早期就對區塊鏈非常感興趣的 90 后的小朋友。

 5 

現在很多形式化驗證慣用的方法是：弄一個黑盒，然后丟一段代碼進去，黑盒再吐出來一個結果：yes or no。

如果是 yes，那就說明丟進去的這段代碼沒有問題。如果是 no ，就說明代碼里有 bug。但這種方式的問題在于，這個盒子本身是個黑盒。你沒辦法證明黑盒的正確性。所以這種方式更多還是用來找 bug。

比如芯片上的形式化驗證就是用“黑盒模式”找漏洞。你把芯片設計圖丟進黑盒里，它盡可能去遍歷所有的狀態，然后找出一個反例，告訴你這里有 bug，在某種情況下可能會出現什么問題等等——但如果找不出來 bug 呢？是代碼本身沒有 bug 嗎？還是黑盒的能力不夠，找不出 bug？

所以這一類形式化驗證，你需要依賴于黑盒本身的正確性。當然你可以把這個黑盒開源，讓全世界的人幫你檢查看有沒有錯誤。但很少人有人能這么做。因為這塊技術目前還沒有做到那么好。

 6 

我們從 05 年開始研究時，采用的是另一種最古老、最傳統、也是最笨的辦法。但這種方式有一個好處是，當它回答 yes 的時候，它會給出一個證據。這個證據是一個數學證明。就像你小時候在黑板上證數學題那樣，把證明過程寫出來就沒辦法造假。老師和同學都可以看到。所有人都可以檢查。

理論上這套方法是可以這樣做的，但實際上我們還做不到自動化。你肯定希望最理想的情況是直接把代碼扔進盒子里，然后就能自動吐出來一個證明。但現在還做不到。這是理論的天花板。

我們現在是半自動化來做這件事。你想象下這個盒子上有一些輔助的把手，當你發現盒子轉不動的時候，就需要人工手動去搖一搖，丟進一段代碼，吐出來一段證明。這是一個通過人操控的盒子。

其實這個盒子是非常復雜的，上面有很多的把手，需要大量做研究的人不停地搖，而且需要搖上好幾年。我們當時跟很多國內的團隊聊，他們稱我們是原教旨主義。因為像我們這樣干的人很少。這種傳統的做法沒法工業化應用。懂得怎么搖盒子把手的人其實很少很少。但我當時就很堅信，這個看似傳統的方法才是未來。

這里面很多人誤解了，覺得由人去搖把手很累，但這其實是人類體現自我價值的意義。就像證明“哥德巴赫猜想”是人應該要做的事情，不可能讓機器來做。人存在的意義就是在盒子卡住的關鍵時候去推動一下。

從一開始我就很接受這種哲學觀。它就應該這么做。但另一方面，你搖上那么幾年這個問題怎么解決？當時我認為，人搖的時間一定是越來越快的。把手會越來越少，盒子會越來越簡單。

事實也的確如此。經過十幾年的發展，這個方法反而被越來越多的人接納。因為這個東西跟其他計算機技術的發展是一樣的。人們寫軟件是用一層一層的 stack ，“堆棧”，不斷壘起來。這種傳統的證明方式之所以低效，是因為它沒有軟件棧，用的全部是最底層的技術，類似 if、else、and、or 這種非常底層的證明語言，那當然會很累。

但如果你有對應的軟件堆棧，有相應的框架和工具，你在很高的抽象層上去做證明，那就不會很累了。你不能因為現在還沒有這種技術棧，就說這條方向沒有前途。這是我從一開始就非常相信的。事實也驗證了是正確的。現在很多人都在往這個方向走。

 7 

為什么智能合約出現后我會非常激動呢？

因為智能合約的代碼量也是比較短的，但它對安全性的要求更高。智能合約一旦部署到區塊鏈上就不能再修改，所以它一定不能出錯。這些基本的特性就決定了它對形式化驗證是有需求的。

再加上區塊鏈的設計哲學是去中心化的，所以想要保證「智能合約的代碼里沒有 bug」 ，這件事必須用一種去中心化的方式去證明。

也就是說，智能合約發布到網上，如果它能自帶一個證明，就是最好的。

我們研究的那套形式化驗證的方法，移植到智能合約上就是要去琢磨，怎么做出一些自帶數學證明的智能合約模版。

這種自帶證明的方式，跟「一個中心化的黑盒直接吐出 yes or no 的結果」相比，它跟區塊鏈的思想是一致的。通過某一個機構為智能合約做安全審計也不是未來。因為它仍然依賴于機構的中心化的權威，無法確保智能合約可信。

而從另一方面來說，這種去中心化的方式效率上會更高。因為生成證明是非常難的，需要大量人類的智慧，但檢驗證明是很簡單的。機器非常容易做。檢驗的難度，跟代碼的行數成正比。哪怕要驗證的代碼有一億行，用機器來做檢查仍然會非常快，因為可以并行做。

所以我非常堅信，智能合約是我們這種傳統的形式化驗證方法一個絕佳應用場景。它去中心化的精神也和區塊鏈很像。

8

在我的腦海里，未來所有的智能合約發布到網上都必須帶一個自己的數學證明，

這個證明用來：

證明你干了什么事

證明你的管理員權限

證明你的合約對參與各方都是公平的

證明你沒有后門、你的分紅、鎖倉機制到底是什么樣的

……

這是讓智能合約更可信必須要做的事情。

帶了這個數學證明，對于用戶來說，哪怕你看不懂證明過程到底是怎么樣的，你也可以隨時就用另外的工具去檢查這個證明是否正確。

這套檢查的工具可以由其他不同的人提供，所有人都可以來做這樣的工具。這樣就給了用戶一個選擇，讓發布智能合約的人，和負責審計的人，都沒辦法作弊。

9

很多人聽到這里肯定會有一個疑問：這樣是不是就解決了我們一開始提到的“圣杯”問題？

其實遠遠不是。

為一個程序帶上一個證明，這個證明寫了數學推理的過程，用來論證程序自身沒有 bug——但我們都知道，數學推理需要有一些公理作為前提，然后才能往后進行推導。

如果這個前提本身是錯誤的，推理是不是也就不成立了？

舉個例子：密碼學里的加密問題。

橢圓曲線簽名算法里有一個假設叫離散對數難題。加密算法的安全性依賴于這么一件事：解離散域上的對數是非常非常難的，它的解空間非常大，最后解出來的概率，會遠小于一個非常非常小的數。就像在大海里撈針。但如果量子計算機造出來，這個問題就不存在了。所以，「基于這個假設去證明這套密碼學是安全的」這件事本身也不可靠了。

在程序里面也是一樣的。

比如我想證明 EVM （以太坊虛擬機）里面的一段代碼跑出來的返回結果是“1”，那么我需要先把程序的語義表達出來，而這就是代碼級的形式化驗證會遇到的一個問題：很多編程語言的手冊很不完善，因此程序的語義翻譯很難做到 100% 精準。

一套編程語言的設計，語義往往會存在模糊的地方。因此，形式化語義的時候就會遇到一個巨大的鴻溝。

EVM 的設計水平已經算是比較高的了，以太坊黃皮書對語義的描述寫得很清楚，所以它可能是有 99.99%的準確度，但也不是 100%。最終翻譯到形式化驗證里，理論上還是有可能存在問題。如果有問題，推理的過程和實際在 EVM 上跑的過程，二者就不一致了。這樣推理過程本身就不可靠，所有的證明就沒有意義了。這個偏差是一定存在的。

形式化驗證還有一個嚴重的依賴，是推理的邏輯本身。換句話說，就是推理的邏輯本身有沒有問題。這點也是有可能會受到質疑的。

邏輯學至今已經發展了好幾百年，有本神書叫 GEB ——《哥德爾、艾舍爾、巴赫》，里面也談到了這個問題。哥德爾是個超級聰明的人，他在 1931 年提出一個定理叫“哥德爾第二不完備性定理”。這個定理在說一個什么事情呢？給定一個邏輯推理系統，你需要證明這個系統自洽不自洽。

所謂的“自洽”是指在這個邏輯系統里沒有前提的情況下無法推出 False。用人話來說，你的邏輯不能前后矛盾。所謂的自洽系統，就是你永遠不可能說出自相矛盾的話。但“自洽”是需要證明出來的。一旦你要證明這個邏輯系統是自洽的，你就必須用一個更復雜的邏輯系統來證明。這個更復雜的邏輯系統又需要一個超級復雜的邏輯系統來證明它的自洽。

哥德爾第二不完備性定理明確提出：不可能有一個系統能證明自己自洽。它甚至很明確的找到反例說，如果你找到了一個系統能證明自己的系統邏輯自洽，那么你的邏輯就不自洽。GEB 這本神書就在談論這個問題背后的整套哲學系統，整本書大概七百多頁，非常長，也很深，到現在我也才看了三分之一。

我們在形式化驗證里用來推理程序所用的邏輯，它有沒有問題呢？其實它也是個黑盒。但這個黑盒跟我上面說的那個黑盒不太一樣。它相對比較穩定，不怎么變化。但它背后依賴的數學理論，“自洽性”也還沒有人證明過。只是有幾個數學家說，這里面大概是沒有問題的。

其實在邏輯學上，有很多公理是互相矛盾的。

嚴格來說，必須真的有人證出來兩個公理是不矛盾的、可以一起用，我們才可以去使用這些公理。但這些東西太復雜了，很多至今都沒有人能搞懂。

有人說，數學證明是特別純粹的。證出來是對就是對，是錯就是錯。其實是因為他可能不太理解這套東西。搞邏輯學的人都知道，很多公理單獨使用可能沒有問題，但你再加入一個公理，這個系統還能否自洽就是未知的了。因此，很多數學家會憑著自己的直覺加進去，覺得沒問題，但具體有沒有證明過呢？需要另一套更復雜的邏輯。

這里面是有很多開放性的問題。有很多不同的選擇。我們在做的時候，傾向于不去輕易引入一些甚至很有名的公理。能不用就不用。比如反證法，反正法會跟很多公理發生矛盾，如果用了，說不定哪天就出問題了。

10

所以，我們可能永遠都找不到圣杯。

歸根到底，我們總要依賴于一點點其他的東西。你總需要一個小小的支點。而所依賴的這個支點，需要做到盡量可靠。但你永遠做不到 100% 可靠。

當然，我覺得這個支點已經是人類文明的精華了。因此還是比較可靠的。

這里面還有很多非常有意思的故事。這也是為什么我會說它們背后有很多很美的東西。只是了解的人不多而已。

11

那么，形式化驗證跟大家更熟悉的密碼學，他們之間有關系嗎？

有關系。

我個人覺得，密碼學這套歷史有一條線，可以把它分隔成兩半。在這條線之后，密碼學所有東西你要證明可靠；而在之前，你往往不需要證明，全靠經驗。

如果你現在隨便去買一本密碼學的書，大概率翻開，第一章會講“對稱加密”、第二章講“非對稱加密”、第三章講“哈希、隨機數”。這些東西都是沒有證明的，只是教你怎么用而已。所以到頭來，你可能只是背了一堆的算法。這叫前密碼學。

但現在不一樣了。現在如果你自己想提出一個密碼學的東西，你必須先證明它的安全性。所以從某個時候開始，這在學術上稱作 Provable Security，“可證安全性”。如果現在新提出一個哈希函數是沒證明過的，那沒有人敢用。現代一點的密碼學的書，從一開始就要證明「為什么是安全的」。

所以就需要先定義什么叫“安全”。

有很多不同種類的攻擊模型。“安全”指的是在某一種攻擊模型下的安全。也就是說，一個算法在某個攻擊模型下被證明是安全的了，那在現實生活中也不一定是安全的。因為實際的安全環境，可能跟理論上的攻擊模型會不一樣。比如零知識證明、多方安全計算，都有他們各自的安全模型前提。你選了一個密碼學算法，你就要知道算法的安全模型是什么。你必須搞懂每一種安全的前提和假設，才能不出錯。

每一個后現代密碼學書，英文書居多，一上來就要證明安全性。一直證明到，某個算法在某種攻擊模型下被攻破的幾率，小于一個可忽略值，一般是 2 的 n 次方之一，才可以。

近年來密碼學開始逐漸有了更多現代化的工具去做證明。這種證明不是寫在紙上那種，因為里面的邏輯是越來越復雜的，寫在紙上沒人看得懂，萬一跳步了怎么辦呢？所以要用特殊的程序和工具去證明，保證每一步都執行。而且每一步的引理都必須寫得非常清楚，不能有模糊的地方。

密碼學現在幾乎都是這樣。你要提出新東西，都必須要證明。包括分布式協議也要證明。如果不證，就說明它有的地方沒考慮清楚。有證明，才代表一個協議所有的角落都排查過了。

所以我認為，未來在區塊鏈領域，證明也是會越來越重要的。

12

對區塊鏈行業來說，未來成熟的生態里，智能合約必須具備三個關鍵要素：

1、安全。

保證代碼沒有漏洞。這是大部分搞安全的人正在做的事情，也是比較基礎的東西。但我個人覺得，這件事其實并沒有那么有趣。

2、可信。

可信其實是目的。就是讓用戶信任某個智能合約。比如最近 fomo3d 很熱，但沒人知道這個合約對所有人是否都是公平的。它里面部署了很多不同的合約，有的合約是不開源的。即使開源了，里面的邏輯比較復雜也沒那么容易能看懂。因此智能合約想要可信，最好合約作者的每個聲明都必須有配套的證明。這個證明必須和代碼掛鉤在一起，不管是源代碼還是編譯后的字節碼。

3、規范。

現在很多項目需要多個合約互相交互，所以不同合約之間就必須要有規范。比如，去中心化交易所其實就是一個智能合約。這個智能合約與其他 ERC20 代幣的合約進行交互，互相兌換。去中心化交易所要上幣的時候，審計智能合約有時候會重點去看，這個代幣的管理員有沒有權限凍結 token。如果有權限，那就很危險。

所以我們發現一個很有意思的現象，國外很多做金融 DApp 的公司，到最后都變成了一個合約審計的公司。因為沒有審計公司能幫他們干，他們自己審核了一堆智能合約后，就有這個能力去幫別人審計合約，就可以去接這塊業務了。現在的智能合約本質上都不存在規范。ERC20、ERC721 這些標準都很粗糙。我們手上有形式化驗證的工具，也會幫去中心化交易所審計上幣的代碼，這樣效率會比較高。

我們發現規范性這個問題是很嚴重的。太多的智能合約缺少規范，因此很容易產生很多兼容性問題。比如我們都知道 ERC20 里有一個變量叫 symbol，是用來表示代幣的名字，是叫“比特幣”還是“以太幣”。這個 symbol 的字母大小寫完全是混亂的，因為它沒有具體的規范，規定必須怎么寫。再比如函數執行失敗要不要return false，還是不return？這里也有很多東西沒寫清楚。因為沒寫清楚，大家就各做各的，導致最終的接口不一致。于是很多合約充值就會有漏洞。

我認為合約只有規范了，DApp 才能真正繁榮起來。不僅僅只是 ERC20 這個合約標準，還有許多合約標準都有規范性問題。未來我們很有可能會在 ERC20 上面再搭一個棧，比如去中心化交易所，然后去中心化交易所上面再搭一個金融借貸類的棧，再往上還可以搭金融衍生品、資產管理——但你每往上搭一層，每一層都必須規范。只有每一層都打牢固了，才能造出高樓。

13

我個人相信，區塊鏈安全會是一個細分行業。而且它一定會不斷細分下去。

區塊鏈公司跟很多傳統公司不一樣。傳統公司一定要做大，要把很多業務進行整合，因為只有整合才能發揮優勢。就像 BAT，每家都做外賣，每家都做支付，什么業務都有。歸根到底，它只有把自己整合起來變成怪獸才能勝出。

但區塊鏈行業反而是，做好自己最擅長的事情就是最好的。因為區塊鏈本來就是用來解決生產關系的。傳統公司需要有一個老板發號施令讓員工往同一個方向走。區塊鏈行業是發現一個規律能掙錢，那大家就會自發往那走。

所以通過區塊鏈已經可以解決傳統公司的一些問題了。很多時候，你和別人之間是互惠關系。這種互惠關系加上 token 綁定，就會成為一個小圈子。

就像現在的幣圈，它不是一個公司，就是一個小圈子，組織形式非常松散，但又有一致的利益綁定。這種運作方式遠比一個公司的效率來得高。為什么區塊鏈行業發展速度都很快也是因為這個原因。沒有老板，三人成軍。發展非常靈活。所以我認為，區塊鏈公司不一定需要做大。

智能合約讓人們協作的成本變得很低。這也是我們選擇以智能合約為中心做形式化驗證業務的一個原因。只不過現階段它還不掙錢。但這個方向，它跟傳統 BAT 的業務不太一樣。所以這些巨頭公司也沒辦法進來。

智能合約天生對協作就是友好的。而大公司想的是一定要把別人收購，這樣我們才能一條心。但同時，大公司各部門間的協作又會產生很多內耗。這是傳統公司不可避免的弊病。所以從這個角度來看，小公司也許更有優勢。未來我們認為會出現越來越多的小公司。

14

公鏈的安全和智能合約底層的安全，其實僅僅只是區塊鏈安全領域的一小部分。未來更重要的部分也許是上層業務邏輯的安全。

現階段我們看到的大部分的漏洞是底層的漏洞，比如各種溢出。這是因為現在大家還不了解區塊鏈技術，行業里的程序員沒有經過行業的教育。但未來大家會變得越來越聰明，底層非常低級的安全漏洞會越來越少。

而上層業務會隨著整個行業的發展變得越來越復雜，可能出現的漏洞也會越來越多。代碼的行數在變大，智能合約的數量也在增加。而業務漏洞是安全審計公司做不來的，工具也做不到自動化檢查。因為工具無法理解高層的業務意圖，傳統的安全公司也沒辦法解決這個問題。沒有完善的工具，配套人才非常稀缺。因此，區塊鏈安全是一片藍海。

今年 9 月初，我會在一個學術會議上做報告，給高校的人講「什么是智能合約」。他們很多都沒聽說過智能合約，但一旦他們聽說了，很多人可能就會進來這個行業。因為這些做形式化驗證研究的老師，他們會很敏感地察覺到，智能合約是一個大金礦。現在還沒有多少人在挖。我可能不需要跟他們講具體怎么在智能合約上做形式化驗證，只需要給他們講智能合約現在面臨哪些問題，他們就能意識到這一點。因此，很多高校類的老師出來創業，這可能也會成為區塊鏈的一個趨勢。