現(xiàn)代社會是一臺龐大的機器任岸。它讓我們每個人都從事精細(xì)化分工的工作。于是「專業(yè)」越來越像一個黑盒狡刘，人們可以通過黑盒的“API”與不同專業(yè)的人進行合作渴邦，卻很難了解黑盒內(nèi)部到底是怎樣運作的易核。

正因為如此洋措，區(qū)塊鏈對我而言是一個有意思的領(lǐng)域菇用。因為這里學(xué)科交叉的現(xiàn)象非常普遍。你不僅會遇到計算機行業(yè)里的人澜术，還會遇到經(jīng)濟艺蝴、金融、政治與社會學(xué)的人鸟废。和這些人聊天又是一種非常神秘的體驗猜敢。就好像，他們會為你拆開一個陌生的玩具侮攀，展示其中的齒輪和零件锣枝。

大概一周前，我們約了一個區(qū)塊鏈安全團隊的創(chuàng)始人聊天兰英。這位朋友之前在中科大研究了十幾年的“形式化驗證”撇叁，屬于非常冷門小眾的專業(yè)。機緣巧合畦贸，最近這個專業(yè)因為區(qū)塊鏈的出現(xiàn)火了陨闹，就像“密碼學(xué)”那樣。我們和他聊了很久薄坏，他用兩個小時為我們拆開了另一個陌生的玩具趋厉。這讓我們感到非常有趣。因此現(xiàn)在我們想把這個玩具也分享給橙皮書的讀者們胶坠。

如果你是一個好奇心很重的人君账，我們強烈推薦你閱讀這篇文章。它會用說人話的方式告訴你“形式化驗證”是用來干嘛的沈善，為什么區(qū)塊鏈安全的未來只有開源是不夠的乡数，它還應(yīng)該用去中心化的方式，由機器自己證明自己可信闻牡，而不是把信任寄托于一個中心化的安全公司净赴。

ps：文章末尾有福利彩蛋，不要錯過罩润。

郭宇玖翅，從 05 年開始在中科大研究「形式化驗證」，現(xiàn)在是區(qū)塊鏈安全公司安比（SECBIT）實驗室創(chuàng)始人。

?“??有人說金度，數(shù)學(xué)證明是特別純粹的应媚，證出來是對就是對，是錯就是錯猜极。其實這個說法是錯誤的珍特。我們可能永遠(yuǎn)都找不到圣杯。歸根到底魔吐，我們總要依賴于一點點其他的東西。你總需要一個小小的支點莱找。這個支點已經(jīng)是人類文明的精華了酬姆，但它永遠(yuǎn)做不到 100% 可靠。

尋找軟件世界的圣杯

口述 | 郭宇

采訪奥溺、整理 | 橙皮書

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

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

?1?

對我來說立美，形式化驗證是在追尋計算機領(lǐng)域里的圣杯。它要解決的問題方灾，是怎么保證軟件里沒有 bug 建蹄。你肯定會很驚訝，軟件有 bug 這件事幾乎是一定的裕偿。只要涉及到復(fù)雜代碼洞慎，就很難避免出錯。

怎么保證它沒有 bug 呢嘿棘？

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

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

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

那么碳默，到底什么是形式化驗證贾陷？

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

?2?

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

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

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

一般一個 PHD 剛?cè)腴T速和，需要先花上很長的時間，不斷看東西剥汤，培養(yǎng)這種用符號表達的感覺颠放。像小時候剛開始學(xué)造句一樣。等你會造句了吭敢，最后一步才是開始寫作文碰凶。也就是把整個推理的邏輯論證出來÷雇眨“推理”本身又會涉及到很多理論深度的東西欲低。所以總結(jié)起來，它對門檻的要求確實比較高畜晰。

我研究這個東西十幾年了伸头。我是 01 年在科大讀研，05 開始研究舷蟀，07 年 PHD 畢業(yè)，然后留在科大當(dāng)老師面哼。讀研的時候野宜，最開始一段時期做的是網(wǎng)絡(luò)研究，后來才做的形式化驗證魔策。做了之后我發(fā)現(xiàn)匈子，形式化驗證里面有很多特別美的東西。它背后有很多特別美的數(shù)學(xué)理論闯袒。但很少有人能觸及到這種美虎敦。因為你在觸及到這種美之前，需要花費非常多的時間來琢磨政敢。

