作者 |郭建 上海控安可信軟件創新研究院特聘專家

版塊 |鑒源論壇 · 觀模

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

操作系統內核作為軟件系統的核心，確保操作系統內核的安全性與可靠性是構造高可信軟件最為關鍵的一步。采用形式化方法（Formal Methods）是實現操作系統安全可靠的途徑之一。形式化方法是采用數學化的方法、工具、技術對軟硬件系統進行研究、建立精確的模型，并驗證其是否滿足特定規范的方法。

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

操作系統內核是軟件系統的核心，操作系統內核可靠性直接影響著整個軟件系統的運行。然而操作系統的驗證仍面臨著諸多挑戰。

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

01SeL4的形式化驗證

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

圖1 SeL4的形式化驗證框架

02PikeOS的形式化驗證

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

03mCertiKOS的形式化驗證

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

圖2 基于混合語言的操作系統的驗證

04xv6操作系統內核的形式化驗證

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

圖3 Hyperkernel的開發流程

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

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

圖4 mC/OS II驗證框架

06ARINC653的形式化驗證

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

圖5 ARINC653形式化驗證框架

07AUTOSAR OS的形式化驗證

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

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

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

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

審核編輯：湯梓紅