---
tags: sysprog
---
# 形式化驗證 (Formal Verification)
資料整理: [jserv](https://wiki.csie.ncku.edu.tw/User/jserv)
## 概況
以數學的角度來說，無論硬體還是軟體，一如世間萬物，所有的學問歸根結底都是數學問題。倘若所有的設計開發都能夠按照嚴格的數學方法進行，那麼開發出來的系統就會像數學本身一樣的完美：軟體不會出錯，硬體永遠以符合預期的規範工作。當然，這是數學家的理想。
形式化方法從硬體設計開始普及，人們從若干血淋淋的教訓中體悟，著手以形式化驗證來解決問題。iPhone XS 使用的 Apple [A12 Bionic](https://en.wikipedia.org/wiki/Apple_A12) 晶片，採用 7nm 製程，電晶體數量達到 69 億個，之後的 [A12X](https://en.wikipedia.org/wiki/Apple_A12X) 更擁有高達 100 億個電晶體。藉由形式化驗證，在構建硬體和生產軟體之前，工程人員得以提前找出設計錯誤。
晶片設計領域中，最知名的失敗案例，是 Intel 的 Pentium 處理器浮點運算單元出錯 ([FDIV Bug](https://en.wikipedia.org/wiki/Pentium_FDIV_bug))，數以萬計的 Pentium 處理器不得不回收和替換，給 Intel 造成約 4.7 億美元的損失。在那之後，Intel 開始在其晶片設計中廣泛採用形式化驗證。
:::info
1994 年 10 月，美國維吉尼亞州 Lynchburg College 數學系教授 [Thomas Nicely](http://www.trnicely.net/) 發現用 Pentium 電腦計算[布朗常數](https://en.wikipedia.org/wiki/Brun%27s_theorem)時，意外發現 824,633,702,441 和 824,633,702,443 的倒數的小數點後第 10 位算錯。事後發現是 Intel 為加速運算，將整個乘法表燒錄在處理器內，但在 2048 個乘法數字中，有 5 個輸入錯誤。這些錯誤其實不容易顯現，在運算過程中，它會自動修復錯誤，只有幾個二進位的數字組，才會造成完全錯誤的結果。Intel 工程師指出，約 90 億個除法才會遇到一個錯誤，但隨後有人聲稱實際上遭遇到這個錯誤的頻率要高得多。Intel 在 1994 年 12 月不得不召回有缺陷的 Pentium 處理器產品。
:::
根據 Moore 定律，硬體的複雜度是每 18 個月增加一倍，而工程師的設計生產力卻跟不上這個速率。徒然增加設計團隊的人力、沒在根本的生產力工具上改進，最終只會拉高整合的困難。現實的經驗中，頗多大型計畫超過一半的預算是花在整合（integration）與驗證 (verification) 之上。
> 延伸閱讀: [軟體缺失導致的危害](https://hackmd.io/s/B1eo44C1-)
現行確保系統設計品質的方法大致分以下三類：
* 傳統的測試 (testing)
* 模擬 (simulation)
* 形式化驗證
測試是指在軟硬體產品生產後，將選定的輸入信號送入待測物 (device under testing；DUT)，從而檢驗產品設計的正確與否。模擬則不需要用到實際的待測物件，而用一個數學模型代替，觀察此數學模型的行為，以推斷產品設計的正確與否。而形式化驗證則完全在數學模型的抽象層次，企圖證明系統設計架構的正確性。
形式化方法在電腦資訊系統的應用，可追溯到 1970 年代 IBM 維也納研究中心所開發出來的 [VDM (Vienna Development Methods)](https://en.wikipedia.org/wiki/Vienna_Development_Method) 技術，以數學符號表達出系統設計的規格，從而降低工程師間的錯誤溝通，提昇系統設計的品質。有形式化的 spec，可驗證的項目就分為「人工」和「機器運算」兩種。舉例來說，全自動化的驗證中有個叫做 model checking 的方法，簡單的說就是窮舉系統運行過程中所能達到的所有狀態 (state)。
1954 年，Martin Davis 首度用機器證明波蘭邏輯學家 Mojzesz Presburger 在 1929 年提出的 [Presburger 算術命題](https://en.wikipedia.org/wiki/Presburger_arithmetic) 的真偽。更早之前，圖靈就已藉由一個著名的「停機問題」證明圖靈完備的機器的不可解問題。2005 年由劍橋 Microsoft 研究院的 Georges Gonthier 給出[四色問題](https://mathworld.wolfram.com/Four-ColorTheorem.html) (任意地圖都可用四種顏色著色，使得沒有兩個相鄰國家的顏色相同) 的形式化證明，結果顯示，四色定理的機器驗證程式確實有效地驗證所有構形的可約性，完成證明中的要求。
:::info
Mojzesz Presburger 證明若只考慮加法運算，自然數系統是相容的
:::
目前對於系統軟體的形式化驗證，多集中在幾個微核心為基礎的作業系統，如 seL4，也僅僅是對微核心那區區數千行程式碼的驗證，微核心的精神就是只在特權模式執行最關鍵的作業系統操作，例如排程，其他都儘量搬到非特權模式中。
:::info
像網頁瀏覽器這樣複雜的軟體其實也能進行形式化驗證，請見: [Quark : A Web Browser with a Formally Verified Kernel](http://goto.ucsd.edu/quark/)
:::
:::success
耶魯大學的研究團隊在 [CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernel](https://www.usenix.org/system/files/conference/osdi16/osdi16-gu.pdf) 指出，用以開發 hypervisor 的 C 語言的子集和組合語言都可透過形式化驗證，在核心層面實作並行 ([concurrency](https://hackmd.io/@sysprog/concurrency))，避免多核系統中的 big kernel lock (BKL)。
延伸閱讀: [耶魯大學邵中：作業系統發展拐點已到，我們需要的是「反黑客入侵」的 CertiKOS](https://www.hksilicon.com/articles/1376689)
:::
程式碼層面的形式化驗證做完，是否就萬無一失呢？我們不能忘記編譯器，還有對應的執行時期系統 (如 C runtime)。為了保證穩定性和安全性，在美國軍方廣泛使用的 Ada 程式語言的編譯器是形式化方法開發。除了程式要經過形式化驗證，包含作業系統在內的執行環境呢？比如大家熟悉的智慧卡，其硬體、作業系統，甚至到編譯器均是通過形式化方法開發流程，所有的 API 和通訊協定均有形式化驗證背書，畢竟涉及到鉅額的賠償，務求嚴謹。在航空領域的 [DO-178B](https://en.wikipedia.org/wiki/DO-178B) 和 [DO-178C](https://en.wikipedia.org/wiki/DO-178C) 標準中，編譯器屬於需要鑑定的工具類型軟體，受檢驗的程度比照機載軟體一樣對待。
> 延伸閱讀:
> * [形式化方法的逆襲 —— 如何找出 Timsort 演算法和玉兔月球車中的 Bug？](https://bindog.github.io/blog/2015/03/30/use-formal-method-to-find-the-bug-in-timsort-and-lunar-rover/)
> * [Formal verification makes RSA faster — and faster to deploy](https://www.amazon.science/blog/formal-verification-makes-rsa-faster-and-faster-to-deploy)
形式化驗證做得最徹底的單位，可能是美國軍方。[Hacker-Proof Code Confirmed](https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920/) 是篇極好的科普文章，概述近年來形式化驗證領域的發展，主題探討美國 DARPA 用形式化方法證明一段武器程式碼的正確性。
2015 年夏季，一組駭客嘗試控制一架軍用無人直升機，藉由存取無人機的部分電腦系統，這群駭客入侵無人機的機載飛行控制電腦，當然之後就可透過無人機為所欲為。美國國防部高級研究計劃署 (DARPA) 藉由形式化驗證開發的 [HACMS (High-Assurance Cyber Military Systems)](http://www.darpa.mil/program/high-assurance-cyber-military-systems)，讓駭客們用 6 個星期仍未攻破。該文還舉例說明把直覺的「程式正確性」變成形式化規範不容易。比方說排序，下述規格看似正確：
> 對於列表裡任意第 $j$ 項，都有第 $j$ 項不大於第 $j + 1$ 項
不過這存在本質的問題，因為規格沒說結果列表是輸入的排列，你如果給定輸入`7 3 5`，程式卻輸出 `1 2`，也符合上述規範。
值得注意的是，在金融領域，很早就應用形式化驗證，諸如區塊鏈 (blockchain) 和乙太坊 ([Ethereum](https://www.ethereum.org/)) 的新技術在提出時，也透過形式化驗證過程，證明一個系統不存在某個缺陷，同時匹配某個或某些屬性。[The DAO](https://daohub.org/) 全名為「去中心自治組織」(Decentralized Autonomous Organization)，可解讀為開放式的創投基金，建構在 Ethereum 技術的基礎，投資使用區塊鏈技術的共享經濟專案。2016 年 6 月 17 日，駭客透過德國 Ethereum 新創公司 Slock.it 提供的開放原始碼裡頭的 [系統漏洞](http://www.coindesk.com/understanding-dao-hack-journalists/)，攻擊 The DAO，致使以太幣資產池中，重複分離出本應被清零的自有以太幣，從而讓以太幣在被清零之前增長數十倍，直接劫持的以太幣總額高達 360 萬之譜 (市值約 7 千萬美元)。
The DAO 事件發生后，以太坊創始人 Vitalik Buterin 提議修改以太坊代碼，對以太坊區塊鏈實施硬分叉 (hard fork)，將被盜取資金的交易記錄退回，儘管獲得大部分礦工的支持，也遭到少數人的強烈反對，最終導致以太坊社群的分裂。隔年 7 月 19 日，多重簽章錢包 [Parity](https://github.com/paritytech/parity-ethereum) 被爆出其 1.5 版出現安全漏洞，15 萬枚以太幣被盜，約等同價值 3000 萬美元。
[Ethereum Foundation](https://ethereum.org/foundation) 在本次攻擊事件中吸收到最大的教訓就是，在智慧合約中設立觸發條件，經多人數位簽名或經多數區塊節點表決同意後，可停止智慧合約的自動執行，並且部署藉由形式化驗證技術，對智慧合約進行自動化偵錯、檢查和驗證。
> 延伸閱讀:
> * [以太坊的演進之路](http://www.8btc.com/the-evolution-of-ethereum)
> * [未來，核武器也可以用區塊鏈進行控制？](https://www.inside.com.tw/2016/10/11/even-the-us-military-is-looking-at-blockchain-technology)
> * [Formal Verification of Ethereum Contracts](https://github.com/pirapira/ethereum-formal-verification-overview)
> * [Solidity 的形式化驗證](https://read01.com/zh-tw/8gQPz3.html)
網路服務公司，像是 Amazon，用 [TLA+](http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html) 來驗證他們的核心架構內容，比如 S3。OpenSSL 於 2014 年 4月 7 日被揭露的 Heartbleed Bug，對整個網路和伺服器產業帶來巨大影響，連同 Google, Facebook 一類的廠商紛紛提出更安全的 SSL 實作。
2015 年 6 月 Amazon 發布一項新的開放原始碼 Transport Layer Security (TLS) 通訊協定的實作，取名為 [s2n](https://github.com/awslabs/s2n)，其中設計目標就是更高的安全性。2016 年 9 月，Amazon 和 Galois, Inc. (一間資訊安全公司，專門承接美國軍方和航空太空這類高風險的研究計畫委託) 合作，對 s2n 進行形式化驗證，請見:
1. [Verifying s2n HMAC with SAW](https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/)
2. [Specifying HMAC in Cryptol](https://galois.com/blog/2016/09/specifying-hmac-in-cryptol/)
3. [Proving Program Equivalence with SAW](https://galois.com/blog/2016/09/proving-program-equivalence-with-saw/)
延伸閱讀:
* [Use of Formal Methods at Amazon Web Services](http://research.microsoft.com/en-us/um/people/lamport/tla/amazon.html)
* [IronFleet](https://github.com/Microsoft/Ironclad)︰使用 TLA 驗証分散式系統。Microsoft Research 的論文︰[IronFleet: proving practical distributed systems correct](http://dl.acm.org/citation.cfm?doid=2815400.2815428)
Arm 公司的研究員 Alastair Reid 發表一篇文章 [Verifying against the official ARM specification](https://alastairreid.github.io/alastairreid.github.io/using-armarm/)，探討形式化驗證對 Arm 指令集架構 (ISA) 設計和驗證的助益。
## 驗證的發軔
資訊系統的正確性之所以很難完全確認，很多時候是因為需求本身就是模糊不清。關於工程人員追求資訊系統正確性的嘗試，可追溯到發明差分機和分析機的 [Charles Babbage](https://en.wikipedia.org/wiki/Charles_Babbage)，他是活躍於十九世紀的數學家、發明家兼機械工程師，源於工業時代的進步帶來蒸汽機和各種機械裝置，人們相信機械的力量可滿足各式需求，將人們從各式勞動中解放出來。Babbage 開始對數學製表的機械化的研究 -- 在電子計算機問世前，很多計算仰賴查表，但靠人工來製表不僅費時費力，而不免會有運算、抄寫數值、校對，和印製等等各式錯誤。Babbage 在劍橋求學時，發現到這個現象，並將改善製表時的各種問題作為畢生志業。
Babbage 向人們展示，如果在船隻導航過程中沒有留意前述表格的誤差，就有可能讓船隻偏航，進而沈沒。1823 年，Babbage 說服英國政府資助他發展差分機，後者可快速提供計算導航計算表，而且完全避開人為運算的誤差。
差分機又稱差分引擎 (difference engine)，不是一般意義上的「計算機」，要注意到，當時可做簡單的加減乘除的機械裝置已存在 (如計算尺)，而 Babbage 想打造的機器本質是一台「多項式求值機」，只要將欲求值的方程式輸入到機器裡，機器每運轉一輪，即可產生答案數值。
以 $F(x) = x^2 +4$ 為例，差分機處理的過程會是 `F(1) = 5`, `F(2) = 8`, `F(3) = 13`, ... 直到系統停止為止。求值完全只需用到加減法操作。
上圖展示差分機處理的每個步驟：第一步是算出 `F(1)` 和 `F(2)` 的值之間的差 (`8 - 5 = 3`)，稱為第一階差 (first difference)。若這個值和 `F(2)` 及 `F(3)` 之間的差 (`13 - 8 = 5`）不同的話，就拿這兩個第一階差再算一次差 (`5 - 3 = 2`），稱為第二階差 (second difference)。此例中，第二階差每一個都是 2，所以就不用再計算下去。一次方程式最多只有第一階差，二次會到第二階差，推廣到 N 次會到 N 階差。一旦有個固定不變的差數後，即可往前推算回去，接下來的每一個值，是將差數和前一階的上一個值相加，就可獲得。例如求 `F(4)` 時，先將 2 加上上一階差的值 5 得到 7，再將 7 加上 `F(3)` 的值 13，就會得到 F(4) = 20，以此類推。
* 延伸閱讀: [查爾斯．巴貝奇的差分機與分析機](https://chinese.engadget.com/2011/04/27/charles-babbages-difference-and-analytical-engines/)
可惜 Babbage 的差分機引擎一號 (Difference Engine No.1) 經過 10 年的打造仍只完成七分之一，最後英國政府也失去耐心，這項計畫還未完全實作，就在超支和延期中被迫停止。
在 1834 年，Babbage 著手設計一台野心更大的機器，稱為分析機引擎 (analytical engine)，這無疑超前時代過多，註定成為悲劇。怎麼說呢？首先，它的機械結構分成「計算單元」和「儲存單元」兩個部份，計算單元不僅內建四則運算，還可儲存四組不同的運算方程式，用穿孔卡片 (punch card) 載入到機器裡。這台機器在設計上甚至有能力進行條件分支 (if-else 一類)、迴圈、平行處理等程式邏輯，當然 Babbage 的年代尚未有這類詞彙來描述，最後運算的結果可選擇印刷、打卡、繪圖等多種輸出方式。分析機將計算、儲存、輸出輸入等三項分離的設計，概念上等同於今日的電腦架構，只是分析機停留在設計圖上，缺乏資本和適度的工藝來落實。
瑞典的父子檔工程師 [Georg Scheutz 和 Edvard Scheutz](http://www.computerhistory.org/babbage/georgedvardscheutz/) 在 1843 年著手重建兩台 Babbage 設計的差分機，並輸出運算表格，但機器效能不穩定且需要繁瑣的配置，很少有人願意使用。
這段歷史插曲告訴我們，計算機發展的過程從未脫離錯誤，而且致使錯誤的原因相當多元，設計者必須證明機械碼準確地實踐預期的功能，倘若機器只是近似實作某些預期功能 (如同上述差分機)，設計者需要額外的分析和證明，確保這類近似功能所產生的錯誤，不會對運算結果帶來實質衝擊。
在人們驗證的過程中，自動正確性驗證是其中一個重要考量，其一進展是 model checking，基本想法是將軟體系統建構為一個有限狀態機 (FSM)，然後驗證該有限狀態機滿足一組時序邏輯推論，有限狀態機模型展現實際機器所能觀察到的行為，以及這些行為之間的遷移關係，而時序邏輯表達軟體系統行為的形式化規範。
## 公理系統
論及形式化方法前，讓我們重新面對數學。由於中小學充斥著大量的算術，致使某些人認定數學的學習無非就是接觸一系列解題公式或步驟，這樣的看法非常偏頗。畢竟顧及學生的回饋和便於測驗，中小學的數學教育往往偏重於數學技巧，但數學的真諦並非於掌握解題技巧，而是在於了解各個概念、定理之間的邏輯關係，換言之，解題結果不是最重要的，邏輯推理過程同樣重要。
數學的演進中，許多新概念來自舊概念的推廣 (generalize)，一方面使學數者得以借助舊概念理解新概念，另一方面亦要求學數者能從不同的角度思考，因為新概念往往不是舊概念的簡單推廣，而是在舊概念進行重新解釋或突出舊概念某些點後作出的推廣。
數理邏輯可視為數學的邏輯分析，但通常與符號邏輯 (Symbolic Logic) 之涵義相同，也就是說，數理邏輯指的是人用符號來進行邏輯演算和分析。狹義的數理邏輯專指邏輯的演算，包含命題演算及述詞演算 (Propositional and Predicate Calculi)。廣義的則包含數學的集合論、證明論及其他相關的系統。由於數理邏輯比照代數般運用符號，因此相當形式化。今日數理邏輯也與語言學、資訊科學密切聯繫，並不侷限於數學與邏輯領域。
公理化方法 (或公理方法)，是自儘可能少的無定義的原始概念 (基本概念) 和一組不證自明的命題 (基本公理) 出發，利用純邏輯推理法則，把一門數學建立成為演繹系統的一種方法。所謂基本概念和公理，當然必須反映數學實體對象的最單純的本質和客觀關係，而並非人們自由意志的隨意創造。
> 延伸閱讀: [布林邏輯與公理系統](https://ccckmit.gitbooks.io/rlab/content/axiom.html)
根據歷史發展，公理方法大致分為三個階段：
- [ ] 公理方法的產生階段
大約在公元前 3 世紀，希臘的哲學家和邏輯學家亞里士多德總結古代積累起來的邏輯知識，以演繹證明的科學（主要是數學）為實例，把完全三段論作為公理，由此推導出別的所有三段論法（共分 19 個格式）。亞里士多德提出了史上第一個成文的公理系統。
亞里士多德的思想方法深深影響歐幾里得，後者把形式邏輯的公理演繹方法應用於幾何學，從而完成數學史上的重要著作《幾何原本》。《幾何原本》的問世標誌數學領域中公理方法的誕生。
> 延伸閱讀: [用邏輯系統就能判斷論證對確嗎？](https://www.thenewslens.com/article/39586)
- [ ] 公理方法的完善階段
歐氏幾何的公理系統是不夠完善的。其主要的不足之處可以概括為：
* 有些定義是不自足的，亦即往往使用一些未加定義的概念去對別的概念下定義;
* 有些定義是多餘的，略去它毫不影響往後的演繹和展開;
* 有些定理的證明過程往往依賴於圖形的直觀;
另一方面，由於第五公設（即平行線公理）在陳述於內容上的複雜和累贅，古代學者們早就懷疑地指出，第五公設是不是多餘的，它能否從其他公設、公理中邏輯地推導出來？而且進步一認為，歐幾里得之所以把它作為公設，只是因為他未能給出這一命題的證明。因而，學者們紛紛致力於證明第五公設。
19 世紀俄國數學家羅巴切夫斯基 (Nikolas lvanovich Lobachevsky) 提出迥異於前人的想法：首先，第五公設不能從其餘的公理幾何作為定理來證明；其次，除掉第五公設成立的歐幾里得幾何之外，還可有第五公設不成立的新幾何系統存在。於是，他在剔除第五公設並保留歐氏幾何其餘公理的前提下，引進了一個相反於第五公設的公理：
>「過平面上一已知直線外的一點至少可引兩條直線與該已知直線平行」。
這樣，羅巴切夫斯基在與前人完全不同的思想方法基礎上構造一個新的幾何系統，它與歐幾里得幾何系統相併列。後來，人們又證明這兩個部分地互相矛盾的幾何系統竟然是相對相容的，亦即假定其中之一無矛盾，則另一個必定無矛盾。如此，只要這兩個系統是無矛盾的，第五公設與歐氏系統的其餘公理就必定獨立無關。現在人們就用羅巴切夫斯基的名字對這一新幾何命名，並把一切不同於歐氏幾何公理系統的幾何系統統稱為非歐幾何。
非歐幾何學中的一系列命題都和人們的樸素直觀不相符合。但是，這種背離直觀的幾何學在邏輯系統內沒有矛盾，演繹論證的嚴格性也是無瑕可擊的。事實上，非歐幾何給人們開拓「空間」的概念（正如大家所知的，非歐幾何的重要分支「黎曼幾何」在愛因斯坦 1915 年創立廣義相對論後，已得到證實和應用）。非歐幾何的產生，不僅為公理化方法進一步奠定基礎，而且為公理方法可推廣和建立新的數學理論提供依據。
- [ ] 公理方法的形式化階段
17 世紀萊布尼茲 (Gottfried Wilhelm Leibniz) 曾討論一些邏輯方面的問題，但數理邏輯之發展要到 19 世紀才有重大的突破。摩根 (A. de Morgan) 提出「關係邏輯」觀念，提供人們一種新的思考方向，布爾 (George Boole) 將邏輯置於數學系統內，並建立了邏輯演算的雛型。弗列格 (Gottlob Frege) 在前兩人的基礎上繼續努力，並建立一個邏輯演算體系，使邏輯的形式化有進一步的發展。
19 世紀後葉由弗列格開啟的形式邏輯，將數學證明中所常用到的「量詞」(像是 "for any" 和 "exist") 形式化。在這之前，僅有三段論被形式化，但以數學證明而言，只有三段論是遠遠不夠。
以 17 世紀就被提出的微積分來說，其邏輯基礎其實相當薄弱，長達兩百年的時間，沒有人有辦法去處理諸如無窮小、無窮多這種觸及邏輯層面的問題 (可見 [芝諾悖論](https://en.wikipedia.org/wiki/Zeno%27s_paradoxes))，一直要到 1860 年 Weierstrass 才嚴格地用今日廣泛使用的 ε-δ 證明法，來處理極限問題。至此，微積分才算建立起無瑕的邏輯基礎，同時大家紛紛體驗到公理化的威力，開啟數學各支派的公理化運動。
> 延伸閱讀: [極限、連續與督脈的貫通](http://ocw.aca.ntu.edu.tw/ocw_files/101S130/101S130_CS10L01.pdf)
Richard Dedekind 將實數公理化；皮亞諾 (Giuseppe Peano) 將數論公理化；非歐幾何的創立提升公理方法的信譽，希爾伯特 (David Hilbert) 於 1899 年發表的《幾何學基礎》一書，解決歐氏幾何的欠缺問題，完善幾何學的公理化方法，此書稱為近代公理化思想的代表作。
> 延伸閱讀: [為什麼要公理化實數而不是從自然數導出？](https://www.zhihu.com/question/51633217)
一步一步往走到集合論公理化時，卻遇上大麻煩，反映於 1901 年提出的羅素悖論 ([Russell's paradox](https://en.wikipedia.org/wiki/Russell%27s_paradox))，造成第三次數學危機。1910 年至 1913 年間懷德海 (Alfred North Whitehead) 與羅素 (Bertrand Russell) 師生共同出版《數學原理》(Principia Mathematica)，書中二人從邏輯的演算中導出數學並以符號來表示推理過程。集合論公理化所遇上的麻煩，需要藉由形式邏輯方可有系統的處理，後來就發展出各種的集合論公理系統，如 ZFC 集合論公理系統，後者是今日數學界普遍承認的公理體系。
當數學各支派大成致完成公理化後，邏輯系統本身也冒出許多屬於自身的問題。希爾伯特為防止弔詭論及邏輯矛盾的出現，提出證明一致性的「希爾伯方案」(Hilbert program) 或證明論，主張完全形式化公理系統之一致性可加以證明。一直到 1930 年代，哥德爾 (Kurt Gödel) 一邊證明古典邏輯的完備定理 (completeness theorem) ── 羅素系統的邏輯真理都可用他的公理系統證明，另一方面也證明算術不完備定理 (incompleteness theorem of arithmetic) ── 沒有一致的公理和推論規則可證明所有數學真理，對邏輯主義投下一枚核彈，著名的「哥德爾定理」 (Gödel’s theorem) ，指的正是後者。
人們這才真正意識到，邏輯系統本身也是有漏洞的 (存在不可証明之真命題)，自此，數理邏輯又衍生出証明論，模型論、遞歸論等等支派，對現在電腦發展造成直接影響。電腦背後的許多觀念，像是邏輯閘 (logic gates)，就如名稱所暗示，和邏輯學有密切關連。於是，20 世紀知名的邏輯學家，像是馮紐曼 (John von Neumann) 、圖靈 (Alan Turing) 、伯克斯 (Arthur Burks) 都曾協助設計電腦，從而建構電腦科學。
> 延伸閱讀:
> * [數學中的公理化方法 (上)](https://www.math.sinica.edu.tw/media/pdf/d171/17111.pdf)
> * [數學中的公理化方法(下)](https://www.math.sinica.edu.tw/media/pdf/d172/17203.pdf)
丘奇 (Alonzo Church) 於 1936 年證明沒有機械式的演算法可判斷述詞邏輯的每一個論證是否對確。既然形式算術系統是不可判定的，那麼任何包含形式算術系統作為子系統的形式系統也是不可判定的。另外丘奇還證明：一階邏輯也是不可判定的，也就是說，沒有一個演算流程可決定一個有限前提的一階論證是有效，抑或是無效。
## 電腦程式的形式化驗證
由於形式化驗證背後對應到不同產業對高品質軟硬體系統的要求，往往就會有不同的陣營，主導開發的國家有法國、德國、美國，以及澳大利亞。
工業上的作法是，透過定理證明器 (theorem prover)，像是如 Isabelle, Coq 等，把程式寫出來並證明相關的性質，然後把定理證明器內寫的程式提取 (Coq 的 code extraction 或 Isabelle 的 code generation) 為 Haskell, OCaml 一類的函數程式語言，再編譯運行。
編譯器的任務是進行忠實將原始程式碼轉換為二進位輸出或者另一種程式語言，但編譯器未必可靠，而且問題往往難以察覺。
法國電腦科學家 Xavier Leroy 帶領開發的 [CompCert](http://compcert.inria.fr)，透過形式化證明來解決這個問題。開發 CompCert 的時候，對於編譯程式的每一步操作，都用 Coq 給予對應的數學證明，確保代碼的語義在每步都不變，最終確保編譯器會忠實轉換給定的程式碼。
:::warning
CompCert 的原始程式碼可在 [GitHub](https://github.com/AbsInt/CompCert) 上存取，但本身並非開放原始碼，限制僅能非商業應用。
:::
開放原始碼的形式化驗證系統軟體成果，可見以下：
* [seL4](https://sel4.systems/): 形式化驗證的作業系統核心，使用 Isabelle
* [FSCQ](https://github.com/mit-pdos/fscq-impl): 形式化驗證的檔案系統，使用 Coq。MIT CSAIL 論文: [Using Crash Hoare logic for certifying the FSCQ file system](http://dl.acm.org/citation.cfm?id=2815402)
Model checking 的具體作法是狀態空間檢索 (state-space search)，原理就是將程式或通訊協定看作一個分散式系統，局部狀態表示每個主題執行通訊協定的過程，而所有局部狀態構成全域狀態，每個局部狀態的改變由主體的訊息接收、發送來觸發。
Model checking 的主流工具包括 SPIN, AsmL, SMV 等等，理論主要是利用時序邏輯(Temporal Logic) 和有限狀態機 (Finite State Machine)，應用遍及硬體設計、安全分析、自動控制等範疇。
1980 年代，貝爾實驗室的形式化驗證團隊開發 SPIN，使用 Promela 程式语言來建構，整個系統可看作一组同步、可擴展的有限狀態機，支援所有可用的線性時序邏輯，來表示正確性驗證要求。
由法國 INRIA 和法國幾間大學合作開發的 Coq 是個交互式的定理證明輔助工具 (proof assistant )，允許開發者輸入包含數學斷言 (assertion) 的表達式、機械化地對這些斷言執行檢查、幫助構造形式化的證明、並從其形式化描述的構造性證明中提取出可驗證的（certified）程式。
Coq 的理論基礎是歸納構造演算（calculus of inductive constructions）、一種構造演算（calculus of constructions）的衍生理論。Coq 並非一個自動化定理機器證明語言；然而，它提供自動化定理證明的策略（tactics）和不同的決策過程。
[Lean](https://leanprover.github.io/) 是另一個新的開放原始碼的定理證明器，由 Microsoft 研究院和卡內基美隆大學大學共同設計並實作。Lean 的目標是透過情景化自動工具和方法，在交互定理證明（ITP）與自動定理證明（ATP）之間建立起一種聯繫，從而填補之間的空白。Lean 支持數學推理、複雜系統推理以及相關驗證。
* [Lean 線上教材](https://leanprover-community.github.io/learn.html)
針對不同的應用領域，運用不同的形式演算方法，出現多種機器定理證明系統，主要分為交互式定理證明器（interactive theorem prover）和自動化定理證明器（automated theorem prover）兩大類。
機器定理證明技術的發展經歷從自動到交互，再回到自動的過程。人們最早設計的定理證明系統是自動化。隨著應用的複雜化，自動化定理證明系統受到執行時間和空間上的挑戰，於是出現交互式定理證明系統。
交互式定理證明器以人機交互為基礎，使用者先指定每一個證明步驟要做的工作，然後由計算機完成具體的工作細節。部分交互式定理證明器可能帶有一個邏輯框架 (logical framework)，從而具有很強的表達能力，可用於實作非常複雜的形式系統，如 [Isabelle/HOL](http://isabelle.in.tum.de/)。交互式定理證明器往往基於有類型的 Lambda 演算（Typed λ-calculus）及自然推理，常用的有用於驗證硬體和即時系統的 HOL 和 PVS，用於數學形式化的 Coq 等。
自動化定理證明則較少需要使用者的直接干預，它們應用各種專門的演算法、資料結構和最佳化技術，自動確定每一個推理步驟的工作，能夠快速證明一些非常複雜的問題。現在已開發出很多高性能的自動化定理證明器，如 Vampire, Otter, SETHEO, PTTP 等。
## seL4
seL4 的形式化驗證分為兩個層次：
* abstract specification（抽象規範）和 executable specification（可執行規範）之間;
* executable specification 和 implementation (實作) 之間;
形式驗證步驟如下：
1. 用 Isabelle/HOL 寫出 IPC, syscall, 排程等等微核心的 kernel object 的 abstract specification;
2. 用 Haskell 撰寫上述 kernel object 的 executable specification，並證明正確實作前一步驟的 abstract specification，藉由狀態機來確保在 abstract specification 的每步狀態轉換，executable specification 都產生唯一對應的狀態轉換;
3. 開發 C 語言程式，並且透過特製的 C 語言程式解析器，證明 C 程式和前一步的 Haskell 定義語義一致;
1970 年代 UCLA 的研究人員就著手對 UNIX 作業系統進行驗證，seL4 則是集大成、帶來巨大變革，原因主要是以下兩個：
* seL4 擁有很強的屬性 (properties): 功能正確性 (functional correctness), 完整性 (integrity) 和機密 (confidentiality);
* 前述屬性已被形式驗證到程式碼等級，最初是 C 程式，現在又到二進位
## 應用案例
* [Formal Verification of Deed Contract in Ethereum Name Service](https://yoichihirai.com/deed.pdf)
* [The C standard formalized in Coq](http://robbertkrebbers.nl/thesis.html)
* [Proving C and C++ programs correct](http://www.eschertech.com/articles/index.php)
## 參考資料
* [SAT/SMT by Example](https://smt.st/SAT_SMT_by_example.pdf)
* [思想開通－學數之人必備的特質](http://chowkafat.net/Mathpassage2.html)
* [形式化研究的侷限](http://www.atlas-zone.com/science/talk/part_1/science1450.htm)
* [So you want to be a proof engineer?](http://proofcraft.org/blog/proof-engineer-reading.html)
* [Don't Test, Verify | 哪個故事真正符合你對形式化驗證的想像？](https://zhuanlan.zhihu.com/p/47564408)
## 相關課程
* [Introduction to Functional Programming (Haskell), edX](https://www.edx.org/course/introduction-functional-programming-delftx-fp101x-0#!)
* [Introduction to Mathematical Thinking, Coursera](https://www.coursera.org/learn/mathematical-thinking)
* [Introduction to Logic, Coursera](https://www.coursera.org/learn/logic-introduction)
* video: [Theory of Computation, Fall 2011, UC Davis](https://www.youtube.com/playlist?list=PLslgisHe5tBM8UTCt1f66oMkpmjCblzkt)
* [Introduction to the Theory of Computation, Fall 2016, MIT](https://math.mit.edu/~sipser/18404/)
* [Algorithmic Verification (UNSW) ](https://cgi.cse.unsw.edu.au/~cs4161/)
* [Formal Reasoning About Programs (MIT) ](https://frap.csail.mit.edu/main)
Sign in with Wallet
Connect another wallet