操作系統形式化驗證綜述

錢漢偉,王承毅

(1.江蘇警官學院計算機信息與網絡安全系，江蘇 南京 210031; 2.江蘇科技大學理學院，江蘇 鎮江 212003)

計算機軟件與人們生活密切相關，從網絡、手機等日常通信設備到能源、國防等關鍵基礎設施，幾乎無處不在。另一方面，由于缺少有效手段控制軟件質量，使得軟件的漏洞或錯誤幾乎不可避免。每年由于軟件的漏洞或者錯誤導致的損失達上百億美元。操作系統是所有軟件的基礎平臺，嚴格保證其可靠性和安全性具有重要價值。目前已知技術中，只有形式化方法能夠保證軟件不會出錯，但是由于操作系統復雜度大、并發度高等問題，其形式化驗證一直以來都是一件非常困難的工作。

隨著定理證明助手等形式化驗證工具功能更加強大，CertiKOS[1]形式化驗證理論和框架更加完善，操作系統的形式化設計和驗證工作進入一個新階段，并且取得了一系列重要成果。如seL4等操作系統軟件的內核功能正確性和無內存泄漏等性質均得到了有效證明。本文對近年來操作系統形式化驗證技術、方法和研究進展進行總結，闡述操作系統形式化驗證過程中對形式化驗證新技術和方法的應用，分析當前操作系統形式化驗證存在的問題，展望操作系統形式化驗證未來的發展方向。

1 形式化驗證技術

1.1 支撐理論和框架

目前操作系統的形式化驗證是用定理證明的方法對操作系統的性質規約進行驗證。其中，Hoare邏輯[2]是性質規約描述的邏輯基礎，當前驗證工作廣泛使用的分離邏輯[3]、并發分離邏輯[4]和并發精化程序邏輯[5](CSL-style relational program logic，CSL-R)等均是以Hoare邏輯為基礎進行的擴展。霍爾邏輯證明規約用形如“{Pre}P{Post}”的Hoare三元組表示，通過前置條件和后置條件，比如某些不變量，放入程序要證明的性質，實現了用一組公理和一組規則描述程序代碼應有的性質。分離邏輯對霍爾邏輯進行了擴展，增加了分離合取和分離蘊含謂詞及相應的推導規則，能夠以自然的方式描述計算過程中內存的屬性和相關操作，驗證指針程序也更加方便。并發精化程序邏輯將并發分離邏輯的斷言語言擴展為關系型斷言，更適合證明與多級中斷有關的并發程序的上下文精化關系。數據精化的概念最早由Back[6]提出，Morgan[7]發展了類似的一種精化方法。Roever等[8]詳細論述了數據精化證明方法。實際上，操作系統驗證問題也是精化驗證問題，操作系統從底層模型到高層規約之間的一致性驗證等問題都是以精化理論為基礎。攜帶證明代碼(proof carrying code，PCC)[9]將Hoare邏輯應用到匯編語言的安全性質檢驗中，可執行代碼和證明捆綁傳遞的方式為證明連接提供了可能性。基礎性攜帶證明的代碼(foundational proof-carrying code，FPCC)[10]將攜帶證明代碼與復雜的推理系統都形式化在一個底層的基礎邏輯中，推理系統的可靠性可以用基礎邏輯保證，可進一步縮小信任基(trusted base)。在基礎性攜帶證明代碼的基礎上進一步提出的開放邏輯框架[11](open certified assembly programming，OCAP)則可以將操作系統軟件不同模塊的驗證邏輯結合起來，形成完整的驗證系統，極大地保證驗證框架的可擴展性，為操作系統模塊化驗證提供了理論基礎。

1.2 形式化驗證工具

