從誕生至今，形式化驗(yàn)證（Formal Verification）方法一直與“小眾、冷門(mén)”等字眼掛鉤。有人說(shuō)形式化驗(yàn)證方法是一種“軍用級(jí)別”的防黑客手段，更是為這項(xiàng)技術(shù)增添了一絲神秘感。
究竟什么是形式化驗(yàn)證方法？
維基百科對(duì)形式化驗(yàn)證的解釋是這樣的：?
在計(jì)算機(jī)硬件（特別是集成電路）和軟件系統(tǒng)的設(shè)計(jì)過(guò)程中，形式化驗(yàn)證的含義是根據(jù)某個(gè)或某些形式化規(guī)范或?qū)傩裕褂?/i>數(shù)學(xué)的方法證明其正確性或非正確性。
神秘感大抵來(lái)源于定義中的兩個(gè)嚴(yán)謹(jǐn)而且抽象的關(guān)鍵詞——“形式化規(guī)范”和“數(shù)學(xué)方法證明”。事實(shí)上，揭開(kāi)這層神秘的面紗，你會(huì)發(fā)現(xiàn)形式化驗(yàn)證的許多有趣之處。
下面這篇文章想要討論的問(wèn)題是：在現(xiàn)階段，以下哪個(gè)故事能夠真正滿(mǎn)足你對(duì)形式化驗(yàn)證的想象？形式化驗(yàn)證真的可以作為一種技術(shù)在區(qū)塊鏈領(lǐng)域流行起來(lái)嗎？如果可以，怎樣才能做到？
（PS：上文中提到的“形式化規(guī)范”的概念，在下文中也會(huì)講到。）
要回答上面這些問(wèn)題，我們可以先思考另一個(gè)更簡(jiǎn)單的問(wèn)題：
現(xiàn)階段，人們使用形式化方法來(lái)做什么？
這個(gè)問(wèn)題的答案無(wú)非有兩種：
1、? 規(guī)避錯(cuò)誤
2、? 對(duì)抗攻擊
| 規(guī)避錯(cuò)誤
規(guī)避錯(cuò)誤其實(shí)就是避免損失。
我們首先來(lái)探討一下，哪些領(lǐng)域?qū)Τ绦蝈e(cuò)誤是零容忍的？在哪些領(lǐng)域，程序錯(cuò)誤帶來(lái)的損失難以估量？
實(shí)際上，形式化方法是從硬件設(shè)計(jì)開(kāi)始普及的。一個(gè)著名的例子是：當(dāng)年Intel的Pentium CPU浮點(diǎn)運(yùn)算單元出錯(cuò)(FDIV Bug)，數(shù)以萬(wàn)計(jì)的CPU不得不回收和替換，給Intel造成了巨大損失(475M$)[1]。
從那之后，Intel開(kāi)始在其芯片設(shè)計(jì)中廣泛采用形式化方法。
計(jì)算機(jī)硬件巨頭如IBM，AMD， NVIDIA 和 CADENCE[2]等等也都是形式化方法的使用者…
要說(shuō)起吃一塹才能長(zhǎng)一智，其實(shí)各行各業(yè)都有試錯(cuò)者，在工業(yè)界也是如此。舉個(gè)例子：1996年，歐洲航天局首次發(fā)射的阿麗亞娜5型（Ariane 5）火箭，由于慣性導(dǎo)航系統(tǒng)發(fā)送的錯(cuò)誤指令（浮點(diǎn)數(shù)轉(zhuǎn)換為整數(shù)造成溢出），導(dǎo)致火箭在發(fā)射僅僅37秒后便偏離了預(yù)定軌道，最終墜毀。歐洲航天局的巨額研發(fā)經(jīng)費(fèi)（8B $）[3]付之一炬。
在那之后不久，EADS公司開(kāi)發(fā)阿麗亞娜火箭的任務(wù)調(diào)度模型就開(kāi)始使用形式化方法。
美國(guó)國(guó)家宇航局NASA和英國(guó)國(guó)防部在90年代相繼發(fā)布設(shè)計(jì)標(biāo)準(zhǔn)[4]，形式化方法的使用位列其中。我國(guó)的玉兔號(hào)月球車(chē)控制系統(tǒng)和我國(guó)第一個(gè)自主研發(fā)的空間飛行器嵌入式實(shí)時(shí)操作系統(tǒng)SpaceOS[5]，也都是通過(guò)形式化方法驗(yàn)證其正確性。
歷史的發(fā)展告訴我們，金錢(qián)才是推動(dòng)社會(huì)發(fā)展的第一動(dòng)力！程序錯(cuò)誤帶來(lái)的巨額損失，任誰(shuí)也只能?chē)@一聲傷不起。
如果說(shuō)上面兩個(gè)故事聽(tīng)起來(lái)都過(guò)分沉重了，我們不妨看一下下面這張圖：
上圖顯示了全球范圍內(nèi)用形式化方法開(kāi)發(fā)的地鐵項(xiàng)目分布情況。[6]
可以看出，由巴黎地鐵信號(hào)系統(tǒng)開(kāi)始，在北美、歐洲、亞洲的主要國(guó)家，以及南美洲的部分國(guó)家的地鐵系統(tǒng)開(kāi)發(fā)中，形式化方法已經(jīng)被廣泛使用了。這或許是我們幾乎從未聽(tīng)過(guò)由于地鐵系統(tǒng)故障而造成重大損失和災(zāi)難的原因。
還是那句話(huà)，金錢(qián)是第一生產(chǎn)力。
既然形式化方法在保障日常出行方面做出的貢獻(xiàn)已經(jīng)得到廣泛的認(rèn)可，那么，在依托區(qū)塊鏈技術(shù)而發(fā)展起來(lái)的數(shù)字資產(chǎn)領(lǐng)域，通過(guò)形式化驗(yàn)證技術(shù)來(lái)保障智能合約安全性、進(jìn)而保障財(cái)產(chǎn)安全性的理念就顯得合理甚至緊迫了。
具體需要怎么做？這里簡(jiǎn)單介紹一下。
首先需要引入一個(gè)“形式化規(guī)范”的概念了。
形式化規(guī)范? (formal specification)是指通過(guò)數(shù)學(xué)語(yǔ)言對(duì)系統(tǒng)的預(yù)期行為 (例如將數(shù)量 S 的 token 從賬戶(hù) A 轉(zhuǎn)移到賬戶(hù) B) 和性質(zhì) (例如轉(zhuǎn)賬不會(huì)造成賬戶(hù) B 額度的溢出) 進(jìn)行嚴(yán)格和全面的定義。形式化規(guī)范往往定義了系統(tǒng)的正確性和安全性
給定一個(gè)系統(tǒng)的形式化規(guī)范，我們即可以從規(guī)范出發(fā)開(kāi)始迭代設(shè)計(jì)和實(shí)現(xiàn)出這個(gè)系統(tǒng)。在迭代的每一步中，我們可以通過(guò)精化 (refinement)、集成 (synthesis) 、形式化證明在內(nèi)的一系列方法在數(shù)學(xué)上嚴(yán)格的保證迭代產(chǎn)生的系統(tǒng)和迭代前的規(guī)范或者系統(tǒng)保持一致。
除了從形式化規(guī)范出發(fā)設(shè)計(jì)和實(shí)現(xiàn)一個(gè)系統(tǒng)，我們也可以使用包括符號(hào)執(zhí)行 (symbolic execution)、模型檢測(cè) (model check) 和形式化證明 (formal proving) 在內(nèi)的一系列方法驗(yàn)證已有的設(shè)計(jì)和實(shí)現(xiàn)與該規(guī)范保持一致。
聽(tīng)起來(lái)很高大上，對(duì)不對(duì)？
舉個(gè)例子來(lái)說(shuō)，對(duì)于一段智能合約程序，我們可以從它所有可能的輸入 (例如函數(shù)參數(shù)的組合) 和初始狀態(tài) (例如狀態(tài)變量初始值的組合) 出發(fā)，根據(jù)每條語(yǔ)句的語(yǔ)義，逐句推導(dǎo)出程序的所有可能的結(jié)束狀態(tài) (例如合約執(zhí)行結(jié)束后的狀態(tài)變量的值和產(chǎn)生的 event log)，并檢查合約的所有輸入、初始狀態(tài)、結(jié)束狀態(tài)的組合是否都和形式化規(guī)范保持一致。這有點(diǎn)類(lèi)似于柯南破案那樣，一步步地推演。只不過(guò)，這里所有的定義都是通過(guò)嚴(yán)格的數(shù)學(xué)語(yǔ)言描述，推導(dǎo)和檢查也是嚴(yán)格的數(shù)學(xué)推導(dǎo)和證明。根據(jù)待驗(yàn)證的系統(tǒng)及其形式化規(guī)范的復(fù)雜程度，推導(dǎo)和證明即可以手工構(gòu)造，也可能可以由機(jī)器自動(dòng)產(chǎn)生。
在實(shí)踐中，推導(dǎo)和證明無(wú)法進(jìn)行下去往往意味著設(shè)計(jì)和實(shí)現(xiàn)中存在不符合規(guī)范的 bug。通過(guò)分析推導(dǎo)和證明卡殼的位置和原因，可以定位出 bug 在設(shè)計(jì)和實(shí)現(xiàn)中的具體位置和成因。這樣的方法，讓數(shù)字資產(chǎn)領(lǐng)域中中嚴(yán)格意義上的規(guī)避錯(cuò)誤、避免損失成為可能。
| 對(duì)抗攻擊
對(duì)抗攻擊其實(shí)是另一種意義上的避免損失。
故事從美國(guó)軍方的一次電子攻擊說(shuō)起。2015年夏天，一起黑客奉命對(duì)美國(guó)軍方Little Bird無(wú)人直升機(jī)發(fā)動(dòng)電子攻擊，并掌握無(wú)人機(jī)控制權(quán)的事件中，黑客最初的攻擊十分順利，如入無(wú)人之境。然而，當(dāng)美國(guó)國(guó)防部重新開(kāi)發(fā)了該無(wú)人機(jī)的核心控制程序后，黑客們使用了當(dāng)今世界上所有的攻擊手段，都未能攻破新部署的系統(tǒng)。[7]
到底是什么技術(shù)給予了Little Bird超強(qiáng)的防御能力，從而使它阻擋了所有的攻擊？答案就是：形式化驗(yàn)證方法。
形式化驗(yàn)證方法通過(guò)嚴(yán)格的數(shù)學(xué)證明保證程序行為與預(yù)期一致，但形式化驗(yàn)證程序的正確性非常消耗人力，所以，與程序測(cè)試等通用技術(shù)不同的是，形式化驗(yàn)證方法常常只被應(yīng)用于安全攸關(guān)領(lǐng)域，如無(wú)人機(jī)、航天器、操作系統(tǒng)等的程序正確性驗(yàn)證。
這里不得不提的是2016 年發(fā)現(xiàn)的一個(gè)非常嚴(yán)重的 linux 操作系統(tǒng)內(nèi)核漏洞Dirty Cow (CVE-2016-5195)[8]，攻擊者可以通過(guò)這個(gè)漏洞獲得系統(tǒng)最高權(quán)限，從而使系統(tǒng)全部處于可被利用的狀態(tài)之下。
在操作系統(tǒng)領(lǐng)域，一些人身先士卒，嘗試用形式化方法避免安全攸關(guān)領(lǐng)域中的系統(tǒng)漏洞和黑客攻擊。耶魯大學(xué)邵中老師團(tuán)隊(duì)通過(guò)模塊分層驗(yàn)證法(modular layered verification methods)成功研發(fā)了安全性和可靠性極高的計(jì)算機(jī)操作系統(tǒng)CertiKOS[9]; 中科大軟件安全實(shí)驗(yàn)室馮新宇老師團(tuán)隊(duì)也提出了一個(gè)針對(duì)搶占式多任務(wù)操作系統(tǒng)內(nèi)核的形式化驗(yàn)證框架，并成功的應(yīng)用在對(duì)嵌入式操作系統(tǒng) uC/OS-II （該操作系統(tǒng)被廣泛應(yīng)用于航空電子產(chǎn)品中）的驗(yàn)證中[10]。
| 安全攸關(guān)的區(qū)塊鏈領(lǐng)域
區(qū)塊鏈領(lǐng)域亦然，一方面，小錯(cuò)誤也會(huì)導(dǎo)致大損失；另一方面，巨大的經(jīng)濟(jì)利益也會(huì)吸引大量的攻擊者。
以太坊黑客攻擊第一大案The DAO中，攻擊者竊取了當(dāng)時(shí)價(jià)值5500萬(wàn)美元的以太幣，并且導(dǎo)致了以太坊的硬分叉[11]；這之后，與以太坊智能合約相關(guān)的攻擊一直在繼續(xù)——比如，2017年11月，以太坊Parity錢(qián)包由于被黑客攻擊，導(dǎo)致用戶(hù)損失了價(jià)值約為1.5億美元的數(shù)字資產(chǎn)[11]。
據(jù)安比實(shí)驗(yàn)室統(tǒng)計(jì)，僅2018年上半年，就已經(jīng)有大約11億美元的數(shù)字資產(chǎn)被盜，與區(qū)塊鏈系統(tǒng)相關(guān)的漏洞（如以太坊中的智能合約漏洞）以及圍繞數(shù)字資產(chǎn)的生態(tài)系統(tǒng)安全問(wèn)題（如多個(gè)中心化交易所被盜）更是層出不窮。
目前區(qū)塊鏈系統(tǒng)中的相關(guān)漏洞，以及數(shù)字資產(chǎn)生態(tài)系統(tǒng)的安全問(wèn)題，歸根結(jié)底是相關(guān)程序設(shè)計(jì)與實(shí)現(xiàn)的問(wèn)題。在形式化方法以前，這類(lèi)問(wèn)題多是通過(guò)程序測(cè)試來(lái)發(fā)現(xiàn)的。
形式化驗(yàn)證進(jìn)入?yún)^(qū)塊鏈領(lǐng)域的初期，以太坊社區(qū)的Yoichi Hirai對(duì)以太坊（Ethereum）的智能合約虛擬機(jī)EVM做了完整的形式化建模。此外，來(lái)自UIUC大學(xué)的團(tuán)隊(duì)也對(duì)EVM進(jìn)行了形式化的建模和驗(yàn)證[12]。EVM是以太坊智能合約的底層核心，關(guān)系到以太坊安全，涉及到數(shù)字資產(chǎn)保護(hù)等重大議題，引起了社區(qū)的廣泛關(guān)注。
此外，MakerDAO項(xiàng)目方發(fā)布了第一個(gè)經(jīng)過(guò)形式化驗(yàn)證的去中心化應(yīng)用程序（DApp）[13]。MakerDAO 是一個(gè)基于以太坊的智能合約平臺(tái)，該平臺(tái)提供了穩(wěn)定幣（stablecoin），抵押貸款（collateral loans），以及去中心化社區(qū)治理功能。為了保證所部署的智能合約的安全性，MakerDAO團(tuán)隊(duì)對(duì)抵押貸款（CDP）核心引擎合約代碼通過(guò)K-Framewok進(jìn)行了驗(yàn)證，因此而表明其智能合約程序能夠完全抵抗黑客攻擊。
安比實(shí)驗(yàn)室也在以太坊智能合約形式化驗(yàn)證方面做了大量的工作，提出了一個(gè)智能合約形式化驗(yàn)證框架，并在該框架內(nèi)證明了一些常見(jiàn)的Token合約，比如ERC20，ERC721等（其中包含轉(zhuǎn)賬、Token總量等通用性功能）。這些被數(shù)學(xué)證明過(guò)的智能合約可以直接使用，不再需要擔(dān)心安全問(wèn)題。這些合約源代碼和證明過(guò)程已經(jīng)以開(kāi)源[14]的方式貢獻(xiàn)給社區(qū)。
Github社區(qū)地址：
https://github.com/sec-bit/tokenlibs-with-proofs
| 結(jié)論
大多數(shù)人認(rèn)為形式化驗(yàn)證方法高深莫測(cè)，究其原因，形式化驗(yàn)證方法不是一種通用技術(shù)，而是需要和領(lǐng)域結(jié)合來(lái)發(fā)揮價(jià)值的一種特定技術(shù)。在區(qū)塊鏈領(lǐng)域，形式化方法究竟是一種nice to have還是一種must have，也是與項(xiàng)目特點(diǎn)密不可分的。
隨著區(qū)塊鏈技術(shù)與項(xiàng)目應(yīng)用的探索不斷深入，項(xiàng)目方對(duì)于規(guī)避錯(cuò)誤、對(duì)抗黑客攻擊和避免財(cái)產(chǎn)損失的需求已經(jīng)越來(lái)越強(qiáng)。
當(dāng)互聯(lián)網(wǎng)世界中的絕大部分活動(dòng)都完成上鏈，當(dāng)社會(huì)中的絕大部分群體都需要區(qū)塊鏈的絕對(duì)安全來(lái)保護(hù)自己的財(cái)產(chǎn)安全的時(shí)候，形式化驗(yàn)證方法作為區(qū)塊鏈技術(shù)的must have才會(huì)迎來(lái)大爆發(fā)。
文末福利| 關(guān)于Verification與Testing的糾葛，你了解多少？
最后來(lái)談一下形式化驗(yàn)證（Formal Verification）與程序測(cè)試（Testing）之間的關(guān)系。
“程序測(cè)試能證明錯(cuò)誤的存在,但不能證明錯(cuò)誤不存在”。Edsger Dijkstra（1972年圖靈獎(jiǎng)獲得者、形式化方法核心思想的提出者）如此評(píng)述。
在實(shí)踐中，尤其是在代碼足夠復(fù)雜的場(chǎng)景中，形式化驗(yàn)證（Verification）與程序測(cè)試方法（Testing） 的驗(yàn)證效果有如云泥之別。
舉個(gè)例子來(lái)說(shuō)：2009年，澳大利亞的科學(xué)家使用形式化方法對(duì)工業(yè)級(jí)操作系統(tǒng)seL4微內(nèi)核進(jìn)行了完整功能性驗(yàn)證[15]，驗(yàn)證方式同時(shí)以形式化驗(yàn)證和程序測(cè)試兩種方式分別展開(kāi)，驗(yàn)證的結(jié)果是：形式化方法共發(fā)現(xiàn)460多個(gè)Bug，而程序測(cè)試只發(fā)現(xiàn)了16個(gè)Bug。
更有趣的是，在以高驗(yàn)證成本著稱(chēng)的形式化驗(yàn)證領(lǐng)域，完全驗(yàn)證seL4微內(nèi)核只需要600萬(wàn)美元的驗(yàn)證成本，而以測(cè)試的方式通過(guò)CC EAL6級(jí)認(rèn)證的成本竟高達(dá)8700萬(wàn)美元[15]。
由此可見(jiàn)，通過(guò)形式化驗(yàn)證可以更經(jīng)濟(jì)的為seL4微內(nèi)核提供更強(qiáng)的安全性保證。
當(dāng)然，有人說(shuō)，程序測(cè)試是在“真實(shí)”環(huán)境里進(jìn)行的，形式化驗(yàn)證只是數(shù)學(xué)層面，在“真實(shí)”環(huán)境中的測(cè)試是形式化驗(yàn)證無(wú)法取代的。從這個(gè)角度來(lái)說(shuō)，形式化驗(yàn)證與程序測(cè)試如何做到共生互補(bǔ)？讓這項(xiàng)技術(shù)在區(qū)塊鏈領(lǐng)域真正流行起來(lái)，可能就是鏈圈同仁們接下來(lái)要共同探索的方向了。
參考文獻(xiàn)
【1】History of Formal Verification at Intel
https://dac.com/blog/post/history-formal-verification-intel
【2】王?。赫f(shuō)說(shuō)形式化驗(yàn)證（Formal Verification）吧
http://chainb.com/?P=Cont&id=1957
【3】Modeling and Validation of a Software Architecture for the Ariane-5Launcher
https://link.springer.com/chapter/10.1007/11768869_6
【4】Tenth NASA Formal Methods Symposium https://shemesh.larc.nasa.gov/NFM2018/
【5】玉兔使用的國(guó)產(chǎn)SpaceOS操作系統(tǒng)未來(lái)有望衍生出民用版本
http://blog.sina.com.cn/s/blog_ae55841d0101hemg.html
【6】Cimatti, A., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T.,Roveri, M., Sanseviero, A. and Tchaltsev, A., 2012, July. Formal verificationand validation of ERTMS industrial railway train spacing system. InInternational Conference on Computer Aided Verification (pp. 378-393).Springer, Berlin, Heidelberg.
【7】COMPUTER SCIENTISTS CLOSE IN ON PERFECT, HACK-PROOF CODEhttps://www.wired.com/2016/09/computer-scientists-close-perfect-hack-proof-code/
【8】利用Dirty Cow實(shí)現(xiàn)docker逃逸
https://www.anquanke.com/post/id/84866
【9】CertiKOS: Yale develops world's first hacker-resistant operatingsystem
【10】Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang andZhaohui Li. A Practical Verification Framework for Preemptive OS Kernels. Proc.28th International Conference on Computer Aided Verification (CAV'16)
【11】從技術(shù)角度剖析針對(duì)THE DAO的攻擊手法
https://www.8btc.com/article/93713
https://github.com/kframework/evm-semantics
【13】風(fēng)投巨頭 A16Z 投資穩(wěn)定幣項(xiàng)目MakerDAO
https://www.jinse.com/bitcoin/246582.html
【14】構(gòu)造形式化證明，解決智能合約安全問(wèn)題——你的合約亟待證明
https://mp.weixin.qq.com/s/xUNKT8v9ikEYFnuMWzvXdg
【15】Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick,David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski,Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4:formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22ndsymposium on Operating systems principles (SOSP '09).