這點感覺跟區(qū)塊鏈挺像的其徙。區(qū)塊鏈初看很簡單，但是你深入研究喷户，反復(fù)去做唾那、去試驗，花上一些時間褪尝，你才能慢慢領(lǐng)略到區(qū)塊鏈背后美妙的地方在哪闹获。

?3?

當(dāng)時研究形式化驗證，我最大的苦惱是一直沒能找到合適的應(yīng)用場景河哑。

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

我們還嘗試過存儲芯片方面的應(yīng)用轨功。閃存芯片上有一層很薄的軟件旭斥，這層軟件非常關(guān)鍵，不能有 bug古涧，因為它要用來確保存儲和讀取時候不會出錯垂券。你平常用 u 盤如果沒有在操作系統(tǒng)里退出直接硬拔出來，它就有可能會觸及到這層軟件的 bug羡滑，導(dǎo)致數(shù)據(jù)丟失菇爪。

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

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

但即使是這樣有梆，我們?nèi)匀挥X得形式化驗證在工業(yè)應(yīng)用上的性價比很低是尖。因為工程的變化速度太快了，理論距離實際使用泥耀，其實還是有不少的差距饺汹。

?4?

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

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

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

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

?5?

現(xiàn)在很多形式化驗證慣用的方法是：弄一個黑盒生百，然后丟一段代碼進去，黑盒再吐出來一個結(jié)果：yes or no柄延。

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

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

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

?6?

我們從 05 年開始研究時族沃，采用的是另一種最古老、最傳統(tǒng)泌参、也是最笨的辦法脆淹。但這種方式有一個好處是，當(dāng)它回答 yes 的時候沽一，它會給出一個證據(jù)盖溺。這個證據(jù)是一個數(shù)學(xué)證明。就像你小時候在黑板上證數(shù)學(xué)題那樣铣缠，把證明過程寫出來就沒辦法造假烘嘱。老師和同學(xué)都可以看到昆禽。所有人都可以檢查。

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

我們現(xiàn)在是半自動化來做這件事牍蜂。你想象下這個盒子上有一些輔助的把手漾根，當(dāng)你發(fā)現(xiàn)盒子轉(zhuǎn)不動的時候，就需要人工手動去搖一搖鲫竞，丟進一段代碼辐怕，吐出來一段證明。這是一個通過人操控的盒子从绘。

其實這個盒子是非常復(fù)雜的寄疏，上面有很多的把手，需要大量做研究的人不停地?fù)u僵井，而且需要搖上好幾年陕截。我們當(dāng)時跟很多國內(nèi)的團隊聊，他們稱我們是原教旨主義批什。因為像我們這樣干的人很少农曲。這種傳統(tǒng)的做法沒法工業(yè)化應(yīng)用。懂得怎么搖盒子把手的人其實很少很少驻债。但我當(dāng)時就很堅信乳规，這個看似傳統(tǒng)的方法才是未來。

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

從一開始我就很接受這種哲學(xué)觀拆祈。它就應(yīng)該這么做恨闪。但另一方面，你搖上那么幾年這個問題怎么解決放坏？當(dāng)時我認(rèn)為凛剥，人搖的時間一定是越來越快的。把手會越來越少轻姿，盒子會越來越簡單犁珠。

事實也的確如此逻炊。經(jīng)過十幾年的發(fā)展，這個方法反而被越來越多的人接納犁享。因為這個東西跟其他計算機技術(shù)的發(fā)展是一樣的余素。人們寫軟件是用一層一層的 stack ，“堆棿独ィ”桨吊，不斷壘起來。這種傳統(tǒng)的證明方式之所以低效凤巨，是因為它沒有軟件棧视乐，用的全部是最底層的技術(shù)，類似 if敢茁、else佑淀、and、or 這種非常底層的證明語言彰檬，那當(dāng)然會很累伸刃。

但如果你有對應(yīng)的軟件堆棧，有相應(yīng)的框架和工具逢倍，你在很高的抽象層上去做證明捧颅，那就不會很累了。你不能因為現(xiàn)在還沒有這種技術(shù)棧较雕，就說這條方向沒有前途碉哑。這是我從一開始就非常相信的。事實也驗證了是正確的×两現(xiàn)在很多人都在往這個方向走扣典。

?7?

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

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

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

也就是說序六，智能合約發(fā)布到網(wǎng)上任连，如果它能自帶一個證明，就是最好的例诀。

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

這種自帶證明的方式拱她，跟「一個中心化的黑盒直接吐出 yes or no 的結(jié)果」相比二驰，它跟區(qū)塊鏈的思想是一致的。通過某一個機構(gòu)為智能合約做安全審計也不是未來秉沼。因為它仍然依賴于機構(gòu)的中心化的權(quán)威桶雀，無法確保智能合約可信。

