麻豆国内精品欧美在线-麻豆国内精品久久久久久-麻豆国产在线观看一区二区-麻豆国产在线观看免费-麻豆国产原创-麻豆国产一区二区在线观看

尋找軟件世界的圣杯

對(duì)很多沒(méi)聽說(shuō)過(guò)「形式化驗(yàn)證」的人，你可能暫時(shí)沒(méi)辦法理解它背后一些很美的東西。

沒(méi)關(guān)系，今天我想用一個(gè)故事向你們介紹這種美。如果你覺得有意思的話，可能也會(huì)順帶理解區(qū)塊鏈美的地方在哪。

 1 

對(duì)我來(lái)說(shuō)，形式化驗(yàn)證是在追尋計(jì)算機(jī)領(lǐng)域里的圣杯。它要解決的問(wèn)題，是怎么保證軟件里沒(méi)有 bug 。你肯定會(huì)很驚訝，軟件有 bug 這件事幾乎是一定的。只要涉及到復(fù)雜代碼，就很難避免出錯(cuò)。

怎么保證它沒(méi)有 bug 呢？

從計(jì)算機(jī)出現(xiàn)開始就有很多人在研究這個(gè)問(wèn)題，但一直沒(méi)人能給出答案。所以，它是一個(gè)圣杯。就像一本誰(shuí)都沒(méi)看過(guò)的武林秘籍。

我大概是 05 年開始搞這個(gè)東西的。形式化驗(yàn)證是一個(gè)非常小眾的研究方向。當(dāng)時(shí)我在安徽的中國(guó)科學(xué)技術(shù)大學(xué)里，我們實(shí)驗(yàn)室想招研究生，非常難招。因?yàn)橥瑢W(xué)們都跑去研究人工智能了。而形式化驗(yàn)證他們很多人壓根就沒(méi)聽說(shuō)過(guò)。

但最近兩年，這個(gè)非常冷門的研究方向突然火了。主要還是因?yàn)閰^(qū)塊鏈橫空出世，吸引了很多人進(jìn)來(lái)研究。就像密碼學(xué)跟著區(qū)塊鏈火起來(lái)一樣。以太坊創(chuàng)始人 V 神一定程度上也助推了「形式化驗(yàn)證」的發(fā)展。

那么，到底什么是形式化驗(yàn)證？

我們都知道，代碼和程序是邏輯性很強(qiáng)的東西。既然邏輯性很強(qiáng)，那我們當(dāng)然也可以用邏輯來(lái)推理它，論證這個(gè)軟件到底安不安全、有沒(méi)有 bug。只不過(guò)平常我們所理解的“推理”，可能都是在自己的大腦里進(jìn)行的。像柯南破案那樣，一步步地推演。但現(xiàn)在我們需要把這個(gè)推理的過(guò)程，用更嚴(yán)謹(jǐn)、更標(biāo)準(zhǔn)的數(shù)學(xué)和數(shù)理邏輯的方式表達(dá)出來(lái)，讓計(jì)算機(jī)能夠看懂——這個(gè)東西就叫形式化驗(yàn)證。

 2 

為什么形式化驗(yàn)證會(huì)非常小眾？

除了因?yàn)楸旧碓趯ふ沂ケ猓€有一個(gè)原因是它對(duì)技術(shù)門檻的要求比較高。

如果你想研究形式化驗(yàn)證，首先需要先弄懂這套邏輯系統(tǒng)的“語(yǔ)言”。人們平常溝通的時(shí)候，講話用的是自然語(yǔ)言和文字，很直接，很簡(jiǎn)單，彼此也很容易聽懂。但邏輯語(yǔ)言全部都是符號(hào)。你必須先弄懂符號(hào)是什么意思。然后，你還要理解怎么把你平常說(shuō)的話，用這些符號(hào)表達(dá)出來(lái)。這個(gè)東西是最花時(shí)間的。