工具在降低操作系統自動化驗證難度、提高驗證開發的效率等方面起著重要作用。操作系統的驗證問題都將轉成定理證明問題，解決定理證明問題最終依賴于定理證明器。目前廣泛應用于操作系統驗證的定理證明器有Z3[12]、Isabelle[13]和Coq[14]等。Z3是微軟著名的自動定理證明器，能夠對驗證條件進行自動證明。由于大部分證明性質的不可判定性，自動定理證明器只能證明有限的性質，更多的證明則要依賴于人機交互式定理證明器，如Isabelle和Coq等。Isabelle是由英國劍橋大學Paulson和德國慕尼黑技術大學Nipkow于1986年共同開發的基于高階邏輯的證明器。Isabelle用函數型語言ML編寫，使用自然演繹規則進行定理證明。證明驗證工作在元邏輯(meta-logic)提供的框架下展開，所以它能支持多種邏輯系統。Coq是法國國家信息研究所(INRIA)開發的一個基于高階邏輯的證明器，由OCaml語言和少量C語言編寫。最初來源于1984年Coquand等開發的一個綜合依賴類型和多態類型的系統[15]，并命名為構造演算(calculus of constructions，CoC)。后來經過擴展，增加了歸納數據類型算法公理化的一些良好性質，形成歸納構造演算(calculus of inductive co nstructions，CiC)。歸納構造演算賦予了Coq更強的表達能力。

可信編譯器(verified compiler)是另外一類有用的工具，它嚴格保證了源代碼和編譯之后機器碼之間的語義一致性，使在源碼層驗證的定理很容易擴展到機器碼層。如果驗證了用C語言編寫的操作系統源代碼，通過可信編譯器生成的相應機器碼也可以被認為是通過驗證了，這樣實現端到端的定理證明變得更加容易。法國國家信息研究所(INRIA)著名的可信編譯器CompCert C[16]可以將Clight[17]編譯成語義一致的PowerPC、ARM和x86匯編代碼。編譯器中大約90%的編譯器算法(包括所有優化和所有代碼生成算法)已經在Coq中被證明是正確的[18]。CompCertMC[19]和CASCompCert[20]是對CompCert的一個擴展，前者可以保證堆棧的有限性和細粒度的堆棧權限，后者是能夠對無競爭的并發Clight程序進行認證的單獨編譯。編程語言CakeML自帶了一個經過驗證的正確編譯器[21]。其他的有C Parser[22]和AutoCorres[23]工具的組合使用，可以自動將C程序轉換為語義一致的更高級別的monadic表示形式，簡化了C代碼的形式化驗證。VST-Floyd能夠提供一套半自動的策略，幫助用戶使用Verifiable C構建C程序的功能正確性證明[24]。

1.3 形式化語言

目前C語言是大多數操作系統的程序設計語言，但是C語言的操作性語義難以表達不同層次規約，特別是高層的抽象規約，驗證時必須要將C語言轉換成等價的形式化語言。驗證μC/OS-Ⅱ[25]時，先使用Coq歸納定義了C語言數據結構和程序語句等，再將μC/OS-Ⅱ的C代碼手動轉換成對應的Coq代碼進行驗證。DeepSpec聯盟[26]提倡的深度規約(deep specification)具有豐富、雙邊、形式化和靈活等基本性質。符合深度規約的編程語言與規約語言的界限不再明顯。mC2[27]的大多數內核代碼都是用ClightX[28]編寫的，ClightX是對Clight的一個擴展，兩者能夠支持絕大部分C語言的語法。

Haskell[29]和COGENT[30]是純函數式語言，能夠方便地在Isabelle/HOL中定義規約進行推理，在操作系統的形式化設計與驗證中使用也非常多，如seL4的性質驗證是基于Haskell編寫的原型系統[31]。作為函數式程序設計模型的lambda演算與自然推理系統這樣的證明演算之間具有相同的結構，因此不少人機交互定理證明器內核是用函數式語言編寫，這使得函數式語言在用定理證明器時具有更好耦合性。COGENT保持了C語言的操作性和精簡性特點，還能夠簡單地表示高層抽象規約，驗證高層抽象定理。COGENT代碼可以經過編譯器生成相同語義的C代碼。BilbyFs文件[32]系統就是使用COGENT語言設計編寫完成，并生成C代碼編譯運行。Coq 編寫的代碼也可以直接抽取出語義相同Haskell、OCaml等腳本。FSCQ文件系統[33]和DFSCQ文件系統[34]就是先通過Coq設計編寫，再自動抽取Haskell編譯運行。