而從另一方面來說唬复，這種去中心化的方式效率上會更高矗积。因為生成證明是非常難的，需要大量人類的智慧敞咧，但檢驗證明是很簡單的棘捣。

機器非常容易做

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

8

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

這個證明用來：

• 證明你干了什么事

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

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

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

• ……

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

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

這套檢查的工具可以由其他不同的人提供甜橱，所有人都可以來做這樣的工具逊笆。這樣就給了用戶一個選擇，讓發(fā)布智能合約的人岂傲，和負(fù)責(zé)審計的人难裆，都沒辦法作弊。

9

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

其實遠(yuǎn)遠(yuǎn)不是乃戈。

為一個程序帶上一個證明褂痰，這個證明寫了數(shù)學(xué)推理的過程，用來論證程序自身沒有 bug——但我們都知道偏化，數(shù)學(xué)推理需要有一些公理作為前提脐恩，然后才能往后進行推導(dǎo)。

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

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

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

在程序里面也是一樣的汗洒。

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

一套編程語言的設(shè)計憨攒，語義往往會存在模糊的地方世杀。因此，形式化語義的時候就會遇到一個巨大的鴻溝肝集。

EVM 的設(shè)計水平已經(jīng)算是比較高的了瞻坝，以太坊黃皮書對語義的描述寫得很清楚，所以它可能是有 99.99%的準(zhǔn)確度杏瞻，但也不是 100%所刀。最終翻譯到形式化驗證里，理論上還是有可能存在問題伐憾。如果有問題勉痴，推理的過程和實際在 EVM 上跑的過程赫模，二者就不一致了树肃。這樣推理過程本身就不可靠，所有的證明就沒有意義了瀑罗。這個偏差是一定存在的胸嘴。

形式化驗證還有一個嚴(yán)重的依賴雏掠，是推理的邏輯本身。換句話說劣像，就是推理的邏輯本身有沒有問題乡话。這點也是有可能會受到質(zhì)疑的。

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

所謂的“自洽”是指在這個邏輯系統(tǒng)里沒有前提的情況下無法推出 False庇楞。用人話來說，你的邏輯不能前后矛盾否纬。所謂的自洽系統(tǒng)吕晌，就是你永遠(yuǎn)不可能說出自相矛盾的話。但“自洽”是需要證明出來的烦味。一旦你要證明這個邏輯系統(tǒng)是自洽的聂使，你就必須用一個更復(fù)雜的邏輯系統(tǒng)來證明。這個更復(fù)雜的邏輯系統(tǒng)又需要一個超級復(fù)雜的邏輯系統(tǒng)來證明它的自洽谬俄。

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

我們在形式化驗證里用來推理程序所用的邏輯扼劈，它有沒有問題呢？其實它也是個黑盒菲驴。但這個黑盒跟我上面說的那個黑盒不太一樣荐吵。它相對比較穩(wěn)定，不怎么變化。但它背后依賴的數(shù)學(xué)理論先煎，“自洽性”也還沒有人證明過贼涩。只是有幾個數(shù)學(xué)家說，這里面大概是沒有問題的薯蝎。

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

嚴(yán)格來說占锯，必須真的有人證出來兩個公理是不矛盾的袒哥、可以一起用，我們才可以去使用這些公理消略。但這些東西太復(fù)雜了统诺，很多至今都沒有人能搞懂。

有人說疑俭，數(shù)學(xué)證明是特別純粹的粮呢。證出來是對就是對，是錯就是錯钞艇。其實是因為他可能不太理解這套東西啄寡。搞邏輯學(xué)的人都知道，很多公理單獨使用可能沒有問題哩照，但你再加入一個公理挺物，這個系統(tǒng)還能否自洽就是未知的了。因此飘弧，很多數(shù)學(xué)家會憑著自己的直覺加進去识藤，覺得沒問題，但具體有沒有證明過呢次伶？需要另一套更復(fù)雜的邏輯痴昧。

這里面是有很多開放性的問題。有很多不同的選擇冠王。我們在做的時候赶撰，傾向于不去輕易引入一些甚至很有名的公理。能不用就不用柱彻。比如反證法豪娜，反正法會跟很多公理發(fā)生矛盾，如果用了哟楷，說不定哪天就出問題了瘤载。

10

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

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

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

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

11

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

有關(guān)系鞭衩。

