操作系統(tǒng)形式化驗證綜述

錢漢偉,王承毅

(1.江蘇警官學(xué)院計算機(jī)信息與網(wǎng)絡(luò)安全系，江蘇 南京 210031; 2.江蘇科技大學(xué)理學(xué)院，江蘇 鎮(zhèn)江 212003)

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

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

1 形式化驗證技術(shù)

1.1 支撐理論和框架

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

1.2 形式化驗證工具

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

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

1.3 形式化語言

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

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

2 操作系統(tǒng)驗證方法

2.1 操作系統(tǒng)精化關(guān)系驗證

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

操作系統(tǒng)的驗證往往包括了從設(shè)計到實現(xiàn)等多個不同抽象層的內(nèi)容，通常在低層抽象模型進(jìn)行推理證明是困難的，通過層次之間的精化關(guān)系證明，低層抽象模型性質(zhì)證明問題可轉(zhuǎn)化為更加容易證明的高層抽象模型性質(zhì)問題。

2.2 操作系統(tǒng)驗證路徑

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

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

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

無論自頂向下還是自底向上的驗證途徑，最終目標(biāo)是驗證機(jī)器硬件的最終實現(xiàn)與用戶規(guī)約的一致性，并以此為基礎(chǔ)證明系統(tǒng)滿足某種性質(zhì)，即證明定理成立。

2.3 大規(guī)模軟件驗證

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

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

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

3 操作系統(tǒng)形式化驗證研究現(xiàn)狀

3.1 Verve

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

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

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

3.2 PikeOS

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

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

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

3.3 seL4

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

驗證過程中將seL4自頂向下分為3個層次。最上層MA是抽象層規(guī)約，描述了系統(tǒng)全部行為。這一層包含了系統(tǒng)外部接口足夠多的細(xì)節(jié)，定義了系統(tǒng)能做什么。中間層ME是執(zhí)行層規(guī)約，它是一個可執(zhí)行模型，也是一個實現(xiàn)，包括了所有數(shù)據(jù)結(jié)構(gòu)和實現(xiàn)細(xì)節(jié)的描述。中間層是最上層的細(xì)化，進(jìn)一步描述了系統(tǒng)怎么做。最底層MC是seL4的C實現(xiàn)，包含了所有具體實現(xiàn)的細(xì)節(jié)。系統(tǒng)設(shè)計和驗證中，中間層的Haskell原型是一個關(guān)鍵因素，它有效協(xié)調(diào)了形式化驗證和系統(tǒng)性能之間的矛盾。操作系統(tǒng)開發(fā)小組使用Haskell作為編程語言，形式化驗證小組將原型作為中間執(zhí)行層導(dǎo)入定理證明器進(jìn)行驗證。

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

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

3.4 CertiKOS

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

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

2016年，以深度規(guī)約技術(shù)為基礎(chǔ)，F(xiàn)lint團(tuán)隊利用CertiKOS構(gòu)建并且驗證了一個細(xì)粒度并發(fā)多核操作系統(tǒng)mC2。CertiKOS是一個構(gòu)建認(rèn)證并發(fā)操作系統(tǒng)內(nèi)核的可擴(kuò)展框架，分為多個認(rèn)證抽象層，將困難的驗證任務(wù)分解為多個簡單、可自動化的小任務(wù)。mC2包含了6 100行C代碼和400行x86匯編代碼，目前已經(jīng)應(yīng)用于地面無人車輛系統(tǒng)的虛擬機(jī)(hypervisor)。

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

3.5 μC/OS-Ⅱ

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

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

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

表1 操作系統(tǒng)驗證工作比較

3.6 其他相關(guān)工作

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

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

4 操作系統(tǒng)形式化驗證存在的問題

4.1 軟件復(fù)雜度高

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

內(nèi)核的并發(fā)使得代碼執(zhí)行具有了不確定性。當(dāng)用戶和I /O并發(fā)執(zhí)行時，涉及控制權(quán)從一個線程轉(zhuǎn)移到另一個線程的控制機(jī)制。細(xì)粒度鎖的多核并發(fā)需要復(fù)雜的自旋鎖實現(xiàn)。這些并發(fā)機(jī)制的構(gòu)造都很復(fù)雜，執(zhí)行結(jié)果不確定，更難進(jìn)行推理驗證。與此同時，用戶關(guān)心的常常是整個系統(tǒng)在運行過程中一直保持的全局性質(zhì)，因此驗證過程很可能要涉及操作系統(tǒng)的全部代碼。

內(nèi)核功能復(fù)雜性、并發(fā)的不確定性和驗證性質(zhì)的全局性的結(jié)合使得對操作系統(tǒng)功能正確性等性質(zhì)的形式化驗證變得十分困難。

4.2 驗證工作成本高

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

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

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

4.3 驗證工具局限性

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

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

5 結(jié) 語

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

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

隨著相關(guān)技術(shù)和工具的逐步成熟，實現(xiàn)以操作系統(tǒng)形式化驗證為代表的證明工程工業(yè)普及與應(yīng)用將成為可能，操作系統(tǒng)軟件系統(tǒng)的安全等問題也將從根本上得到解決。