2 操作系統驗證方法

2.1 操作系統精化關系驗證

操作系統的驗證很大一部分歸結為精化關系驗證，例如驗證操作系統進程調度無饑餓(starving-freedom)性質時，任何單個語句函數都不能直接推導出結論，需要更高抽象規約描述，具體的代碼實現與高層抽象規約對軟件行為的定義必須要保持一致(等價)。精化關系則是定義了不同抽象模型或者程序之間的等價關系。操作系統驗證要選擇合適的精化關系定義。精化關系對運行環境假設太強時，現實運行環境難以滿足假設條件，相反假設太弱時，精化關系沒有可組合性等良好性質，難以進行有效推理。當前應用較多的上下文精化關系從可觀測的角度對等價關系進行定義。它是指在任何上下文環境中A替代B不產生更多的行為，并且客戶程序觀察不到A與B的區別。上下文精化與線性一致性是等價的[35]，并發對象的功能正確性通常定義為線性一致性，因此操作系統在并發環境中的功能正確性證明等價于上下文精化關系的證明。實際上，從用戶角度來看，操作系統可以看作是為上層的應用提供一組API接口服務的抽象虛擬機。同時操作系統是運行在硬件層上，能夠提供資源管理等服務的一組中間件的總和。所以說操作系統的正確性就是要求無論應用程序是運行在抽象虛擬機上，還是運行在屏蔽硬件細節的中間件上，應用程序觀察不到兩者的區別。

操作系統的驗證往往包括了從設計到實現等多個不同抽象層的內容，通常在低層抽象模型進行推理證明是困難的，通過層次之間的精化關系證明，低層抽象模型性質證明問題可轉化為更加容易證明的高層抽象模型性質問題。

2.2 操作系統驗證路徑

操作系統形式化驗證基本的假設是硬件形式化模型的正確性和驗證性質形式化規約正確性。它們本身都是非形式化的，硬件模型正確性取決于真實芯片運行與模型模擬運行是否完全一致，規約正確性取決于人們對操作系統性質的定義是否符合其本意。兩者是聯系非形式化的現實世界與形式化的計算機世界的一個橋梁。從最上層的規約到最底層的硬件模型之間的形式化部分是操作系統形式化驗證的內容，如圖1所示。由于操作系統驗證工作量比較大，有時會選擇擴大上層或者底層的信任基，比如假設編譯器是正確的，以減少實際驗證工作量。

圖1 驗證路徑示意圖Fig.1 Schematic map of verification path

從操作系統規約開始自頂向下驗證操作系統，是將頂層用戶非形式化需求變成系統形式化規約，對系統的功能需求進行定義。對形式化規約建立抽象模型，通過定理證明驗證抽象模型的性質。從CPU機器碼模型開始自底向上驗證操作系統，根據CPU硬件指令構造機器碼形式化模型，再通過建立逐步精化的模型不斷向上層抽象，最終證明系統滿足某些性質。安全性(safety)是指“不好”的事情(如多個進程進入臨界區)從不發生，活性(liveness)是指“好”的事情(如進程申請進入臨界區)最終一定會發生，Alpern等[36]證明了任何性質均可以表示成2種性質的交。功能正確性是指代碼正確實現了規約的功能。這幾種性質往往是操作系統驗證的關鍵性質。

無論自頂向下還是自底向上的驗證途徑，最終目標是驗證機器硬件的最終實現與用戶規約的一致性，并以此為基礎證明系統滿足某種性質，即證明定理成立。

2.3 大規模軟件驗證