我個人覺得，密碼學(xué)這套歷史有一條線娃善，可以把它分隔成兩半论衍。在這條線之后，密碼學(xué)所有東西你要證明可靠聚磺；而在之前坯台，你往往不需要證明，全靠經(jīng)驗瘫寝。

如果你現(xiàn)在隨便去買一本密碼學(xué)的書蜒蕾，大概率翻開，第一章會講“對稱加密”焕阿、第二章講“非對稱加密”咪啡、第三章講“哈希、隨機數(shù)”暮屡。這些東西都是沒有證明的瑟匆，只是教你怎么用而已。所以到頭來栽惶，你可能只是背了一堆的算法愁溜。這叫前密碼學(xué)。

但現(xiàn)在不一樣了⊥獬В現(xiàn)在如果你自己想提出一個密碼學(xué)的東西冕象，你必須先證明它的安全性。所以從某個時候開始汁蝶，這在學(xué)術(shù)上稱作 Provable Security渐扮，“可證安全性”论悴。如果現(xiàn)在新提出一個哈希函數(shù)是沒證明過的，那沒有人敢用∧孤桑現(xiàn)代一點的密碼學(xué)的書膀估，從一開始就要證明「為什么是安全的」。

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

有很多不同種類的攻擊模型察纯。“安全”指的是在某一種攻擊模型下的安全。也就是說针肥，一個算法在某個攻擊模型下被證明是安全的了饼记，那在現(xiàn)實生活中也不一定是安全的。因為實際的安全環(huán)境慰枕，可能跟理論上的攻擊模型會不一樣具则。比如零知識證明、多方安全計算具帮，都有他們各自的安全模型前提博肋。你選了一個密碼學(xué)算法，你就要知道算法的安全模型是什么蜂厅。你必須搞懂每一種安全的前提和假設(shè)束昵，才能不出錯。

每一個后現(xiàn)代密碼學(xué)書葛峻，英文書居多锹雏，一上來就要證明安全性。一直證明到术奖，某個算法在某種攻擊模型下被攻破的幾率礁遵，小于一個可忽略值，一般是 2 的 n 次方之一采记，才可以佣耐。

近年來密碼學(xué)開始逐漸有了更多現(xiàn)代化的工具去做證明。這種證明不是寫在紙上那種唧龄，因為里面的邏輯是越來越復(fù)雜的兼砖，寫在紙上沒人看得懂，萬一跳步了怎么辦呢既棺？所以要用特殊的程序和工具去證明讽挟，保證每一步都執(zhí)行。而且每一步的引理都必須寫得非常清楚丸冕，不能有模糊的地方耽梅。

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

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

12

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

1沃琅、安全哗咆。

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

2年碘、可信。

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

3疯兼、規(guī)范然遏。

現(xiàn)在很多項目需要多個合約互相交互，所以不同合約之間就必須要有規(guī)范吧彪。比如啦鸣，去中心化交易所其實就是一個智能合約。這個智能合約與其他 ERC20 代幣的合約進行交互来氧，互相兌換诫给。去中心化交易所要上幣的時候香拉，審計智能合約有時候會重點去看，這個代幣的管理員有沒有權(quán)限凍結(jié) token中狂。如果有權(quán)限凫碌，那就很危險。

所以我們發(fā)現(xiàn)一個很有意思的現(xiàn)象胃榕，國外很多做金融 DApp 的公司盛险，到最后都變成了一個合約審計的公司。因為沒有審計公司能幫他們干勋又，他們自己審核了一堆智能合約后苦掘，就有這個能力去幫別人審計合約，就可以去接這塊業(yè)務(wù)了⌒ㄈ溃現(xiàn)在的智能合約本質(zhì)上都不存在規(guī)范鹤啡。ERC20、ERC721 這些標(biāo)準(zhǔn)都很粗糙蹲嚣。我們手上有形式化驗證的工具递瑰，也會幫去中心化交易所審計上幣的代碼，這樣效率會比較高隙畜。

我們發(fā)現(xiàn)規(guī)范性這個問題是很嚴(yán)重的抖部。太多的智能合約缺少規(guī)范，因此很容易產(chǎn)生很多兼容性問題议惰。比如我們都知道 ERC20 里有一個變量叫 symbol慎颗，是用來表示代幣的名字，是叫“比特幣”還是“以太幣”言询。這個 symbol 的字母大小寫完全是混亂的哗总，因為它沒有具體的規(guī)范，規(guī)定必須怎么寫倍试。再比如函數(shù)執(zhí)行失敗要不要return false讯屈，還是不return？這里也有很多東西沒寫清楚县习。因為沒寫清楚涮母，大家就各做各的，導(dǎo)致最終的接口不一致躁愿。于是很多合約充值就會有漏洞叛本。

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

