從誕生至今，形式化驗證（Formal Verification）方法一直與“小眾、冷門”等字眼掛鉤。有人說形式化驗證方法是一種“軍用級別”的防黑客手段，更是為這項技術增添了一絲神秘感。
究竟什麼是形式化驗證方法？
維基百科對形式化驗證的解釋是這樣的：
在計算機硬件（特別是集成電路）和軟件系統的設計過程中，形式化驗證的含義是根據某個或某些形式化規範或屬性，使用數學的方法證明其正確性或非正確性。
神秘感大抵來源於定義中的兩個嚴謹而且抽象的關鍵詞——“形式化規範”和“數學方法證明”。事實上，揭開這層神秘的面紗，你會發現形式化驗證的許多有趣之處。
下面這篇文章想要討論的問題是：在現階段，以下哪個故事能夠真正滿足你對形式化驗證的想像？形式化驗證真的可以作為一種技術在區塊鏈領域流行起來嗎？如果可以，怎樣才能做到？
（PS：上文中提到的“形式化規範”的概念，在下文中也會講到。）
要回答上面這些問題，我們可以先思考另一個更簡單的問題：
>現階段，人們使用形式化方法來做什麼？
這個問題的答案無非有兩種：
>一級標題
>一級標題
| 規避錯誤
規避錯誤其實就是避免損失。
我們首先來探討一下，哪些領域對程序錯誤是零容忍的？在哪些領域，程序錯誤帶來的損失難以估量？
實際上，形式化方法是從硬件設計開始普及的。一個著名的例子是：當年Intel的Pentium CPU浮點運算單元出錯(FDIV Bug)，數以萬計的CPU不得不回收和替換，給Intel造成了巨大損失(475M $)[1]。
從那之後，Intel開始在其芯片設計中廣泛採用形式化方法。
計算機硬件巨頭如IBM，AMD， NVIDIA 和CADENCE[2]等等也都是形式化方法的使用者…
要說起吃一塹才能長一智，其實各行各業都有試錯者，在工業界也是如此。舉個例子：1996年，歐洲航天局首次發射的阿麗亞娜5型（Ariane 5）火箭，由於慣性導航系統發送的錯誤指令（浮點數轉換為整數造成溢出），導致火箭在發射僅僅37秒後便偏離了預定軌道，最終墜毀。歐洲航天局的巨額研發經費（8B $）[3]付之一炬。
在那之後不久，EADS公司開發阿麗亞娜火箭的任務調度模型就開始使用形式化方法。
美國國家宇航局NASA和英國國防部在90年代相繼發佈設計標準[4]，形式化方法的使用位列其中。我國的玉兔號月球車控制系統和我國第一個自主研發的空間飛行器嵌入式實時操作系統SpaceOS[5]，也都是通過形式化方法驗證其正確性。
歷史的發展告訴我們，金錢才是推動社會發展的第一動力！程序錯誤帶來的巨額損失，任誰也只能嘆一聲傷不起。
如果說上面兩個故事聽起來都過分沉重了，我們不妨看一下下面這張圖：
上圖顯示了全球範圍內用形式化方法開發的地鐵項目分佈情況[6]。
可以看出，由巴黎地鐵信號系統開始，在北美、歐洲、亞洲的主要國家，以及南美洲的部分國家的地鐵系統開發中，形式化方法已經被廣泛使用了。這或許是我們幾乎從未聽過由於地鐵系統故障而造成重大損失和災難的原因。
還是那句話，金錢是第一生產力。
既然形式化方法在保障日常出行方面做出的貢獻已經得到廣泛的認可，那麼，在依托區塊鏈技術而發展起來的數字資產領域，通過形式化驗證技術來保障智能合約安全性、進而保障財產安全性的理念就顯得合理甚至緊迫了。
具體需要怎麼做？這裡簡單介紹一下。
首先需要引入一個“形式化規範”的概念了。
形式化規範(formal specification) 是指通過數學語言對系統的預期行為(例如將數量S 的token 從賬戶A轉移到賬戶B) 和性質(例如轉賬不會造成賬戶B 額度的溢出) 進行嚴格和全面的定義。形式化規範往往定義了系統的正確性和安全性。
給定一個系統的形式化規範，我們即可以從規範出發開始迭代設計和實現出這個系統。在迭代的每一步中，我們可以通過精化(refinement)、集成(synthesis)、形式化證明在內的一系列方法在數學上嚴格的保證迭代產生的系統和迭代前的規範或者係統保持一致。
除了從形式化規範出發設計和實現一個系統，我們也可以使用包括符號執行(symbolic execution)、模型檢測(model check) 和形式化證明(formal proving) 在內的一系列方法驗證已有的設計和實現與該規範保持一致。
聽起來很高大上，對不對？
一級標題
一級標題
| 對抗攻擊
對抗攻擊其實是另一種意義上的避免損失。
故事從美國軍方的一次電子攻擊說起。 2015年夏天，一起黑客奉命對美國軍方Little Bird無人直升機發動電子攻擊，並掌握無人機控制權的事件中，黑客最初的攻擊十分順利，如入無人之境。然而，當美國國防部重新開發了該無人機的核心控製程序後，黑客們使用了當今世界上所有的攻擊手段，都未能攻破新部署的系統[7]。
到底是什麼技術給予了Little Bird超強的防禦能力，從而使它阻擋了所有的攻擊？答案就是：形式化驗證方法。
形式化驗證方法通過嚴格的數學證明保證程序行為與預期一致，但形式化驗證程序的正確性非常消耗人力，所以，與程序測試等通用技術不同的是，形式化驗證方法常常只被應用於安全攸關領域，如無人機、航天器、操作系統等的程序正確性驗證。
一級標題
一級標題
| 安全攸關的區塊鏈領域
區塊鏈領域亦然，一方面，小錯誤也會導致大損失；另一方面，巨大的經濟利益也會吸引大量的攻擊者。
以太坊黑客攻擊第一大案The DAO中，攻擊者竊取了當時價值5500萬美元的以太幣，並且導致了以太坊的硬分叉[11]；這之後，與以太坊智能合約相關的攻擊一直在繼續——比如，2017年11月，以太坊Parity錢包由於被黑客攻擊，導致用戶損失了價值約為1.5億美元的數字資產[11]。
據安比實驗室統計，僅2018年上半年，就已經有大約11億美元的數字資產被盜，與區塊鏈系統相關的漏洞（如以太坊中的智能合約漏洞）以及圍繞數字資產的生態系統安全問題（如多個中心化交易所被盜）更是層出不窮。
目前區塊鏈系統中的相關漏洞，以及數字資產生態系統的安全問題，歸根結底是相關程序設計與實現的問題。在形式化方法以前，這類問題多是通過程序測試來發現的。
形式化驗證進入區塊鏈領域的初期，以太坊社區的Yoichi Hirai對以太坊（Ethereum）的智能合約虛擬機EVM做了完整的形式化建模。此外，來自UIUC大學的團隊也對EVM進行了形式化的建模和驗證[12]。 EVM是以太坊智能合約的底層核心，關係到以太坊安全，涉及到數字資產保護等重大議題，引起了社區的廣泛關注。
此外，MakerDAO項目方發布了第一個經過形式化驗證的去中心化應用程序（DApp）[13]。 MakerDAO 是一個基於以太坊的智能合約平台，該平台提供了穩定幣（stablecoin），抵押貸款（collateral loans），以及去中心化社區治理功能。為了保證所部署的智能合約的安全性，MakerDAO團隊對抵押貸款（CDP）核心引擎合約代碼通過K-Framewok進行了驗證，因此而表明其智能合約程序能夠完全抵抗黑客攻擊。
一級標題
一級標題
https://github.com/sec-bit/tokenlibs-with-proofs
| 結論
大多數人認為形式化驗證方法高深莫測，究其原因，形式化驗證方法不是一種通用技術，而是需要和領域結合來發揮價值的一種特定技術。在區塊鏈領域，形式化方法究竟是一種nice to have還是一種must have，也是與項目特點密不可分的。
一級標題
一級標題
寫在最後| 關於Verification與Testing的糾葛，你了解多少？
最後來談一下形式化驗證（Formal Verification）與程序測試（Testing）之間的關係。
“程序測試能證明錯誤的存在,但不能證明錯誤不存在”。 Edsger Dijkstra（1972年圖靈獎獲得者、形式化方法核心思想的提出者）如此評述。
在實踐中，尤其是在代碼足夠複雜的場景中，形式化驗證（Verification）與程序測試方法（Testing） 的驗證效果有如雲泥之別。
舉個例子來說：2009年，澳大利亞的科學家使用形式化方法對工業級操作系統seL4微內核進行了完整功能性驗證[15]，驗證方式同時以形式化驗證和程序測試兩種方式分別展開，驗證的結果是：形式化方法共發現460多個Bug，而程序測試只發現了16個Bug。
更有趣的是，在以高驗證成本著稱的形式化驗證領域，完全驗證seL4微內核只需要600萬美元的驗證成本，而以測試的方式通過CC EAL6級認證的成本竟高達8700萬美元[15 ]。
參考文獻
參考文獻
參考文獻
【1】History of Formal Verification at Intel
https://dac.com/blog/post/history-formal-verification-intel
【2】王健：說說形式化驗證（Formal Verification）吧
http://chainb.com/?P=Cont&id=1957
【3】Modeling and Validation of a Software Architecture for the Ariane-5 Launcher
https://link.springer.com/chapter/10.1007/11768869_6
【4】Tenth NASA Formal Methods Symposium
https://shemesh.larc.nasa.gov/NFM2018/
【5】玉兔使用的國產SpaceOS操作系統未來有望衍生出民用版本
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 verification and validation of ERTMS industrial railway train spacing system. In International Conference on Computer Aided Verification (pp. 378-393). Springer, Berlin, Heidelberg.
【7】COMPUTER SCIENTISTS CLOSE IN ON PERFECT, HACK-PROOF CODE https://www.wired.com/2016/09/computer-scientists-close-perfect-hack-proof-code/
【8】利用Dirty Cow實現docker逃逸
https://www.anquanke.com/post/id/84866
【9】CertiKOS: Yale develops world’s first hacker-resistant operating system
https://www.ibtimes.co.uk/certikos-yale-develops-worlds-first-hacker-resistant-operating-system-1591712
【10】Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li. A Practical Verification Framework for Preemptive OS Kernels. Proc. 28th International Conference on Computer Aided Verification (CAV’16)
【11】從技術角度剖析針對THE DAO的攻擊手法
https://www.8btc.com/article/93713
【12】kframework/evm-semantics
https://github.com/kframework/evm-semantics
【13】風投巨頭A16Z 投資穩定幣項目MakerDAO
https://www.jinse.com/bitcoin/246582.html
【14】構造形式化證明，解決智能合約安全問題——你的合約亟待證明
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 22nd symposium on Operating systems principles (SOSP '09).
