嵌入式實時操作系統(tǒng)的形式化驗證

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

版塊 |鑒源論壇 · 觀模

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

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

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

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

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

01SeL4的形式化驗證

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

圖1 SeL4的形式化驗證框架

02PikeOS的形式化驗證

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

03mCertiKOS的形式化驗證

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

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

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

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

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

05μC/OS-II的形式化驗證

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

圖4 mC/OS II驗證框架

06ARINC653的形式化驗證

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

圖5 ARINC653形式化驗證框架

07AUTOSAR OS的形式化驗證

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

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

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

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

審核編輯：湯梓紅