一般一個(gè) PHD 剛?cè)腴T，需要先花上很長(zhǎng)的時(shí)間，不斷看東西，培養(yǎng)這種用符號(hào)表達(dá)的感覺。像小時(shí)候剛開始學(xué)造句一樣。等你會(huì)造句了，最后一步才是開始寫作文。也就是把整個(gè)推理的邏輯論證出來(lái)。“推理”本身又會(huì)涉及到很多理論深度的東西。所以總結(jié)起來(lái)，它對(duì)門檻的要求確實(shí)比較高。

我研究這個(gè)東西十幾年了。我是 01 年在科大讀研，05 開始研究，07 年 PHD 畢業(yè)，然后留在科大當(dāng)老師。讀研的時(shí)候，最開始一段時(shí)期做的是網(wǎng)絡(luò)研究，后來(lái)才做的形式化驗(yàn)證。做了之后我發(fā)現(xiàn)，形式化驗(yàn)證里面有很多特別美的東西。它背后有很多特別美的數(shù)學(xué)理論。但很少有人能觸及到這種美。因?yàn)槟阍谟|及到這種美之前，需要花費(fèi)非常多的時(shí)間來(lái)琢磨。

這點(diǎn)感覺跟區(qū)塊鏈挺像的。區(qū)塊鏈初看很簡(jiǎn)單，但是你深入研究，反復(fù)去做、去試驗(yàn)，花上一些時(shí)間，你才能慢慢領(lǐng)略到區(qū)塊鏈背后美妙的地方在哪。

 3 

當(dāng)時(shí)研究形式化驗(yàn)證，我最大的苦惱是一直沒(méi)能找到合適的應(yīng)用場(chǎng)景。

我們嘗試過(guò)很多方向的應(yīng)用，大多數(shù)是操作系統(tǒng)內(nèi)核的驗(yàn)證，包括很多實(shí)時(shí)性的內(nèi)核，比如工業(yè)控制、醫(yī)療設(shè)備、專用芯片這些東西。

我們還嘗試過(guò)存儲(chǔ)芯片方面的應(yīng)用。閃存芯片上有一層很薄的軟件，這層軟件非常關(guān)鍵，不能有 bug，因?yàn)樗脕?lái)確保存儲(chǔ)和讀取時(shí)候不會(huì)出錯(cuò)。你平常用 u 盤如果沒(méi)有在操作系統(tǒng)里退出直接硬拔出來(lái)，它就有可能會(huì)觸及到這層軟件的 bug，導(dǎo)致數(shù)據(jù)丟失。

我們希望把形式化驗(yàn)證那套東西拿過(guò)來(lái)用，確保這些軟件代碼里沒(méi)有 bug。這些應(yīng)用場(chǎng)景的代碼量比較短又足夠復(fù)雜，所以適合拿來(lái)做驗(yàn)證。

只有代碼足夠復(fù)雜才值得做形式化驗(yàn)證，如果代碼太簡(jiǎn)單就不需要了，你讓程序員肉眼看一下就能判斷有沒(méi)有 bug 了。

但即使是這樣，我們?nèi)匀挥X得形式化驗(yàn)證在工業(yè)應(yīng)用上的性價(jià)比很低。因?yàn)楣こ痰淖兓俣忍炝耍碚摼嚯x實(shí)際使用，其實(shí)還是有不少的差距。

 4 

這個(gè)讓人苦惱的現(xiàn)象一直持續(xù)到 16 年。那時(shí)我開始研究區(qū)塊鏈的底層技術(shù)。

我看了比特幣和以太坊。當(dāng)以太坊出現(xiàn)后，智能合約冒出水面。我很敏銳地察覺到，這里面其實(shí)有一些很適合我們的新機(jī)會(huì)。智能合約是形式化驗(yàn)證非常理想的一個(gè)應(yīng)用場(chǎng)景。

