哪個故事真正符合你對形式化驗證的想象？

從誕生至今，形式化驗證（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）在內的一系列方法驗證已有的設計和實現與該規範保持一致。

聽起來很高大上，對不對？

舉個例子來說，對於一段智能合約程序，我們可以從它所有可能的輸入（例如函數參數的組合）和初始狀態（例如狀態變量初始值的組合）出發，根據每條語句的語義，逐句推導出程序的所有可能的結束狀態（例如合約執行結束後的狀態變量的值和產生的 event lo），並檢查合約的所有輸入、初始狀態、結束狀態的組合是否都和形式化規範保持一致。這有點類似於柯南破案那樣，一步步地推演。只不過，這裏所有的定義都是通過嚴格的數學語言描述，推導和檢查也是嚴格的數學推導和證明。根據待驗證的系統及其形式化規範的複雜程度，推導和證明即可以手工構造，也可能可以由機器自動產生。

在實踐中，推導和證明無法進行下去往往意味着設計和實現中存在不符合規範的 bug。通過分析推導和證明卡殼的位置和原因，可以定位出 bug 在設計和實現中的具體位置和成因。這樣的方法，讓數字資產領域中中嚴格意義上的規避錯誤、避免損失成爲可能。

對抗攻擊

對抗攻擊其實是另一種意義上的避免損失。

故事從美國軍方的一次電子攻擊說起。2015 年夏天，一起黑客奉命對美國軍方 Little Bird 無人直升機發動電子攻擊，並掌握無人機控制權的事件中，黑客最初的攻擊十分順利，如入無人之境。然而，當美國國防部重新開發了該無人機的核心控制程序後，黑客們使用了當今世界上所有的攻擊手段，都未能攻破新部署的系統 [7]。

到底是什麼技術給予了 Little Bird 超強的防禦能力，從而使它阻擋了所有的攻擊？答案就是：形式化驗證方法。

形式化驗證方法通過嚴格的數學證明保證程序行爲與預期一致，但形式化驗證程序的正確性非常消耗人力，所以，與程序測試等通用技術不同的是，形式化驗證方法常常只被應用於安全攸關領域，如無人機、航天器、操作系統等的程序正確性驗證。

這裏不得不提的是 2016 年發現的一個非常嚴重的 linux 操作系統內核漏洞 Dirty Cow （CVE-2016-5195）[8]，攻擊者可以通過這個漏洞獲得系統最高權限，從而使系統全部處於可被利用的狀態之下。

在操作系統領域，一些人身先士卒，嘗試用形式化方法避免安全攸關領域中的系統漏洞和黑客攻擊。耶魯大學邵中老師團隊通過模塊分層驗證法（modularlayered verification methods）成功研發了安全性和可靠性極高的計算機操作系統 CertiKOS[9]；中科大軟件安全實驗室馮新宇老師團隊也提出了一個針對搶佔式多任務操作系統內核的形式化驗證框架，併成功的應用在對嵌入式操作系統 uC/OS-II （該操作系統被廣泛應用於航空電子產品中）的驗證中 [10]。

安全攸關的區塊鏈領域

區塊鏈領域亦然，一方面，小錯誤也會導致大損失；另一方面，巨大的經濟利益也會吸引大量的攻擊者。

以太坊黑客攻擊第一大案 The DAO 中，攻擊者竊取了當時價值 5500 萬美元的以太幣，並且導致了以太坊的硬分叉 [11]；這之後，與以太坊智能合約相關的攻擊一直在繼續——比如，2017 年 11 月，以太坊 Parity 錢包由於被黑客攻擊，導致用戶損失了價值約爲 1.5 億美元的數字資產 [11]。

據安比實驗室統計，僅 2018 年上半年，就已經有大約 11 億美元的數字資產被盜，與區塊鏈系統相關的漏洞（如以太坊中的智能合約漏洞）以及圍繞數字資產的生態系統安全問題（如多箇中心化交易所被盜）更是層出不窮。

目前區塊鏈系統中的相關漏洞，以及數字資產生態系統的安全問題，歸根結底是相關程序設計與實現的問題。在形式化方法以前，這類問題多是通過程序測試來發現的。

形式化驗證進入區塊鏈領域的初期，以太坊社區的 Yoichi Hirai 對以太坊（Ethereum）的智能合約虛擬機 EVM 做了完整的形式化建模 [12]。此外，來自 UIUC 大學的團隊也對 EVM 進行了形式化的建模和驗證。EVM 是以太坊智能合約的底層核心，關係到以太坊安全，涉及到數字資產保護等重大議題，引起了社區的廣泛關注。

此外，MakerDAO 項目方發佈了第一個經過形式化驗證的去中心化應用程序（DApp）[13]。MakerDAO 是一個基於以太坊的智能合約平臺，該平臺提供了穩定幣（stablecoin），抵押貸款（collateral loans），以及去中心化社區治理功能。爲了保證所部署的智能合約的安全性，MakerDAO 團隊對抵押貸款（CDP）核心引擎合約代碼通過 K-Framewok 進行了驗證，因此而表明其智能合約程序能夠完全抵抗黑客攻擊。

安比實驗室也在以太坊智能合約形式化驗證方面做了大量的工作，提出了一個智能合約形式化驗證框架，並在該框架內證明了一些常見的 Token 合約，比如 ERC20，ERC721 等（其中包含轉賬、Token 總量等通用性功能）。這些被數學證明過的智能合約可以直接使用，不再需要擔心安全問題。這些合約源代碼和證明過程已經以開源 [14] 的方式貢獻給社區。

Github 倉庫地址： https://github.com/sec-bit/tokenlibs-with-proofs

結論

大多數人認爲形式化驗證方法高深莫測，究其原因，形式化驗證方法不是一種通用技術，而是需要和領域結合來發揮價值的一種特定技術。在區塊鏈領域，形式化方法究竟是一種 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 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/117688696
[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).