形式化驗證的工作量非常大，整個過程需要人工參與較多，特別是在操作系統這樣大規模驗證中問題更加突出。seL4項目中，約8 600行C代碼的證明工作涉及20萬行Isabelle腳本代碼，花去了11人·a的工作量。與軟件工程解決大規模軟件開發問題相類比，產生了證明工程的概念，引入軟件工程的思想和經驗，可以應用于解決一部分形式化方法中大規模驗證的問題。在軟件工程的關注點分離等原則的啟發下，驗證過程中很自然地引入了分層、模塊化和復用等方法技術。

操作系統內核函數調用關系錯綜復雜，局部微小的變動可能影響整個系統。通過認證的方式將操作系統驗證分為多個模塊，減少單個模塊驗證的難度，同時將變動帶來的影響限制在模塊內。復用已經證明過的結果，可以盡量減少重復勞動，將已經驗證的模塊或者常用證明結論形成定理庫，比如Coq的Iris[37]是一個高階并發分離邏輯庫，支持推理操作系統并發程序的安全性。工具能夠提高驗證開發的效率，大量減少驗證腳本工作量，CSIRO的data61為操作系統的形式化驗證開發了一系列相關工具，覆蓋驗證工作的各個階段[38]。DeepSpec項目也在致力于開發適用于形式化驗證的一整套工具鏈。

另外，在操作系統實際驗證過程中，選用微內核操作系統作為驗證對象是減少驗證規模的一個重要方法。以Linux為代表的宏內核代碼量早已突破1 000萬行，seL4等大多數微內核代碼都不到1萬行。從信任基最大限度地縮小和系統安全性等角度，選擇微內核進行形式化驗證也有著較為明顯的優勢。目前操作系統驗證工作取得一定成果的seL4、mC2、PikeOS[39]、μC/OS-Ⅱ等也都是微內核架構。

3 操作系統形式化驗證研究現狀

3.1 Verve

2010年，微軟基于類型化匯編語言(TAL)[40]和Hoare邏輯自動化驗證了Verve的類型安全和內存安全[41]。完整的Verve由硬件抽象層Nucleus、內核和應用程序組成。Nucleus由TAL編寫，提供對硬件和內存的原語訪問，實現內存分配、垃圾收集、多堆棧、中斷處理和設備訪問等功能。內核是在Nucleus之上構建的更完整的高級別內核服務，例如搶占線程等，內核是用C#語言編寫并最終編譯成TAL。

驗證過程中，所有驗證代碼最終編譯成TAL，在TAL中手工注釋(hand-annotating)前置條件、后置條件和循環不變量斷言，再由Boogie[42]驗證器根據注釋的安全性和正確性規范進行自動驗證。Boogie驗證器底層默認的是一個Z3求解器，檢查斷言是否可滿足。

Verve是第一個證明了類型安全和內存安全的操作系統，證明的自動化程度非常高，但是類型安全和內存安全屬于比較弱的性質。如果希望證明結論更有價值，通常需要證明更加強的性質，如功能正確性的證明。

3.2 PikeOS

2009年，德國Verisoft XT團隊應用VCC[43]驗證了PikeOS系統內核一個改變線程優先級的系統調用p4syscall_fast_set_prio的功能正確性，該系統調用跨越了PikeOS內核所有層次，從硬件相關層次到用戶接口層次[44]。VCC是微軟等研發的一個用C語言開發的工業級驗證框架，支持通過添加輔助代碼(auxiliary code)和輔助狀態(ghost states)驗證底層并發的C 程序。驗證過程中，VCC把C代碼轉換成中間驗證語言Boogie，然后再轉換成驗證條件，最后由Z3實現定理證明或者給出反例。

同年，Verisoft XT團隊應用VCC框架形式化驗證了Microsoft的多處理器虛擬機軟件Hyper-V，Hyper-V總共包含了10萬行并發C代碼和5 000行匯編代碼。VCC對Hyper-V中20%的代碼進行了函數合約(function contract)和類型不變量等方面的驗證[45]。

Verisoft XT團隊在操作系統驗證方面做了小規模嘗試，驗證了操作系統PikeOS和Hyper-V的部分代碼的部分性質。驗證工作VCC底層使用Z3，具有相對較高的自動化程度，但是其表達和證明能力有所不足，存在一定的局限性。驗證的代碼只占整個操作系統很少的一部分，而且也并未驗證Hyper-V的功能正確性等重要屬性。