我馬上就和一位朋友商量，要不要一起出來(lái)干這件事：用形式化驗(yàn)證的方式搞區(qū)塊鏈安全。那個(gè)朋友之前在 360 工作，他跟我說(shuō)，要干，不干你將來(lái)一定后悔。他本身也有連續(xù)創(chuàng)業(yè)的經(jīng)驗(yàn)，所以我當(dāng)時(shí)就決定：出來(lái)創(chuàng)業(yè)。

于是今年 4 月份，我們拿了一點(diǎn)錢，就組建了一個(gè)團(tuán)隊(duì)開始搞。這個(gè)團(tuán)隊(duì)也是以我之前在中科大的幾個(gè)學(xué)弟為主，還有一些早期就對(duì)區(qū)塊鏈非常感興趣的 90 后的小朋友。

 5 

現(xiàn)在很多形式化驗(yàn)證慣用的方法是：弄一個(gè)黑盒，然后丟一段代碼進(jìn)去，黑盒再吐出來(lái)一個(gè)結(jié)果：yes or no。

如果是 yes，那就說(shuō)明丟進(jìn)去的這段代碼沒(méi)有問(wèn)題。如果是 no ，就說(shuō)明代碼里有 bug。但這種方式的問(wèn)題在于，這個(gè)盒子本身是個(gè)黑盒。你沒(méi)辦法證明黑盒的正確性。所以這種方式更多還是用來(lái)找 bug。

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

所以這一類形式化驗(yàn)證，你需要依賴于黑盒本身的正確性。當(dāng)然你可以把這個(gè)黑盒開源，讓全世界的人幫你檢查看有沒(méi)有錯(cuò)誤。但很少人有人能這么做。因?yàn)檫@塊技術(shù)目前還沒(méi)有做到那么好。

 6 

我們從 05 年開始研究時(shí)，采用的是另一種最古老、最傳統(tǒng)、也是最笨的辦法。但這種方式有一個(gè)好處是，當(dāng)它回答 yes 的時(shí)候，它會(huì)給出一個(gè)證據(jù)。這個(gè)證據(jù)是一個(gè)數(shù)學(xué)證明。就像你小時(shí)候在黑板上證數(shù)學(xué)題那樣，把證明過(guò)程寫出來(lái)就沒(méi)辦法造假。老師和同學(xué)都可以看到。所有人都可以檢查。

理論上這套方法是可以這樣做的，但實(shí)際上我們還做不到自動(dòng)化。你肯定希望最理想的情況是直接把代碼扔進(jìn)盒子里，然后就能自動(dòng)吐出來(lái)一個(gè)證明。但現(xiàn)在還做不到。這是理論的天花板。

我們現(xiàn)在是半自動(dòng)化來(lái)做這件事。你想象下這個(gè)盒子上有一些輔助的把手，當(dāng)你發(fā)現(xiàn)盒子轉(zhuǎn)不動(dòng)的時(shí)候，就需要人工手動(dòng)去搖一搖，丟進(jìn)一段代碼，吐出來(lái)一段證明。這是一個(gè)通過(guò)人操控的盒子。

其實(shí)這個(gè)盒子是非常復(fù)雜的，上面有很多的把手，需要大量做研究的人不停地?fù)u，而且需要搖上好幾年。我們當(dāng)時(shí)跟很多國(guó)內(nèi)的團(tuán)隊(duì)聊，他們稱我們是原教旨主義。因?yàn)橄裎覀冞@樣干的人很少。這種傳統(tǒng)的做法沒(méi)法工業(yè)化應(yīng)用。懂得怎么搖盒子把手的人其實(shí)很少很少。但我當(dāng)時(shí)就很堅(jiān)信，這個(gè)看似傳統(tǒng)的方法才是未來(lái)。

這里面很多人誤解了，覺得由人去搖把手很累，但這其實(shí)是人類體現(xiàn)自我價(jià)值的意義。就像證明“哥德巴赫猜想”是人應(yīng)該要做的事情，不可能讓機(jī)器來(lái)做。人存在的意義就是在盒子卡住的關(guān)鍵時(shí)候去推動(dòng)一下。