13

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

區(qū)塊鏈公司跟很多傳統(tǒng)公司不一樣绑榴。傳統(tǒng)公司一定要做大，要把很多業(yè)務(wù)進行整合盈魁，因為只有整合才能發(fā)揮優(yōu)勢翔怎。就像 BAT，每家都做外賣备埃，每家都做支付姓惑，什么業(yè)務(wù)都有褐奴。歸根到底按脚，它只有把自己整合起來變成怪獸才能勝出。

但區(qū)塊鏈行業(yè)反而是敦冬，做好自己最擅長的事情就是最好的辅搬。因為區(qū)塊鏈本來就是用來解決生產(chǎn)關(guān)系的。傳統(tǒng)公司需要有一個老板發(fā)號施令讓員工往同一個方向走脖旱。區(qū)塊鏈行業(yè)是發(fā)現(xiàn)一個規(guī)律能掙錢堪遂，那大家就會自發(fā)往那走。

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

就像現(xiàn)在的幣圈，它不是一個公司巍虫，就是一個小圈子彭则，組織形式非常松散，但又有一致的利益綁定占遥。這種運作方式遠(yuǎn)比一個公司的效率來得高俯抖。為什么區(qū)塊鏈行業(yè)發(fā)展速度都很快也是因為這個原因。沒有老板瓦胎，三人成軍芬萍。發(fā)展非常靈活尤揣。所以我認(rèn)為，區(qū)塊鏈公司不一定需要做大担忧。

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

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

14

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

現(xiàn)階段我們看到的大部分的漏洞是底層的漏洞酌媒，比如各種溢出。這是因為現(xiàn)在大家還不了解區(qū)塊鏈技術(shù)迄靠，行業(yè)里的程序員沒有經(jīng)過行業(yè)的教育秒咨。但未來大家會變得越來越聰明，底層非常低級的安全漏洞會越來越少掌挚。

而上層業(yè)務(wù)會隨著整個行業(yè)的發(fā)展變得越來越復(fù)雜雨席，可能出現(xiàn)的漏洞也會越來越多。代碼的行數(shù)在變大吠式，智能合約的數(shù)量也在增加陡厘。而業(yè)務(wù)漏洞是安全審計公司做不來的，工具也做不到自動化檢查奇徒。因為工具無法理解高層的業(yè)務(wù)意圖雏亚，傳統(tǒng)的安全公司也沒辦法解決這個問題。沒有完善的工具摩钙，配套人才非常稀缺罢低。因此，區(qū)塊鏈安全是一片藍海。

今年 9 月初网持，我會在一個學(xué)術(shù)會議上做報告宜岛，給高校的人講「什么是智能合約」。他們很多都沒聽說過智能合約功舀，但一旦他們聽說了萍倡，很多人可能就會進來這個行業(yè)。因為這些做形式化驗證研究的老師辟汰，他們會很敏感地察覺到列敲，智能合約是一個大金礦。現(xiàn)在還沒有多少人在挖帖汞。我可能不需要跟他們講具體怎么在智能合約上做形式化驗證戴而，只需要給他們講智能合約現(xiàn)在面臨哪些問題，他們就能意識到這一點翩蘸。因此所意，很多高校類的老師出來創(chuàng)業(yè)，這可能也會成為區(qū)塊鏈的一個趨勢催首。

橙皮書 X SECBIT 福利

能讀完文章的都是真愛扶踊。如果你希望了解更多關(guān)于「形式化驗證」與「區(qū)塊鏈安全」的秘密，這里有一條綠色通道：轉(zhuǎn)發(fā)這篇文章到朋友圈并配上文中最打動你的一段話郎任，截屏發(fā)給橙皮書的小姐姐（微信號18519507233）秧耗，她會把你加入到?SECBIT 區(qū)塊鏈愛好者的群里，本文講述人郭宇和 SECBIT 創(chuàng)始團隊會不定期在群里分享最新關(guān)于區(qū)塊鏈安全的信息與心得涝滴。如果你需要購買 SECBIT 的安全服務(wù)（比如合約安全審計）绣版，操作方法同上胶台，小姐姐會送你一份橙皮書用戶專享的八折優(yōu)惠歼疮。