3.3 seL4

2009年，NICTA的seL4團隊(現在是CSIRO的Data61部門的Trustworthy Systems團隊)驗證了高性能操作系統seL4微內核的功能正確性和安全屬性。seL4包括8 600行C代碼和600行匯編代碼。通過形式化驗證，證明了seL4不會有內存泄漏、空指針訪問、算術異常等問題。

驗證過程中將seL4自頂向下分為3個層次。最上層MA是抽象層規約，描述了系統全部行為。這一層包含了系統外部接口足夠多的細節，定義了系統能做什么。中間層ME是執行層規約，它是一個可執行模型，也是一個實現，包括了所有數據結構和實現細節的描述。中間層是最上層的細化，進一步描述了系統怎么做。最底層MC是seL4的C實現，包含了所有具體實現的細節。系統設計和驗證中，中間層的Haskell原型是一個關鍵因素，它有效協調了形式化驗證和系統性能之間的矛盾。操作系統開發小組使用Haskell作為編程語言，形式化驗證小組將原型作為中間執行層導入定理證明器進行驗證。

系統主要性質通過精化關系來證明。將精化關系記為?，seL4的三層模型關系可以表示為MC?ME，ME?MA，根據精化的傳遞性質推出MC?MA。進一步說明了如果一個安全性質在抽象層成立，精化關系保證它在代碼實現層仍然成立。

這是首次用形式化方法對一個通用操作系統內核進行功能正確性的驗證。不過為了降低驗證難度，他們在驗證seL4的內核過程中，對內核中的IO、中斷和內存管理做了簡化處理，比如內核不支持帶有細粒度鎖的多核并發，回避了中斷和搶占導致的內核并發問題。2013年Tessin[46]將單核seL4證明結果擴展到基于BKL鎖的集群多核情況。

3.4 CertiKOS

抽象化、模塊化、層次化是操作系統軟件設計與實現的重要特征，耶魯大學的Flint團隊提出的開放邏輯框架可以將不同計算特征和跨越不同抽象級別的程序模塊驗證組合，解決了難以設計單一類型的系統或程序邏輯來驗證整個操作系統的問題。

2015年，Flint團隊基于深度規約和認證抽象層(certified abstraction layer)概念，通過分層的方法(將mCertiKOS分解成37層)，完成了對操作系統mCertiKOS單核的驗證工作。一般接口的實現者很好地為調用者隱藏了自己內部實現的細節，與通常這種“淺規約”(shallow specification)不同，深度規約需要調用者了解所有有關實現的信息，這些信息是調用者的上下文環境重要的組成部分。每個認證抽象層有足夠的信息使得性質的證明不再關心已被抽象的C語言或者匯編語言實現，可以更好進行逐層精化的證明。每個抽象層都可以證明相應的性質，并且在mCertiKOS將各個證明連接起來，復用了相同的證明。

2016年，以深度規約技術為基礎，Flint團隊利用CertiKOS構建并且驗證了一個細粒度并發多核操作系統mC2。CertiKOS是一個構建認證并發操作系統內核的可擴展框架，分為多個認證抽象層，將困難的驗證任務分解為多個簡單、可自動化的小任務。mC2包含了6 100行C代碼和400行x86匯編代碼，目前已經應用于地面無人車輛系統的虛擬機(hypervisor)。

相對seL4的證明，CertiKOS框架在于對細粒度鎖、真正并發的操作系統內核功能正確性驗證取得了進一步的突破，而通常認為并發程序的驗證比順序程序要困難得多。雖然mC2是細粒度鎖，但是在鎖期間，系統是在關中斷的環境下運行的，還不是搶占式操作系統。另外CertiKOS與mC2高耦合，使得CertiKOS不適用于已有操作系統內核的驗證。

3.5 μC/OS-Ⅱ