從一開始我就很接受這種哲學(xué)觀。它就應(yīng)該這么做。但另一方面，你搖上那么幾年這個(gè)問(wèn)題怎么解決？當(dāng)時(shí)我認(rèn)為，人搖的時(shí)間一定是越來(lái)越快的。把手會(huì)越來(lái)越少，盒子會(huì)越來(lái)越簡(jiǎn)單。

事實(shí)也的確如此。經(jīng)過(guò)十幾年的發(fā)展，這個(gè)方法反而被越來(lái)越多的人接納。因?yàn)檫@個(gè)東西跟其他計(jì)算機(jī)技術(shù)的發(fā)展是一樣的。人們寫軟件是用一層一層的 stack ，“堆棧”，不斷壘起來(lái)。這種傳統(tǒng)的證明方式之所以低效，是因?yàn)樗鼪](méi)有軟件棧，用的全部是最底層的技術(shù)，類似 if、else、and、or 這種非常底層的證明語(yǔ)言，那當(dāng)然會(huì)很累。

但如果你有對(duì)應(yīng)的軟件堆棧，有相應(yīng)的框架和工具，你在很高的抽象層上去做證明，那就不會(huì)很累了。你不能因?yàn)楝F(xiàn)在還沒(méi)有這種技術(shù)棧，就說(shuō)這條方向沒(méi)有前途。這是我從一開始就非常相信的。事實(shí)也驗(yàn)證了是正確的。現(xiàn)在很多人都在往這個(gè)方向走。

 7 

為什么智能合約出現(xiàn)后我會(huì)非常激動(dòng)呢？

因?yàn)橹悄芎霞s的代碼量也是比較短的，但它對(duì)安全性的要求更高。智能合約一旦部署到區(qū)塊鏈上就不能再修改，所以它一定不能出錯(cuò)。這些基本的特性就決定了它對(duì)形式化驗(yàn)證是有需求的。

再加上區(qū)塊鏈的設(shè)計(jì)哲學(xué)是去中心化的，所以想要保證「智能合約的代碼里沒(méi)有 bug」 ，這件事必須用一種去中心化的方式去證明。

也就是說(shuō)，智能合約發(fā)布到網(wǎng)上，如果它能自帶一個(gè)證明，就是最好的。

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

這種自帶證明的方式，跟「一個(gè)中心化的黑盒直接吐出 yes or no 的結(jié)果」相比，它跟區(qū)塊鏈的思想是一致的。通過(guò)某一個(gè)機(jī)構(gòu)為智能合約做安全審計(jì)也不是未來(lái)。因?yàn)樗匀灰蕾囉跈C(jī)構(gòu)的中心化的權(quán)威，無(wú)法確保智能合約可信。

而從另一方面來(lái)說(shuō)，這種去中心化的方式效率上會(huì)更高。因?yàn)樯勺C明是非常難的，需要大量人類的智慧，但檢驗(yàn)證明是很簡(jiǎn)單的。機(jī)器非常容易做。檢驗(yàn)的難度，跟代碼的行數(shù)成正比。哪怕要驗(yàn)證的代碼有一億行，用機(jī)器來(lái)做檢查仍然會(huì)非常快，因?yàn)榭梢圆⑿凶觥?/p>

所以我非常堅(jiān)信，智能合約是我們這種傳統(tǒng)的形式化驗(yàn)證方法一個(gè)絕佳應(yīng)用場(chǎng)景。它去中心化的精神也和區(qū)塊鏈很像。

8

在我的腦海里，未來(lái)所有的智能合約發(fā)布到網(wǎng)上都必須帶一個(gè)自己的數(shù)學(xué)證明，

這個(gè)證明用來(lái)：

證明你干了什么事

證明你的管理員權(quán)限

證明你的合約對(duì)參與各方都是公平的

證明你沒(méi)有后門、你的分紅、鎖倉(cāng)機(jī)制到底是什么樣的

……

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

