從誕生至今，形式化驗(yàn)證（Formal Verification）方法一直與“小眾狮鸭、冷門”等字眼掛鉤合搅。有人說形式化驗(yàn)證方法是一種“軍用級(jí)別”的防黑客手段，更是為這項(xiàng)技術(shù)增添了一絲神秘感歧蕉。
究竟什么是形式化驗(yàn)證方法灾部？
維基百科對形式化驗(yàn)證的解釋是這樣的：?
在計(jì)算機(jī)硬件（特別是集成電路）和軟件系統(tǒng)的設(shè)計(jì)過程中，形式化驗(yàn)證的含義是根據(jù)某個(gè)或某些形式化規(guī)范或?qū)傩怨咄耍褂?/i>數(shù)學(xué)的方法證明其正確性或非正確性赌髓。
神秘感大抵來源于定義中的兩個(gè)嚴(yán)謹(jǐn)而且抽象的關(guān)鍵詞——“形式化規(guī)范”和“數(shù)學(xué)方法證明”。事實(shí)上，揭開這層神秘的面紗春弥，你會(huì)發(fā)現(xiàn)形式化驗(yàn)證的許多有趣之處。
下面這篇文章想要討論的問題是：在現(xiàn)階段叠荠，以下哪個(gè)故事能夠真正滿足你對形式化驗(yàn)證的想象匿沛？形式化驗(yàn)證真的可以作為一種技術(shù)在區(qū)塊鏈領(lǐng)域流行起來嗎？如果可以榛鼎，怎樣才能做到逃呼？
（PS：上文中提到的“形式化規(guī)范”的概念，在下文中也會(huì)講到者娱。）
要回答上面這些問題抡笼，我們可以先思考另一個(gè)更簡單的問題：
現(xiàn)階段，人們使用形式化方法來做什么黄鳍？
這個(gè)問題的答案無非有兩種：
1推姻、? 規(guī)避錯(cuò)誤
2、? 對抗攻擊
| 規(guī)避錯(cuò)誤
規(guī)避錯(cuò)誤其實(shí)就是避免損失框沟。
我們首先來探討一下藏古，哪些領(lǐng)域?qū)Τ绦蝈e(cuò)誤是零容忍的？在哪些領(lǐng)域忍燥，程序錯(cuò)誤帶來的損失難以估量拧晕？
實(shí)際上，形式化方法是從硬件設(shè)計(jì)開始普及的梅垄。一個(gè)著名的例子是：當(dāng)年Intel的Pentium CPU浮點(diǎn)運(yùn)算單元出錯(cuò)(FDIV Bug)厂捞，數(shù)以萬計(jì)的CPU不得不回收和替換，給Intel造成了巨大損失(475M$)[1]队丝。
從那之后靡馁，Intel開始在其芯片設(shè)計(jì)中廣泛采用形式化方法。
計(jì)算機(jī)硬件巨頭如IBM炭玫，AMD奈嘿， NVIDIA 和 CADENCE[2]等等也都是形式化方法的使用者…
要說起吃一塹才能長一智，其實(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公司開發(fā)阿麗亞娜火箭的任務(wù)調(diào)度模型就開始使用形式化方法。
美國國家宇航局NASA和英國國防部在90年代相繼發(fā)布設(shè)計(jì)標(biāo)準(zhǔn)[4]德崭，形式化方法的使用位列其中斥黑。我國的玉兔號(hào)月球車控制系統(tǒng)和我國第一個(gè)自主研發(fā)的空間飛行器嵌入式實(shí)時(shí)操作系統(tǒng)SpaceOS[5]，也都是通過形式化方法驗(yàn)證其正確性眉厨。
歷史的發(fā)展告訴我們锌奴，金錢才是推動(dòng)社會(huì)發(fā)展的第一動(dòng)力！程序錯(cuò)誤帶來的巨額損失憾股，任誰也只能嘆一聲傷不起鹿蜀。
如果說上面兩個(gè)故事聽起來都過分沉重了，我們不妨看一下下面這張圖：
上圖顯示了全球范圍內(nèi)用形式化方法開發(fā)的地鐵項(xiàng)目分布情況服球。[6]
可以看出茴恰，由巴黎地鐵信號(hào)系統(tǒng)開始，在北美斩熊、歐洲往枣、亞洲的主要國家，以及南美洲的部分國家的地鐵系統(tǒng)開發(fā)中粉渠，形式化方法已經(jīng)被廣泛使用了婉商。這或許是我們幾乎從未聽過由于地鐵系統(tǒng)故障而造成重大損失和災(zāi)難的原因。
還是那句話渣叛，金錢是第一生產(chǎn)力丈秩。
既然形式化方法在保障日常出行方面做出的貢獻(xiàn)已經(jīng)得到廣泛的認(rèn)可，那么淳衙，在依托區(qū)塊鏈技術(shù)而發(fā)展起來的數(shù)字資產(chǎn)領(lǐng)域蘑秽，通過形式化驗(yàn)證技術(shù)來保障智能合約安全性、進(jìn)而保障財(cái)產(chǎn)安全性的理念就顯得合理甚至緊迫了箫攀。
具體需要怎么做肠牲？這里簡單介紹一下。
首先需要引入一個(gè)“形式化規(guī)范”的概念了靴跛。
形式化規(guī)范? (formal specification)是指通過數(shù)學(xué)語言對系統(tǒng)的預(yù)期行為 (例如將數(shù)量 S 的 token 從賬戶 A 轉(zhuǎn)移到賬戶 B) 和性質(zhì) (例如轉(zhuǎn)賬不會(huì)造成賬戶 B 額度的溢出) 進(jìn)行嚴(yán)格和全面的定義缀雳。形式化規(guī)范往往定義了系統(tǒng)的正確性和安全性
給定一個(gè)系統(tǒng)的形式化規(guī)范，我們即可以從規(guī)范出發(fā)開始迭代設(shè)計(jì)和實(shí)現(xiàn)出這個(gè)系統(tǒng)梢睛。在迭代的每一步中肥印，我們可以通過精化 (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)藏畅、模型檢測 (model check) 和形式化證明 (formal proving) 在內(nèi)的一系列方法驗(yàn)證已有的設(shè)計(jì)和實(shí)現(xiàn)與該規(guī)范保持一致敷硅。
聽起來很高大上，對不對？
舉個(gè)例子來說绞蹦，對于一段智能合約程序力奋，我們可以從它所有可能的輸入 (例如函數(shù)參數(shù)的組合) 和初始狀態(tài) (例如狀態(tài)變量初始值的組合) 出發(fā)，根據(jù)每條語句的語義幽七，逐句推導(dǎo)出程序的所有可能的結(jié)束狀態(tài) (例如合約執(zhí)行結(jié)束后的狀態(tài)變量的值和產(chǎn)生的 event log)刊侯，并檢查合約的所有輸入、初始狀態(tài)锉走、結(jié)束狀態(tài)的組合是否都和形式化規(guī)范保持一致。這有點(diǎn)類似于柯南破案那樣藕届，一步步地推演挪蹭。只不過，這里所有的定義都是通過嚴(yán)格的數(shù)學(xué)語言描述休偶，推導(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)和證明無法進(jìn)行下去往往意味著設(shè)計(jì)和實(shí)現(xiàn)中存在不符合規(guī)范的 bug碱妆。通過分析推導(dǎo)和證明卡殼的位置和原因肉盹，可以定位出 bug 在設(shè)計(jì)和實(shí)現(xiàn)中的具體位置和成因。這樣的方法疹尾，讓數(shù)字資產(chǎn)領(lǐng)域中中嚴(yán)格意義上的規(guī)避錯(cuò)誤上忍、避免損失成為可能。
| 對抗攻擊
對抗攻擊其實(shí)是另一種意義上的避免損失纳本。
故事從美國軍方的一次電子攻擊說起窍蓝。2015年夏天，一起黑客奉命對美國軍方Little Bird無人直升機(jī)發(fā)動(dòng)電子攻擊繁成，并掌握無人機(jī)控制權(quán)的事件中吓笙，黑客最初的攻擊十分順利，如入無人之境巾腕。然而面睛，當(dāng)美國國防部重新開發(fā)了該無人機(jī)的核心控制程序后，黑客們使用了當(dāng)今世界上所有的攻擊手段尊搬，都未能攻破新部署的系統(tǒng)侮穿。[7]
到底是什么技術(shù)給予了Little Bird超強(qiáng)的防御能力，從而使它阻擋了所有的攻擊毁嗦？答案就是：形式化驗(yàn)證方法亲茅。
形式化驗(yàn)證方法通過嚴(yán)格的數(shù)學(xué)證明保證程序行為與預(yù)期一致，但形式化驗(yàn)證程序的正確性非常消耗人力，所以克锣，與程序測試等通用技術(shù)不同的是茵肃，形式化驗(yàn)證方法常常只被應(yīng)用于安全攸關(guān)領(lǐng)域，如無人機(jī)袭祟、航天器验残、操作系統(tǒng)等的程序正確性驗(yàn)證。
這里不得不提的是2016 年發(fā)現(xiàn)的一個(gè)非常嚴(yán)重的 linux 操作系統(tǒng)內(nèi)核漏洞Dirty Cow (CVE-2016-5195)[8]巾乳，攻擊者可以通過這個(gè)漏洞獲得系統(tǒng)最高權(quán)限您没，從而使系統(tǒng)全部處于可被利用的狀態(tài)之下。
在操作系統(tǒng)領(lǐng)域胆绊，一些人身先士卒氨鹏，嘗試用形式化方法避免安全攸關(guān)領(lǐng)域中的系統(tǒng)漏洞和黑客攻擊。耶魯大學(xué)邵中老師團(tuán)隊(duì)通過模塊分層驗(yàn)證法(modular layered verification methods)成功研發(fā)了安全性和可靠性極高的計(jì)算機(jī)操作系統(tǒng)CertiKOS[9]; 中科大軟件安全實(shí)驗(yàn)室馮新宇老師團(tuán)隊(duì)也提出了一個(gè)針對搶占式多任務(wù)操作系統(tǒng)內(nèi)核的形式化驗(yàn)證框架压状，并成功的應(yīng)用在對嵌入式操作系統(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萬美元的以太幣，并且導(dǎo)致了以太坊的硬分叉[11]十兢；這之后慨蛙，與以太坊智能合約相關(guān)的攻擊一直在繼續(xù)——比如，2017年11月纪挎，以太坊Parity錢包由于被黑客攻擊期贫，導(dǎo)致用戶損失了價(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)安全問題（如多個(gè)中心化交易所被盜）更是層出不窮烤蜕。
目前區(qū)塊鏈系統(tǒng)中的相關(guān)漏洞封孙，以及數(shù)字資產(chǎn)生態(tài)系統(tǒng)的安全問題，歸根結(jié)底是相關(guān)程序設(shè)計(jì)與實(shí)現(xiàn)的問題讽营。在形式化方法以前虎忌，這類問題多是通過程序測試來發(fā)現(xiàn)的。
形式化驗(yàn)證進(jìn)入?yún)^(qū)塊鏈領(lǐng)域的初期橱鹏，以太坊社區(qū)的Yoichi Hirai對以太坊（Ethereum）的智能合約虛擬機(jī)EVM做了完整的形式化建模膜蠢。此外堪藐，來自UIUC大學(xué)的團(tuán)隊(duì)也對EVM進(jìn)行了形式化的建模和驗(yàn)證[12]。EVM是以太坊智能合約的底層核心挑围，關(guān)系到以太坊安全礁竞，涉及到數(shù)字資產(chǎn)保護(hù)等重大議題，引起了社區(qū)的廣泛關(guān)注杉辙。
此外模捂，MakerDAO項(xiàng)目方發(fā)布了第一個(gè)經(jīng)過形式化驗(yàn)證的去中心化應(yīng)用程序（DApp）[13]。MakerDAO 是一個(gè)基于以太坊的智能合約平臺(tái)蜘矢，該平臺(tái)提供了穩(wěn)定幣（stablecoin）狂男，抵押貸款（collateral loans），以及去中心化社區(qū)治理功能品腹。為了保證所部署的智能合約的安全性岖食，MakerDAO團(tuán)隊(duì)對抵押貸款（CDP）核心引擎合約代碼通過K-Framewok進(jìn)行了驗(yàn)證，因此而表明其智能合約程序能夠完全抵抗黑客攻擊珍昨。
安比實(shí)驗(yàn)室也在以太坊智能合約形式化驗(yàn)證方面做了大量的工作，提出了一個(gè)智能合約形式化驗(yàn)證框架句喷，并在該框架內(nèi)證明了一些常見的Token合約镣典，比如ERC20，ERC721等（其中包含轉(zhuǎn)賬唾琼、Token總量等通用性功能）兄春。這些被數(shù)學(xué)證明過的智能合約可以直接使用，不再需要擔(dān)心安全問題锡溯。這些合約源代碼和證明過程已經(jīng)以開源[14]的方式貢獻(xiàn)給社區(qū)赶舆。
Github社區(qū)地址：
https://github.com/sec-bit/tokenlibs-with-proofs
| 結(jié)論
大多數(shù)人認(rèn)為形式化驗(yàn)證方法高深莫測，究其原因祭饭，形式化驗(yàn)證方法不是一種通用技術(shù)芜茵，而是需要和領(lǐng)域結(jié)合來發(fā)揮價(jià)值的一種特定技術(shù)。在區(qū)塊鏈領(lǐng)域倡蝙，形式化方法究竟是一種nice to have還是一種must have九串，也是與項(xiàng)目特點(diǎn)密不可分的。
隨著區(qū)塊鏈技術(shù)與項(xiàng)目應(yīng)用的探索不斷深入寺鸥，項(xiàng)目方對于規(guī)避錯(cuò)誤猪钮、對抗黑客攻擊和避免財(cái)產(chǎn)損失的需求已經(jīng)越來越強(qiáng)。
當(dāng)互聯(lián)網(wǎng)世界中的絕大部分活動(dòng)都完成上鏈胆建，當(dāng)社會(huì)中的絕大部分群體都需要區(qū)塊鏈的絕對安全來保護(hù)自己的財(cái)產(chǎn)安全的時(shí)候烤低，形式化驗(yàn)證方法作為區(qū)塊鏈技術(shù)的must have才會(huì)迎來大爆發(fā)。
文末福利| 關(guān)于Verification與Testing的糾葛笆载，你了解多少扑馁？
最后來談一下形式化驗(yàn)證（Formal Verification）與程序測試（Testing）之間的關(guān)系涯呻。
“程序測試能證明錯(cuò)誤的存在,但不能證明錯(cuò)誤不存在”。Edsger Dijkstra（1972年圖靈獎(jiǎng)獲得者檐蚜、形式化方法核心思想的提出者）如此評述魄懂。
在實(shí)踐中，尤其是在代碼足夠復(fù)雜的場景中闯第，形式化驗(yàn)證（Verification）與程序測試方法（Testing） 的驗(yàn)證效果有如云泥之別市栗。
舉個(gè)例子來說：2009年，澳大利亞的科學(xué)家使用形式化方法對工業(yè)級(jí)操作系統(tǒng)seL4微內(nèi)核進(jìn)行了完整功能性驗(yàn)證[15]咳短，驗(yàn)證方式同時(shí)以形式化驗(yàn)證和程序測試兩種方式分別展開填帽，驗(yàn)證的結(jié)果是：形式化方法共發(fā)現(xiàn)460多個(gè)Bug，而程序測試只發(fā)現(xiàn)了16個(gè)Bug咙好。
更有趣的是篡腌，在以高驗(yàn)證成本著稱的形式化驗(yàn)證領(lǐng)域，完全驗(yàn)證seL4微內(nèi)核只需要600萬美元的驗(yàn)證成本勾效，而以測試的方式通過CC EAL6級(jí)認(rèn)證的成本竟高達(dá)8700萬美元[15]嘹悼。
由此可見，通過形式化驗(yàn)證可以更經(jīng)濟(jì)的為seL4微內(nèi)核提供更強(qiáng)的安全性保證层宫。
當(dāng)然杨伙，有人說，程序測試是在“真實(shí)”環(huán)境里進(jìn)行的萌腿，形式化驗(yàn)證只是數(shù)學(xué)層面限匣，在“真實(shí)”環(huán)境中的測試是形式化驗(yàn)證無法取代的。從這個(gè)角度來說毁菱，形式化驗(yàn)證與程序測試如何做到共生互補(bǔ)米死？讓這項(xiàng)技術(shù)在區(qū)塊鏈領(lǐng)域真正流行起來，可能就是鏈圈同仁們接下來要共同探索的方向了贮庞。
參考文獻(xiàn)
【1】History of Formal Verification at Intel
https://dac.com/blog/post/history-formal-verification-intel
【2】王铰屯病：說說形式化驗(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】玉兔使用的國產(chǎn)SpaceOS操作系統(tǒng)未來有望衍生出民用版本
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ù)角度剖析針對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)造形式化證明，解決智能合約安全問題——你的合約亟待證明
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).