為了解決并發環境精化關系可組合性等問題，中科大-耶魯高可信軟件聯合研究中心2012年提出一種基于依賴-保證的模擬關系(rely-guarantee-based simulation，RGSim)作為通用的并發程序驗證手段，并對并發的垃圾收集(GC)等算法進行了驗證[47]。依賴-保證模擬關系僅僅保證2個外部程序外部可觀測行為之間的包含關系，不要求程序執行路徑集合之間具有包含關系。

2016年，他們基于依賴-保證模擬關系提出一個并發分離邏輯風格的并發精化程序邏輯(CSL-R)，構造了一個并發的上下文精化驗證框架，驗證了μC/OS-Ⅱ的中斷處理、任務調度、消息隊列、信號量和互斥鎖等模塊，證明了該系統互斥鎖不會發生優先級反轉(priority-inversion-freedom，PIF)。一共驗證了1 400行左右的C代碼，同時將涉及的匯編代碼封裝為原語的方式完成底層內核代碼的建模，驗證的函數覆蓋了μC/OS-Ⅱ中68%的常用函數。他們的驗證框架同樣也通過分層的方法，分別定義了底層機器模型和高層機器模型，并驗證了底層和高層之間的精化關系。驗證框架中開發了一系列自動證明策略，大幅度減少了證明腳本量。

這是首次構造了一個可以支持嵌套中斷和搶占操作系統內核的驗證框架，并驗證了商用操作系統部分內核模塊。目前驗證工作還未實現對μC/OS-Ⅱ內核代碼全覆蓋。匯編代碼部分封裝成原語，因此沒有驗證任何匯編代碼，相對CertiKOS對匯編代碼的驗證工作，缺少了端到端的相關性質定理的驗證。幾項主要的操作系統驗證工作比較見表1。

表1 操作系統驗證工作比較

3.6 其他相關工作

2008年Myreen[48]基于Hoare邏輯和VCG(verification condition generation)在機器碼層對LISP語言解析器(interpreters)進行了驗證。Hou等[49]基于LEON3 CPU指令集建立了一個形式化模型。Zhao等[50]定義了一個安全模型，通過驗證不變量，發現了ARINC653標準存在端口ID泄露、進程ID泄露等6個安全問題。ARINC653是國際航空電子工程委員會起草的航空應用標準軟件接口，定義了隔離微內核的標準規約。Nelson等[51]使用Z3求解器，實現了Hyperkernel內核全部自動化驗證，不過所有循環語句都被移出了內核，大大降低了內核的復雜度。2018年，他們使用Z3求解器實現了Nickel框架，可以用來設計驗證內核接口無隱蔽信道[52]。

作為操作系統最重要的組成部分，文件系統的驗證工作也有不少研究。Amani等[32]用COGENT分別寫了Linux兩個文件系統的實現，并進行了驗證。Chen等[34]驗證了FSCQ文件系統，并證明了FSCQ在系統任何時候都可以重啟，恢復數據后保證不會丟失數據。

4 操作系統形式化驗證存在的問題

4.1 軟件復雜度高

操作系統是最復雜的軟件之一，它大多用C語言內嵌匯編語言實現，還包含許多難以分解的相互依賴的組件和程序模塊。C語言中混合匯編語言還需要進行寄存器和棧的操作，導致語義非常復雜。從代碼量上看，應用最為廣泛的Linux操作系統內核代碼量早已突破千萬行。微內核與宏內核相比，雖然最大程度地減小了內核代碼量，但是內核不同部分之間相互依賴性卻提高了很多。

內核的并發使得代碼執行具有了不確定性。當用戶和I /O并發執行時，涉及控制權從一個線程轉移到另一個線程的控制機制。細粒度鎖的多核并發需要復雜的自旋鎖實現。這些并發機制的構造都很復雜，執行結果不確定，更難進行推理驗證。與此同時，用戶關心的常常是整個系統在運行過程中一直保持的全局性質，因此驗證過程很可能要涉及操作系統的全部代碼。