帶了這個(gè)數(shù)學(xué)證明，對(duì)于用戶來(lái)說(shuō)，哪怕你看不懂證明過(guò)程到底是怎么樣的，你也可以隨時(shí)就用另外的工具去檢查這個(gè)證明是否正確。

這套檢查的工具可以由其他不同的人提供，所有人都可以來(lái)做這樣的工具。這樣就給了用戶一個(gè)選擇，讓發(fā)布智能合約的人，和負(fù)責(zé)審計(jì)的人，都沒(méi)辦法作弊。

9

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

其實(shí)遠(yuǎn)遠(yuǎn)不是。

為一個(gè)程序帶上一個(gè)證明，這個(gè)證明寫了數(shù)學(xué)推理的過(guò)程，用來(lái)論證程序自身沒(méi)有 bug——但我們都知道，數(shù)學(xué)推理需要有一些公理作為前提，然后才能往后進(jìn)行推導(dǎo)。

如果這個(gè)前提本身是錯(cuò)誤的，推理是不是也就不成立了？

舉個(gè)例子：密碼學(xué)里的加密問(wèn)題。

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

在程序里面也是一樣的。

比如我想證明 EVM （以太坊虛擬機(jī)）里面的一段代碼跑出來(lái)的返回結(jié)果是“1”，那么我需要先把程序的語(yǔ)義表達(dá)出來(lái)，而這就是代碼級(jí)的形式化驗(yàn)證會(huì)遇到的一個(gè)問(wèn)題：很多編程語(yǔ)言的手冊(cè)很不完善，因此程序的語(yǔ)義翻譯很難做到 100% 精準(zhǔn)。

一套編程語(yǔ)言的設(shè)計(jì)，語(yǔ)義往往會(huì)存在模糊的地方。因此，形式化語(yǔ)義的時(shí)候就會(huì)遇到一個(gè)巨大的鴻溝。

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

形式化驗(yàn)證還有一個(gè)嚴(yán)重的依賴，是推理的邏輯本身。換句話說(shuō)，就是推理的邏輯本身有沒(méi)有問(wèn)題。這點(diǎn)也是有可能會(huì)受到質(zhì)疑的。

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

所謂的“自洽”是指在這個(gè)邏輯系統(tǒng)里沒(méi)有前提的情況下無(wú)法推出 False。用人話來(lái)說(shuō)，你的邏輯不能前后矛盾。所謂的自洽系統(tǒng)，就是你永遠(yuǎn)不可能說(shuō)出自相矛盾的話。但“自洽”是需要證明出來(lái)的。一旦你要證明這個(gè)邏輯系統(tǒng)是自洽的，你就必須用一個(gè)更復(fù)雜的邏輯系統(tǒng)來(lái)證明。這個(gè)更復(fù)雜的邏輯系統(tǒng)又需要一個(gè)超級(jí)復(fù)雜的邏輯系統(tǒng)來(lái)證明它的自洽。

哥德爾第二不完備性定理明確提出：不可能有一個(gè)系統(tǒng)能證明自己自洽。它甚至很明確的找到反例說(shuō)，如果你找到了一個(gè)系統(tǒng)能證明自己的系統(tǒng)邏輯自洽，那么你的邏輯就不自洽。GEB 這本神書就在談?wù)撨@個(gè)問(wèn)題背后的整套哲學(xué)系統(tǒng)，整本書大概七百多頁(yè)，非常長(zhǎng)，也很深，到現(xiàn)在我也才看了三分之一。

我們?cè)谛问交?yàn)證里用來(lái)推理程序所用的邏輯，它有沒(méi)有問(wèn)題呢？其實(shí)它也是個(gè)黑盒。但這個(gè)黑盒跟我上面說(shuō)的那個(gè)黑盒不太一樣。它相對(duì)比較穩(wěn)定，不怎么變化。但它背后依賴的數(shù)學(xué)理論，“自洽性”也還沒(méi)有人證明過(guò)。只是有幾個(gè)數(shù)學(xué)家說(shuō)，這里面大概是沒(méi)有問(wèn)題的。

