作者 |郭建 上?？匕部尚跑浖?chuàng)新研究院特聘專家

版塊 |鑒源論壇 · 觀模

生活在信息時(shí)代的今天，信息技術(shù)的發(fā)展日新月異。軟件系統(tǒng)作為信息技術(shù)的核心，在軌道交通、汽車電子、醫(yī)療器械、航空航天等安全攸關(guān)領(lǐng)域有著廣泛的應(yīng)用。由于軟件安全的問題而導(dǎo)致的惡劣事件是屢見不鮮。2017年上半年的WannaCry勒索病毒全球大爆發(fā)，給全球超過150個(gè)國家、30萬名網(wǎng)絡(luò)用戶帶來了超過80億美元的損失。該病毒是由不法分子利用操作系統(tǒng)軟件的漏洞，入侵他人Windows，將大量重要資料進(jìn)行加密后，使得眾多受感染的用戶無法正常工作，影響巨大。

操作系統(tǒng)內(nèi)核作為軟件系統(tǒng)的核心，確保操作系統(tǒng)內(nèi)核的安全性與可靠性是構(gòu)造高可信軟件最為關(guān)鍵的一步。采用形式化方法（Formal Methods）是實(shí)現(xiàn)操作系統(tǒng)安全可靠的途徑之一。形式化方法是采用數(shù)學(xué)化的方法、工具、技術(shù)對(duì)軟硬件系統(tǒng)進(jìn)行研究、建立精確的模型，并驗(yàn)證其是否滿足特定規(guī)范的方法。

目前軟件的形式化驗(yàn)證技術(shù)有模型檢測(cè)和定理證明，每種驗(yàn)證方法都有各自的特點(diǎn)。模型檢測(cè)是將軟件系統(tǒng)建立有限狀態(tài)機(jī)模型，通過自動(dòng)搜索有限狀態(tài)空間和路徑來驗(yàn)證模型與規(guī)范是否保持一致。模型檢測(cè)的優(yōu)勢(shì)在于其自動(dòng)化，易于被工業(yè)界接受，但缺點(diǎn)也是很明顯，隨著狀態(tài)和路徑的增加，則會(huì)出現(xiàn)狀態(tài)爆炸問題。定理證明技術(shù)是站在數(shù)學(xué)邏輯的角度對(duì)軟件系統(tǒng)進(jìn)行描述，利用數(shù)學(xué)推導(dǎo)演繹規(guī)則對(duì)軟件系統(tǒng)進(jìn)行證明。定理證明優(yōu)點(diǎn)在于能對(duì)系統(tǒng)進(jìn)行精確的描述，相較于模型檢測(cè)技術(shù)不存在狀態(tài)空間爆炸問題，缺點(diǎn)是自動(dòng)化程度低，要求驗(yàn)證工程師需具有較高的數(shù)學(xué)邏輯功底。

操作系統(tǒng)內(nèi)核是軟件系統(tǒng)的核心，操作系統(tǒng)內(nèi)核可靠性直接影響著整個(gè)軟件系統(tǒng)的運(yùn)行。然而操作系統(tǒng)的驗(yàn)證仍面臨著諸多挑戰(zhàn)。

近些年來，學(xué)術(shù)界有諸多的研究將形式化方法運(yùn)用到操作系統(tǒng)驗(yàn)證的工作中，目前已經(jīng)取得了一定的研究成果。比較著名的有澳大利亞研究中心NICTA的SeL4項(xiàng)目、由德國聯(lián)邦教育與研究部資助的Verisoft項(xiàng)目和它的后續(xù)項(xiàng)目Verisoft-XT項(xiàng)目、美國耶魯大學(xué)Zhong Shao團(tuán)隊(duì)組成的Flint研究組關(guān)于操作系統(tǒng)內(nèi)核的驗(yàn)證，以及華盛頓大學(xué)Hyperkernel的項(xiàng)目。國內(nèi)關(guān)于操作系統(tǒng)內(nèi)核的形式化驗(yàn)證研究也是發(fā)展非常迅速，包括浙江大學(xué)、中科大、北航、中科院、華師大等多所高校研究所都做出了貢獻(xiàn)。

01SeL4的形式化驗(yàn)證