內核功能復雜性、并發的不確定性和驗證性質的全局性的結合使得對操作系統功能正確性等性質的形式化驗證變得十分困難。

4.2 驗證工作成本高

一方面，雖然通過各種方法降低了操作形式化驗證的工作量，但是總體來說仍然居高不下，驗證1行C代碼平均需要25行左右的證明代碼。操作系統軟件本身代碼量比較大，需要進行驗證的工作量更大。以μC/OS-Ⅱ 系統內核的驗證為例，1 400行C代碼用了22萬行Coq腳本代碼，其中包括驗證框架約6萬行，證明庫約11萬行，代碼證明約4萬行，證明策略約1.5萬行，共約6人·a的工作量。而這樣的工作量在操作系統形式化驗證項目中并不少見。

另外一方面軟件工程實踐對形式化接受度不高，一般項目很少通過形式化規約定義軟件，因此形式化驗證工作只有全部依賴于非常專業的人員。專業人員除了需要具有深厚的形式化理論功底，豐富的證明工具使用經驗，還要對驗證的軟件有深刻的了解，過高的門檻使得這樣的專業人員非常稀缺。

此外，操作系統需要不斷升級以支持適應新的硬件平臺和應用程序，版本升級帶來部分源代碼的改動有可能會導致重新驗證系統的巨大工作量。

4.3 驗證工具局限性

操作系統形式化驗證過程中，大量證明工作需要專業人員通過形式化工具完成。研究人員希望工具能夠自動化完成大部分證明工作，也希望工具能有強大的表達能力，能夠描述操作系統復雜的性質，但是工具的自動化程度與表達能力強弱往往成反比。如Z3等約束求解器可以對驗證條件自動求解，具有較高的自動化程度，但是它很難完成操作系統復雜數據結構和軟件功能正確性的全部驗證。Coq和Isabelle/HOL等人機交互定理證明助手能夠使用表達更為豐富的高階邏輯，但是需要手工輸入腳本的工作量比較大。一階以上的高階邏輯公式有效性和可證性都是不可判定的，即定理在證明出來之前是無法知道是否可證，更無法找出通用的方法進行自動證明。不可判定性在理論上決定了定理證明工具在自動化方面的局限性。

可信編譯器等工具為實現操作系統從抽象規約到執行代碼一致性的證明發揮了重要作用。這類工具既要保證源代碼和生成代碼的語義一致性，還要盡可能考慮優化生成代碼執行效率，往往兩者難以兼顧。另一方面，編譯器優化太復雜，算法很難被認證，其他非形式化的部分也難以驗證。認可度較高的可信編譯器CompCert編譯生成的代碼運行速度平均比GCC編譯生成的代碼要慢15%左右。通過CompCert編譯產生的目標機器碼，因為性能問題就很難被工業界實際廣泛使用。函數式語言COGENT能夠較好地描述操作系統高層抽象性質，但是COGENT編譯器在生成C代碼時幾乎沒有進行優化，其實用性還有待檢驗。

5 結 語

操作系統形式化驗證從最基本的類型安全等較弱的屬性到現在驗證功能正確性，高層抽象規約與底層代碼精化關系證明，其巨大進步得益于形式化驗證技術和工具的發展。同時，軟件的形式化驗證技術和工具的局限性也在制約著操作系統形式化驗證工作走向最終的工業實用和普及。對這些技術和工具的研究創新，將在未來一段時間操作系統形式化驗證中占有重要位置。

采用模塊化驗證，將復雜的操作系統分成多個更加簡單的模塊分別驗證，有助于減輕操作系統驗證的復雜度。構建驗證框架和驗證定理庫，增強驗證成果的復用，有助于減少驗證工作的重復勞動。通過強化學習和規則學習算法構建定理助手智能證明策略，可以加強定理助手在某些代碼和邏輯特征場景下的自動證明能力。

隨著相關技術和工具的逐步成熟，實現以操作系統形式化驗證為代表的證明工程工業普及與應用將成為可能，操作系統軟件系統的安全等問題也將從根本上得到解決。