其實(shí)在邏輯學(xué)上，有很多公理是互相矛盾的。

嚴(yán)格來(lái)說(shuō)，必須真的有人證出來(lái)兩個(gè)公理是不矛盾的、可以一起用，我們才可以去使用這些公理。但這些東西太復(fù)雜了，很多至今都沒(méi)有人能搞懂。

有人說(shuō)，數(shù)學(xué)證明是特別純粹的。證出來(lái)是對(duì)就是對(duì)，是錯(cuò)就是錯(cuò)。其實(shí)是因?yàn)樗赡懿惶斫膺@套東西。搞邏輯學(xué)的人都知道，很多公理單獨(dú)使用可能沒(méi)有問(wèn)題，但你再加入一個(gè)公理，這個(gè)系統(tǒng)還能否自洽就是未知的了。因此，很多數(shù)學(xué)家會(huì)憑著自己的直覺加進(jìn)去，覺得沒(méi)問(wèn)題，但具體有沒(méi)有證明過(guò)呢？需要另一套更復(fù)雜的邏輯。

這里面是有很多開放性的問(wèn)題。有很多不同的選擇。我們?cè)谧龅臅r(shí)候，傾向于不去輕易引入一些甚至很有名的公理。能不用就不用。比如反證法，反正法會(huì)跟很多公理發(fā)生矛盾，如果用了，說(shuō)不定哪天就出問(wèn)題了。

10

所以，我們可能永遠(yuǎn)都找不到圣杯。

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

當(dāng)然，我覺得這個(gè)支點(diǎn)已經(jīng)是人類文明的精華了。因此還是比較可靠的。

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

11

那么，形式化驗(yàn)證跟大家更熟悉的密碼學(xué)，他們之間有關(guān)系嗎？

有關(guān)系。

我個(gè)人覺得，密碼學(xué)這套歷史有一條線，可以把它分隔成兩半。在這條線之后，密碼學(xué)所有東西你要證明可靠；而在之前，你往往不需要證明，全靠經(jīng)驗(yàn)。

如果你現(xiàn)在隨便去買一本密碼學(xué)的書，大概率翻開，第一章會(huì)講“對(duì)稱加密”、第二章講“非對(duì)稱加密”、第三章講“哈希、隨機(jī)數(shù)”。這些東西都是沒(méi)有證明的，只是教你怎么用而已。所以到頭來(lái)，你可能只是背了一堆的算法。這叫前密碼學(xué)。

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

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

有很多不同種類的攻擊模型。“安全”指的是在某一種攻擊模型下的安全。也就是說(shuō)，一個(gè)算法在某個(gè)攻擊模型下被證明是安全的了，那在現(xiàn)實(shí)生活中也不一定是安全的。因?yàn)閷?shí)際的安全環(huán)境，可能跟理論上的攻擊模型會(huì)不一樣。比如零知識(shí)證明、多方安全計(jì)算，都有他們各自的安全模型前提。你選了一個(gè)密碼學(xué)算法，你就要知道算法的安全模型是什么。你必須搞懂每一種安全的前提和假設(shè)，才能不出錯(cuò)。

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

近年來(lái)密碼學(xué)開始逐漸有了更多現(xiàn)代化的工具去做證明。這種證明不是寫在紙上那種，因?yàn)槔锩娴倪壿嬍窃絹?lái)越復(fù)雜的，寫在紙上沒(méi)人看得懂，萬(wàn)一跳步了怎么辦呢？所以要用特殊的程序和工具去證明，保證每一步都執(zhí)行。而且每一步的引理都必須寫得非常清楚，不能有模糊的地方。

密碼學(xué)現(xiàn)在幾乎都是這樣。你要提出新東西，都必須要證明。包括分布式協(xié)議也要證明。如果不證，就說(shuō)明它有的地方?jīng)]考慮清楚。有證明，才代表一個(gè)協(xié)議所有的角落都排查過(guò)了。