在2009年，澳大利亞的SeL4項(xiàng)目組宣稱世界上第一個(gè)成功完成了對(duì)操作系統(tǒng)內(nèi)核的完全形式化驗(yàn)證，在同年該項(xiàng)目組關(guān)于SeL4的論文被評(píng)為了當(dāng)年計(jì)算機(jī)頂級(jí)會(huì)議（SOSP）的最佳論文，是世界上首個(gè)通過正規(guī)機(jī)器檢測(cè)證明的通用操作系統(tǒng)，這對(duì)形式化領(lǐng)域和操作系統(tǒng)領(lǐng)域具有重大的開創(chuàng)意義。SeL4的驗(yàn)證框架如圖1所示[1]，項(xiàng)目組首先使用Isabelle工具寫出IPC、Syscall調(diào)度等為內(nèi)核對(duì)象的抽象規(guī)范；然后使用Haskell寫出可執(zhí)行規(guī)范，運(yùn)用狀態(tài)機(jī)原理，對(duì)于第一步中抽象規(guī)范的每一步狀態(tài)轉(zhuǎn)換，Haskell寫出的可執(zhí)行規(guī)范都能產(chǎn)生唯一對(duì)應(yīng)的狀態(tài)轉(zhuǎn)換；最后通過由SML編寫的C-Isabelle轉(zhuǎn)換器和Haskabelle聯(lián)合形式證明C代碼和第二步由Haskell定義的語義保持一致。

圖1 SeL4的形式化驗(yàn)證框架

02PikeOS的形式化驗(yàn)證

德國的Verisoft項(xiàng)目[2]組提出了一個(gè)命名為CVM的驗(yàn)證框架，通過CVM驗(yàn)證框架驗(yàn)證了一個(gè)實(shí)際運(yùn)行的操作系統(tǒng)內(nèi)核。該驗(yàn)證框架包括了較為完整的操作系統(tǒng)組件、內(nèi)存、外設(shè)、處理器的形式化語義以及通過驗(yàn)證的C0編譯器。操作系統(tǒng)的主要部分都是由C0語言編寫的，運(yùn)用霍爾邏輯將由C0編寫的內(nèi)核代碼和應(yīng)用代碼在源代碼層上進(jìn)行驗(yàn)證。Verisoft- XT項(xiàng)目使用由微軟研究院研發(fā)的推理證明工具VCC對(duì)PikeOS進(jìn)行了形式化的驗(yàn)證，通過在源代碼層面上添加注釋代碼（Annotated Code）可用來驗(yàn)證并發(fā)的C代碼程序。

03mCertiKOS的形式化驗(yàn)證

美國耶魯大學(xué)Flint研究組是在Zhong Shao研究團(tuán)隊(duì)的帶領(lǐng)下一直研究對(duì)操作系統(tǒng)進(jìn)行形式化驗(yàn)證。研究團(tuán)隊(duì)運(yùn)用Coq工具對(duì)其自行開發(fā)的mCertiKOS操作系統(tǒng)進(jìn)行了端到端的完整的形式化驗(yàn)證[3]，其中mCertiKOS是特定為了用于形式化驗(yàn)證而從CertiKOS的基礎(chǔ)上進(jìn)行精簡(jiǎn)而來的。該項(xiàng)目組借助于CompCert編譯器的拓展版本CompCertX將C原語進(jìn)行可信編譯，采用分層抽象并在相關(guān)的抽象層上建立觀測(cè)函數(shù)的方法，將mCertiKOS內(nèi)核中的C和匯編的混合代碼進(jìn)行了完整的驗(yàn)證，其架構(gòu)如圖2所示。

圖2 基于混合語言的操作系統(tǒng)的驗(yàn)證

04xv6操作系統(tǒng)內(nèi)核的形式化驗(yàn)證

美國的華盛頓大學(xué)Hyperkernel項(xiàng)目則是基于對(duì)一個(gè)類Unix的教學(xué)操作系統(tǒng)名為xv6內(nèi)核的接口程序進(jìn)行了一鍵式的自動(dòng)化形式化驗(yàn)證，該項(xiàng)目組所驗(yàn)證的內(nèi)核代碼是由純C語言編寫而成的，包括了系統(tǒng)調(diào)用、異常處理和中斷代碼。首先去除掉了所有的循環(huán)和遞歸；其次內(nèi)核運(yùn)行在用戶空間下彼此分離的地址空間；然后他們將C語言代碼轉(zhuǎn)化為了中間表達(dá)語言LLVM；最后運(yùn)用Z3 SMT自動(dòng)求解器對(duì)LLVM語言上進(jìn)行端到端的全自動(dòng)化驗(yàn)證，其架構(gòu)如圖3所示。

圖3 Hyperkernel的開發(fā)流程

