Don’t Test, Verify. | 哪個故事真正符合你對形式化驗證的想象？
從誕生至今，形式化驗證（Formal Verification）方法一直與“小眾、冷門”等字眼掛鉤。有人說形式化驗證方法是一種“軍用級別”的防黑客手段，更是為這項技術增添了一絲神祕感。
究竟什麼是形式化驗證方法？
維基百科對形式化驗證的解釋是這樣的：
在計算機硬體（特別是積體電路）和軟體系統的設計過程中，形式化驗證的含義是根據某個或某些形式化規範或屬性，使用數學的方法證明其正確性或非正確性。
神祕感大抵來源於定義中的兩個嚴謹而且抽象的關鍵詞——“形式化規範”和“數學方法證明”。事實上，揭開這層神祕的面紗，你會發現形式化驗證的許多有趣之處。
下面這篇文章想要討論的問題是：在現階段，以下哪個故事能夠真正滿足你對形式化驗證的想象？形式化驗證真的可以作為一種技術在區塊鏈領域流行起來嗎？如果可以，怎樣才能做到？
（PS：上文中提到的“形式化規範”的概念，在下文中也會講到。）
要回答上面這些問題，我們可以先思考另一個更簡單的問題： > 現階段，人們使用形式化方法來做什麼？ 這個問題的答案無非有兩種： > 1、 規避錯誤 > 2、 對抗攻擊
| 規避錯誤
規避錯誤其實就是避免損失。
我們首先來探討一下，哪些領域對程式錯誤是零容忍的？在哪些領域，程式錯誤帶來的損失難以估量？
實際上，形式化方法是從硬體設計開始普及的。一個著名的例子是：當年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]，也都是通過形式化方法驗證其正確性。
歷史的發展告訴我們，金錢才是推動社會發展的第一動力！程式錯誤帶來的鉅額損失，任誰也只能嘆一聲傷不起。
如果說上面兩個故事聽起來都過分沉重了，我們不妨看一下下面這張圖：
可以看出，由巴黎地鐵訊號系統開始，在北美、歐洲、亞洲的主要國家，以及南美洲的部分國家的地鐵系統開發中，形式化方法已經被廣泛使用了。這或許是我們幾乎從未聽過由於地鐵系統故障而造成重大損失和災難的原因。
還是那句話，金錢是第一生產力。
既然形式化方法在保障日常出行方面做出的貢獻已經得到廣泛的認可，那麼，在依託區塊鏈技術而發展起來的數字資產領域，通過形式化驗證技術來保障智慧合約安全性、進而保障財產安全性的理念就顯得合理甚至緊迫了。
具體需要怎麼做？這裡簡單介紹一下。
首先需要引入一個“形式化規範”的概念了。
形式化規範 (formal specification) 是指通過數學語言對系統的預期行為 (例如將數量 S 的 token 從賬戶 A轉移到賬戶 B) 和性質 (例如轉賬不會造成賬戶 B 額度的溢位) 進行嚴格和全面的定義。形式化規範往往定義了系統的正確性和安全性。
給定一個系統的形式化規範，我們即可以從規範出發開始迭代設計和實現出這個系統。在迭代的每一步中，我們可以通過精化(refinement)、整合 (synthesis)、形式化證明在內的一系列方法在數學上嚴格的保證迭代產生的系統和迭代前的規範或者系統保持一致。
除了從形式化規範出發設計和實現一個系統，我們也可以使用包括符號執行 (symbolic execution)、模型檢測 (model check) 和形式化證明 (formal proving) 在內的一系列方法驗證已有的設計和實現與該規範保持一致。
聽起來很高大上，對不對？
舉個例子來說，對於一段智慧合約程式，我們可以從它所有可能的輸入 (例如函式引數的組合) 和初始狀態 (例如狀態變數初始值的組合) 出發，根據每條語句的語義，逐句推匯出程式的所有可能的結束狀態 (例如合約執行結束後的狀態變數的值和產生的 event log)，並檢查合約的所有輸入、初始狀態、結束狀態的組合是否都和形式化規範保持一致。這有點類似於柯南破案那樣，一步步地推演。只不過，這裡所有的定義都是通過嚴格的數學語言描述，推導和檢查也是嚴格的數學推導和證明。根據待驗證的系統及其形式化規範的複雜程度，推導和證明即可以手工構造，也可能可以由機器自動產生。
在實踐中，推導和證明無法進行下去往往意味著設計和實現中存在不符合規範的 bug。通過分析推導和證明卡殼的位置和原因，可以定位出 bug 在設計和實現中的具體位置和成因。這樣的方法，讓數字資產領域中中嚴格意義上的規避錯誤、避免損失成為可能。
| 對抗攻擊
對抗攻擊其實是另一種意義上的避免損失。
故事從美國軍方的一次電子攻擊說起。2015年夏天，一起黑客奉命對美國軍方Little Bird無人直升機發動電子攻擊，並掌握無人機控制權的事件中，黑客最初的攻擊十分順利，如入無人之境。然而，當美國國防部重新開發了該無人機的核心控制程式後，黑客們使用了當今世界上所有的攻擊手段，都未能攻破新部署的系統[7]。
形式化驗證方法通過嚴格的數學證明保證程式行為與預期一致，但形式化驗證程式的正確性非常消耗人力，所以，與程式測試等通用技術不同的是，形式化驗證方法常常只被應用於安全攸關領域，如無人機、航天器、作業系統等的程式正確性驗證。
這裡不得不提的是2016 年發現的一個非常嚴重的 linux 作業系統核心漏洞Dirty Cow (CVE-2016-5195)[8]，攻擊者可以通過這個漏洞獲得系統最高許可權，從而使系統全部處於可被利用的狀態之下。
在作業系統領域，一些人身先士卒，嘗試用形式化方法避免安全攸關領域中的系統漏洞和黑客攻擊。耶魯大學邵中老師團隊通過模組分層驗證法(modular layered verification methods)成功研發了安全性和可靠性極高的計算機作業系統CertiKOS[9]; 中科大軟體安全實驗室馮新宇老師團隊也提出了一個針對搶佔式多工作業系統核心的形式化驗證框架，併成功的應用在對嵌入式作業系統 uC/OS-II （該作業系統被廣泛應用於航空電子產品中）的驗證中[10]。
| 安全攸關的區塊鏈領域
區塊鏈領域亦然，一方面，小錯誤也會導致大損失；另一方面，巨大的經濟利益也會吸引大量的攻擊者。
以太坊黑客攻擊第一大案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進行了驗證，因此而表明其智慧合約程式能夠完全抵抗黑客攻擊。
安比實驗室也在以太坊智慧合約形式化驗證方面做了大量的工作，提出了一個智慧合約形式化驗證框架，並在該框架內證明了一些常見的Token合約，比如ERC20，ERC721等（其中包含轉賬、Token總量等通用性功能）。這些被數學證明過的智慧合約可以直接使用，不再需要擔心安全問題。這些合約原始碼和證明過程已經以開源[14]的方式貢獻給社群。
| 結論
大多數人認為形式化驗證方法高深莫測，究其原因，形式化驗證方法不是一種通用技術，而是需要和領域結合來發揮價值的一種特定技術。在區塊鏈領域，形式化方法究竟是一種nice to have還是一種must 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]。
由此可見，通過形式化驗證可以更經濟的為seL4微核心提供更強的安全性保證。
當然，有人說，程式測試是在“真實”環境裡進行的，形式化驗證只是數學層面，在“真實”環境中的測試是形式化驗證無法取代的。從這個角度來說，形式化驗證與程式測試如何做到共生互補？讓這項技術在區塊鏈領域真正流行起來，可能就是鏈圈同仁們接下來要共同探索的方向了。
參考文獻
【1】History of Formal Verification at Intel
【2】王健：說說形式化驗證（Formal Verification）吧
【3】Modeling and Validation of a Software Architecture for the Ariane-5 Launcher
【5】玉兔使用的國產SpaceOS作業系統未來有望衍生出民用版本
【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.
【8】利用Dirty Cow實現docker逃逸
【9】CertiKOS: Yale develops world’s first hacker-resistant operating system
【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的攻擊手法
【12】kframework/evm-semantics
【13】風投巨頭 A16Z 投資穩定幣專案 MakerDAO
【14】構造形式化證明，解決智慧合約安全問題——你的合約亟待證明
【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).