所以我認(rèn)為，未來(lái)在區(qū)塊鏈領(lǐng)域，證明也是會(huì)越來(lái)越重要的。

12

對(duì)區(qū)塊鏈行業(yè)來(lái)說(shuō)，未來(lái)成熟的生態(tài)里，智能合約必須具備三個(gè)關(guān)鍵要素：

1、安全。

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

2、可信。

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

3、規(guī)范。

現(xiàn)在很多項(xiàng)目需要多個(gè)合約互相交互，所以不同合約之間就必須要有規(guī)范。比如，去中心化交易所其實(shí)就是一個(gè)智能合約。這個(gè)智能合約與其他 ERC20 代幣的合約進(jìn)行交互，互相兌換。去中心化交易所要上幣的時(shí)候，審計(jì)智能合約有時(shí)候會(huì)重點(diǎn)去看，這個(gè)代幣的管理員有沒(méi)有權(quán)限凍結(jié) token。如果有權(quán)限，那就很危險(xiǎn)。

所以我們發(fā)現(xiàn)一個(gè)很有意思的現(xiàn)象，國(guó)外很多做金融 DApp 的公司，到最后都變成了一個(gè)合約審計(jì)的公司。因?yàn)闆](méi)有審計(jì)公司能幫他們干，他們自己審核了一堆智能合約后，就有這個(gè)能力去幫別人審計(jì)合約，就可以去接這塊業(yè)務(wù)了。現(xiàn)在的智能合約本質(zhì)上都不存在規(guī)范。ERC20、ERC721 這些標(biāo)準(zhǔn)都很粗糙。我們手上有形式化驗(yàn)證的工具，也會(huì)幫去中心化交易所審計(jì)上幣的代碼，這樣效率會(huì)比較高。

我們發(fā)現(xiàn)規(guī)范性這個(gè)問(wèn)題是很嚴(yán)重的。太多的智能合約缺少規(guī)范，因此很容易產(chǎn)生很多兼容性問(wèn)題。比如我們都知道 ERC20 里有一個(gè)變量叫 symbol，是用來(lái)表示代幣的名字，是叫“比特幣”還是“以太幣”。這個(gè) symbol 的字母大小寫完全是混亂的，因?yàn)樗鼪](méi)有具體的規(guī)范，規(guī)定必須怎么寫。再比如函數(shù)執(zhí)行失敗要不要return false，還是不return？這里也有很多東西沒(méi)寫清楚。因?yàn)闆](méi)寫清楚，大家就各做各的，導(dǎo)致最終的接口不一致。于是很多合約充值就會(huì)有漏洞。

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

13

我個(gè)人相信，區(qū)塊鏈安全會(huì)是一個(gè)細(xì)分行業(yè)。而且它一定會(huì)不斷細(xì)分下去。

區(qū)塊鏈公司跟很多傳統(tǒng)公司不一樣。傳統(tǒng)公司一定要做大，要把很多業(yè)務(wù)進(jìn)行整合，因?yàn)橹挥姓喜拍馨l(fā)揮優(yōu)勢(shì)。就像 BAT，每家都做外賣，每家都做支付，什么業(yè)務(wù)都有。歸根到底，它只有把自己整合起來(lái)變成怪獸才能勝出。

但區(qū)塊鏈行業(yè)反而是，做好自己最擅長(zhǎng)的事情就是最好的。因?yàn)閰^(qū)塊鏈本來(lái)就是用來(lái)解決生產(chǎn)關(guān)系的。傳統(tǒng)公司需要有一個(gè)老板發(fā)號(hào)施令讓員工往同一個(gè)方向走。區(qū)塊鏈行業(yè)是發(fā)現(xiàn)一個(gè)規(guī)律能掙錢，那大家就會(huì)自發(fā)往那走。

所以通過(guò)區(qū)塊鏈已經(jīng)可以解決傳統(tǒng)公司的一些問(wèn)題了。很多時(shí)候，你和別人之間是互惠關(guān)系。這種互惠關(guān)系加上 token 綁定，就會(huì)成為一個(gè)小圈子。