05μC/OS-II的形式化驗(yàn)證

中國科技大學(xué)的馮新宇團(tuán)隊(duì)，他們是國內(nèi)首個(gè)對(duì)一個(gè)商用的操作系統(tǒng)內(nèi)核μC/OS-II進(jìn)行了較為完整的形式化驗(yàn)證[4]，其驗(yàn)證框架如圖4所示。他們的工作采用了基于依賴/保證關(guān)系的并發(fā)程序證明方法，在保證多任務(wù)可組合的前提下，將多任務(wù)程序的精化證明分解為單任務(wù)的精化證明，從而減小了證明難度。對(duì)于內(nèi)核中的匯編程序，該工作將其封裝并抽象為高級(jí)語言（C 語言）原語。驗(yàn)證工作是在定理證明工具Coq中實(shí)現(xiàn)的，使用約22萬行驗(yàn)證腳本代碼驗(yàn)證了3450行操作系統(tǒng)內(nèi)核實(shí)現(xiàn)代碼。

圖4 mC/OS II驗(yàn)證框架

06ARINC653的形式化驗(yàn)證

北京航天航空大學(xué)趙永望團(tuán)隊(duì)建立了符合ARINC653的分區(qū)內(nèi)核模型，該模型實(shí)現(xiàn)了ARINC653的完整功能和接口，在該項(xiàng)目中他們采用了Event-B對(duì)系統(tǒng)所有的功能和服務(wù)進(jìn)行了形式化的建模，并利用精化方法和功能規(guī)范進(jìn)行了安全性分析與驗(yàn)證[5]，其架構(gòu)圖如圖5所示。采用基于精化的方法建立了兩層規(guī)范模型，其高層模型主要用來描述內(nèi)核初始化、分區(qū)調(diào)度、分區(qū)間通信等系統(tǒng)層面行為，精化模型則以進(jìn)程為單位，描述進(jìn)程調(diào)度和進(jìn)程管理等機(jī)制。他們的工作驗(yàn)證了ARINC 653標(biāo)準(zhǔn)和基于該標(biāo)準(zhǔn)的一些操作系統(tǒng)源碼的安全（Security）性，并發(fā)現(xiàn)了ARINC 653標(biāo)準(zhǔn)中潛在的進(jìn)程內(nèi)信息泄露等缺陷。

圖5 ARINC653形式化驗(yàn)證框架

07AUTOSAR OS的形式化驗(yàn)證

AUTOSAR規(guī)范是目前被廣泛應(yīng)用的車載操作系統(tǒng)規(guī)范之一，旨在為汽車電子體系架構(gòu)建立統(tǒng)一的開放工業(yè)標(biāo)準(zhǔn)。華東師范大學(xué)研究團(tuán)隊(duì)分別使用PAT、K框架等形式化驗(yàn)證工具對(duì)基于AUTOSAR規(guī)范的操作系統(tǒng)的總線通信協(xié)議、調(diào)度機(jī)制、中斷機(jī)制、內(nèi)存管理機(jī)制等部分進(jìn)行了驗(yàn)證。

研究團(tuán)隊(duì)采用基于時(shí)間的進(jìn)程代數(shù)對(duì)AUTOSAR操作系統(tǒng)總線協(xié)議進(jìn)行了形式化描述，并應(yīng)用PAT工具自動(dòng)化驗(yàn)證了總線協(xié)議的安全性、公平性、無饑餓性等性質(zhì)。

團(tuán)隊(duì)?wèi)?yīng)用K框架驗(yàn)證AUTOSAR操作系統(tǒng)中任務(wù)調(diào)度、中斷管理等模塊的實(shí)時(shí)特性。K是用于描述程序語言操作語義的形式化語言，通過定義操作語義可以執(zhí)行對(duì)應(yīng)的代碼，從而達(dá)到代碼分析與驗(yàn)證的目的。借用該思想，團(tuán)隊(duì)在K下定義了AUTOSAR中API的操作語義，進(jìn)而搭建了一個(gè)形式化的AUTOSAR系統(tǒng)，在該系統(tǒng)上可以“執(zhí)行”其應(yīng)用，分析與驗(yàn)證應(yīng)用的正確性。

作為基礎(chǔ)軟件的操作系統(tǒng)，其安全性將會(huì)影響到整個(gè)軟件系統(tǒng)的安全性，如何保證其安全性，本文從形式化方法的角度討論了目前國內(nèi)外的研究狀況。

審核編輯：湯梓紅