就像現(xiàn)在的幣圈，它不是一個(gè)公司，就是一個(gè)小圈子，組織形式非常松散，但又有一致的利益綁定。這種運(yùn)作方式遠(yuǎn)比一個(gè)公司的效率來(lái)得高。為什么區(qū)塊鏈行業(yè)發(fā)展速度都很快也是因?yàn)檫@個(gè)原因。沒(méi)有老板，三人成軍。發(fā)展非常靈活。所以我認(rèn)為，區(qū)塊鏈公司不一定需要做大。

智能合約讓人們協(xié)作的成本變得很低。這也是我們選擇以智能合約為中心做形式化驗(yàn)證業(yè)務(wù)的一個(gè)原因。只不過(guò)現(xiàn)階段它還不掙錢。但這個(gè)方向，它跟傳統(tǒng) BAT 的業(yè)務(wù)不太一樣。所以這些巨頭公司也沒(méi)辦法進(jìn)來(lái)。

智能合約天生對(duì)協(xié)作就是友好的。而大公司想的是一定要把別人收購(gòu)，這樣我們才能一條心。但同時(shí)，大公司各部門間的協(xié)作又會(huì)產(chǎn)生很多內(nèi)耗。這是傳統(tǒng)公司不可避免的弊病。所以從這個(gè)角度來(lái)看，小公司也許更有優(yōu)勢(shì)。未來(lái)我們認(rèn)為會(huì)出現(xiàn)越來(lái)越多的小公司。

14

公鏈的安全和智能合約底層的安全，其實(shí)僅僅只是區(qū)塊鏈安全領(lǐng)域的一小部分。未來(lái)更重要的部分也許是上層業(yè)務(wù)邏輯的安全。

現(xiàn)階段我們看到的大部分的漏洞是底層的漏洞，比如各種溢出。這是因?yàn)楝F(xiàn)在大家還不了解區(qū)塊鏈技術(shù)，行業(yè)里的程序員沒(méi)有經(jīng)過(guò)行業(yè)的教育。但未來(lái)大家會(huì)變得越來(lái)越聰明，底層非常低級(jí)的安全漏洞會(huì)越來(lái)越少。

而上層業(yè)務(wù)會(huì)隨著整個(gè)行業(yè)的發(fā)展變得越來(lái)越復(fù)雜，可能出現(xiàn)的漏洞也會(huì)越來(lái)越多。代碼的行數(shù)在變大，智能合約的數(shù)量也在增加。而業(yè)務(wù)漏洞是安全審計(jì)公司做不來(lái)的，工具也做不到自動(dòng)化檢查。因?yàn)楣ぞ邿o(wú)法理解高層的業(yè)務(wù)意圖，傳統(tǒng)的安全公司也沒(méi)辦法解決這個(gè)問(wèn)題。沒(méi)有完善的工具，配套人才非常稀缺。因此，區(qū)塊鏈安全是一片藍(lán)海。

今年 9 月初，我會(huì)在一個(gè)學(xué)術(shù)會(huì)議上做報(bào)告，給高校的人講「什么是智能合約」。他們很多都沒(méi)聽說(shuō)過(guò)智能合約，但一旦他們聽說(shuō)了，很多人可能就會(huì)進(jìn)來(lái)這個(gè)行業(yè)。因?yàn)檫@些做形式化驗(yàn)證研究的老師，他們會(huì)很敏感地察覺到，智能合約是一個(gè)大金礦。現(xiàn)在還沒(méi)有多少人在挖。我可能不需要跟他們講具體怎么在智能合約上做形式化驗(yàn)證，只需要給他們講智能合約現(xiàn)在面臨哪些問(wèn)題，他們就能意識(shí)到這一點(diǎn)。因此，很多高校類的老師出來(lái)創(chuàng)業(yè)，這可能也會(huì)成為區(qū)塊鏈的一個(gè)趨勢(shì)。