機載分區操作系統形式化建模及驗證研究

彭 寒，曹國震，吳曉葵

(西安航空學院 a.計算機學院；b.教務處，西安 710077)

0 引言

綜合模塊化航空電子架構(Integrated Modular Avionics，IMA)已成為當今航空、航天計算機的主流架構，其主要目標是實現分區操作系統，支持多個系統的時間分區和空間分區，以達到最大的資源利用率，減輕機載設備重量，減小飛機體積。機載分區操作系統為應用程序提供時空隔離的保障，從而實現故障隔離，避免故障傳播，并為不同安全級別的分系統提供物理上的隔離機制。為實現分區操作系統的標準化，美國航空無線電公司提出了機載分區操作系統實現規范——ARINC 653標準，旨在規定分區操作系統和機載應用程序之間的接口，以支持機載安全關鍵系統的開發認證和驗證。ARINC 653標準經過不斷的改進和完善，已經覆蓋了分區操作系統的核心服務、擴展服務、文件系統、測試驗證標準等各個方面。以ARINC 653標準為依據的各種分區操作系統也已得到了廣泛應用，例如，VxWorks653、INTEGRITY-178B，LynxOS-178，PikeOS和開源軟件POK及 Xtratum。

分區操作系統作為機載系統的重要基礎軟件，對其安全性、可靠性有著嚴苛的要求。由于分區操作系統的復雜性，其安全性往往難以通過測試和仿真來保證，根本原因在于軟件工程中的需求分析、設計和驗證通常采用非形式化語言來完成，而這種方式存在很大的二義性、模糊性，缺乏嚴格的數學證明。對于安全關鍵的機載分區操作系統，需要一種嚴格的、可靠的、實用的方法實現對復雜系統的管理。因此，在各種航空軟件安全性規范(如DO-178C)中，已經明確提出了要采用形式化方法對嵌入式系統進行建模和驗證。本文在國內外機載分區操作系統形式化建模及驗證研究工作的基礎上進行了分析總結，指出了當前該領域存在的問題，并提出了新的發展思路。

1 分區操作系統形式化建模與驗證研究現狀

分區操作系統的形式化建模通常是根據建模者的經驗，先設計抽象規約，然后逐步精化為底層模型，最終得到最貼近具體實現的精化模型。當前分區操作系統的形式化建模的研究包括分區操作系統的內核建模研究和分區操作系統規范的建模研究。

1.1 分區操作系統內核建模

Craig[1]使用自動化的建模與驗證工具Z Notations 設計并精化了一個較為完整的操作系統的內核，并證明了可以將其直接轉換為C語言的可執行代碼；而后，又進一步設計和精化了一個分區操作系統的內核，該內核提供了分區操作系統的大部分的功能。Craig使用定理證明方法對幾個內核屬性進行了基本的驗證，Craig設計的分區操作系統的形式化規約是一個較為完整的規約，其精化的級別已經達到了可以直接轉換為C代碼或者Ada代碼的程度。但是Craig的設計中沒有建立分區內進程的模型，另外，對于硬件設備的建模較為簡略，其形式化規約和正確性證明都是完全靠人工完成的。

Velykis在Craig研究的基礎上，考慮了更多的安全性需求， 使用自動化的建模與驗證工具Z Notations完成了分區操作系統的進一步的規約和驗證[2]，使用Z / Eves自動定理證明器對其形式化規約進行了驗證，消除了Craig的模型中的語法錯誤，并驗證了其API的可行性和健壯性，其改進的分區操作系統的形式化模型是完全使用定理證明器自動證明的。但是，Velykis的形式化規約中沒有涉及分區隔離方面的證明，其改進的的形式化模型側重于分區操作系統內核中的核心數據結構，例如進程表、隊列和調度程序，主要是改進了 Craig的調度器模型，并將調度器的某些行為屬性(如調度器死鎖分析)從非形式化的需求轉換為數學不變量來完成了證明。而對于其他組件，如消息傳遞或內存管理，則沒有使用自動證明。

Critical軟件公司的Andre使用形式化建模語言—B語言設計了一個安全的分區操作系統內核(secure partitioning kernel ,SPK)的形式化模型。其研究成果首先是完整的開發了SPK的頂層模型，完成系統的架構設計，并用ProB[3]工具進行了仿真和驗證。頂層的SPK抽象模型由內存管理、調度、內核通信、流策略、時鐘模型等組成。而后，經過驗證的頂層模型可以精化為完全形式化的精化SPK，并最終精化到可以從其自動生成C代碼的級別，這個精化過程是在Atelier B工具的協助下完成的。

Kawamorita 等人也應用B語言開發了安全的嵌入式設備上的分區操作系統內核OS-K，并在Intel的IA-32架構上搭建了該操作系統的原型[4]。Kawamorita使用B語言作為形式化模型的開發工具，并用Spin工具驗證了該模型的屬性，同時，他使用B4free工具自動驗證了模型的正確性和一致性。最終的分區操作系統內核提供了幾個核心的功能：分區管理、分區間通信、分區間通信的訪問控制、內存管理、定時器管理、處理器調度、設備驅動程序操作和中斷處理的I/O中斷同步。

Phelps等人使用Alloy語言設計了一個安全的分區操作系統的安全策略的形式化模型和頂級規約，并用分析工具驗證了該規約的一致性。該規約精化了分區間信息流策略模型，并且使用狀態轉換系統建立了兩個相互連接的分離的子系統，初始化時的子系統和運行時子系統。

Martin等人使用形式化規約開發軟件SPECWARE開發了MASK分區操作系統，并進行了三次精化[5]，其抽象規約主要涉及內核數據結構的規約，而最終的底層規約被手工翻譯成C源代碼。

為了保證Xenon分區操作系統的信息流安全性，Freitas和McDermott使用Circus建模語言建立了Xenon分區操作系統的形式化模型[6]。Murray 等人用Isabelle/HOL建模語言完成了對安全的分區操作系統內核seL4的建模和驗證，他們將seL4的規范用于驗證分區操作系統的信息流安全性，規范中定義了基于分區的輪轉調度策略，給每個分區分配了固定的時間窗口。歐盟EURO-MILS項目以PikeOS操作系統的精確建模和安全策略建模為目標，用Isabelle/HOL建模語言設計了一個通用的分區操作系統CISK(Controlled Interruptible Separation Kernel)的形式化模型，該模型包含了分區操作系統的幾個方面，例如中斷、分區之間的上下文切換和控制，其規約較為詳細，適用于工業系統的形式化驗證。Sanan等人在基于歐洲航天局的IMA for Space項目中，用 Isabelle / HOL建模語言構建了通用的分區操作系統內核的功能模型和安全模型。該規范使用ARINC 653作為功能需求，為了服務于最終的軟件實現，也涉及到了硬件虛擬化、CPU定時器和內存管理的模型。趙永望等人使用Isabelle / HOL建模語言設計了ARINC 653兼容的分區操作系統的頂層模型，其中考慮了ARINC 653的分區管理、分區調度和通信服務。

1.2 分區操作系統規范建模

由于分區操作系統規范的內核接口規范中規定了內核需要為應用程序提供的核心服務，對分區操作系統規范的建模需求也日漸迫切，因為形式化的分區操作系統接口模型能夠支持對分區應用程序的形式化建模與驗證。York大學的Gomes 用Circus建模語言建立了針對IMA系統的ARINC 653規范的形式化模型，Camara 等人對運行在ARINC 653兼容的分區操作系統之上的應用程序進行了建模和驗證[7]。北京航空航天大學的趙永望等人使用Event-B建模語言建立了ARINC 653第1部分的57項服務的系統功能的形式化模型，他們使用Event-B建模語言中的精化結構將ARINC 653抽象模型逐步精化，并將ARINC 653的服務要求轉換為了底層模型。趙永望利用Event-B的邏輯推理的能力證明了該規范的三個隱藏的錯誤和不完整之處，是一個將Event-B建模語言用于復雜系統建模與驗證的很好的范例。

雖然目前已有對分區操作系統的形式化建模的研究，但是還沒有直接從某個分區操作系統的形式化模型直接生成可執行代碼的報告。

2 分區操作系統的形式化驗證

分區操作系統的形式化驗證通常是從已有的操作系統代碼中抽象出形式化模型，并驗證這個抽象模型的各種屬性。分區操作系統的形式化驗證主要包括對時間隔離能力和空間隔離能力的驗證，其中空間隔離能力指的是數據的隔離，也就是數據存儲和數據通信的分離，即不能有非法的、不安全的訪問和分區間的故障傳播。分區的時間隔離能力則確保了共享資源為分區中的軟件提供的服務不會受到其他分區中的軟件的影響，包括計算資源的性能、調度資源的速率、延遲、抖動和持續時間。

2.1 空間隔離能力驗證

Baumann 等人在一個航空電子項目的子工程中用VCC驗證工具驗證了PikeOS分區操作系統源代碼的所有系統調用功能，也就是內核提供給應用程序的核心服務的正確性。他們提出了頂層抽象模型和底層實現的操作系統及應用程序構成的系統之間的模擬關系定理，并識別出了為保證分區操作系統內核的整體正確性而需要所有組件所具備的屬性。因為建立在PikeOS分區操作系統源代碼上的安全關鍵系統依賴于空間分離機制的正確實現，所以對它的驗證必須考慮內存隔離的正確性。因此，Baumann等人使用VCC工具對PikeOS分區操作系統的關鍵組件，即內存管理器進行了源代碼的級別的驗證。

Richards對格林希爾公司的商業化分區操作系統INTEGRITY-178B進行了安全性驗證[8]，其驗證考慮了五個要素：(1)描述系統相關安全屬性的形式化規約；(2)系統功能性接口的形式化表示；(3)系統高層設計的半形式化表示和抽象表示；(4)系統低層設計的半形式化的、詳細的表示；(5)用來表示上述四個要素對之間的對應關系的模型。該系統被建模為狀態轉換系統，它接收系統的當前狀態以及任何外部輸入作為輸入，并產生新的系統狀態以及任何外部輸出。Richards采用這種方式驗證了INTEGRITY-178B的高層模型信息流安全性，系統的低層設計采用ACL2定理證明器建模，并保證了ACL2模型與C代碼的對應性。

基于ARM的嵌入式分區操作系統PROSPER的內核由150行匯編代碼和600行C代碼組成，Dam通過證明抽象規約和內核二進制代碼之間的相互模擬關系，對PROSPER的信息流安全性進行了形式化驗證，其系統模型僅考慮分別在兩個獨立的特殊ARMv7機器上執行的兩個分區，分區間通過異步消息傳遞進行通信，最終驗證了除了通過指定的通信通道之外，分區之間不會有任何直接或間接地影響。具體做法是確保除了通過顯式使用預先指定的通道來實現通信外，分區間無法通過讀/寫其他分區的內存、寄存器的內容來訪問其它分區。

2.2 時間隔離能力驗證

時間隔離需要用分區操作系統的調度器來實現，因為它負責將處理器時間分配給分區。根據ARINC 653標準，時間分離需要兩級調度器，分別為分區級調度器和進程級調度器。

霍尼韋爾動態執行操作系統(Dynamic Enforcement Operating System，DEOS)是一個基于微內核的實時操作系統，通過在進程級別提供空間隔離和在線程級提供時間分區來支持靈活的IMA應用程序。NASA與霍尼韋爾合作，將DEOS的調度內核的核心部分包含10個類，超過1000行的C++代碼翻譯成Promela，并在Spin模型檢測工具中進行了驗證[9]。他們使用兩種方法來分析DEOS內核中的時間隔離屬性。第一種方法是建立程序變量的斷言以識別潛在的錯誤。如果模型檢查器發現了斷言背離，則可以仿真所報告的錯誤的執行路徑，并且可以確定這個路徑是否真的是錯誤的執行路徑。第二種方法是使用LTL表達的活性屬性Idle Execution，其形式為(beginperiod->(！endperiod U idle))。這個活性屬性表示如果系統中有時間松弛(即主線程沒有100%的CPU利用率)，則空閑線程應該在每個最長的周期內運行，這是時間隔離的必要條件。該系統的大小和復雜性限制了它們一次只能分析一個配置。為了克服這個局限性，Ha等人使用定理證明的方法將DEOS的驗證推廣到任意配置，利用PVS定理證明器來分析DEOS調度器。他們使用離散時間狀態轉換系統對PVS中的調度器的操作和DEOS的執行時間線建模，時間隔離屬性被建模為狀態集合上的謂詞，并被證明適用于所有可達到的狀態，整個理論模型共有1648行PVS代碼和212個引理。除了時間隔離不變量的歸納證明之外，他們還使用基于特征模型的技術來模擬狀態轉換系統并確定歸納不變量，這種技術對于漸增復雜度的系統的增量式的定理證明非常適用。

Asberg等人使用時間任務自動機對WindRiver的分區操作系統VxWorks進行建模，并使用Times工具對其進行了驗證。他們使用時間任務自動機建立了全局調度器、分區內本地調度器和事件處理程序的模型，用事件處理程序模型將全局調度器和分區個數的變化解耦。Asberg用時間計算樹邏輯TCTL建模了分區內局部調度器和全局調度器應滿足的安全性需求，例如“當分區處于活動狀態時，分區內任務就緒隊列中優先級最高的任務應始終是服務器當前正在運行的任務”。

2.3 討論

通過對國內外分區操作系統形式化建模與驗證技術研究現狀的分析，我們可以發現，大多數對空間隔離能力進行的建模和驗證都采用了定理證明的方法，原因在于模型檢查方法由于其狀態空間爆炸問題無法完整地驗證操作系統的所有可能執行路徑，并且很難用屬性建模語言(如LTL和CTL)表達空間隔離屬性。反之，驗證時間隔離屬性時，通常會使用模型檢驗方法，這是因為在各種模型檢查器中可以很方便地表達時間屬性，例如UPPAAL工具中的時間自動機。

3 現有建模及驗證研究中存在的問題

雖然國內外研究人員已在分區操作系統建模及驗證方面做了一定的工作，但是這些研究目前尚存在下述問題。

3.1 驗證工作的不充分性

目前分區操作系統驗證的工作通常是對已有的操作系統代碼的“設計后驗證”，所驗證的模型僅僅是實際系統的一個抽象，只能體現系統的可能行為，而不是全部行為。這種方法最大的問題在于必須保證抽象出來的形式化模型與原來的源代碼的行為是一致的，而事實上，無論這個抽象過程是自動的還是人工的，都無法避免不一致性。因此，這些驗證工作是不充分的。

3.2 建模與驗證方法的單一性

目前已有的分區操作系統建模及驗證方法主要側重于建模或者驗證系統的某個方面的屬性，很少能夠完整地覆蓋多個方面的屬性建模和驗證需求。例如，Event-B、B、Z等基于數據精化的建模語言主要注重于保證模型精化的一致性，而無法對各種時態邏輯屬性進行驗證。時間自動機、狀態轉換系統等工具可以很方便的建模和驗證模型的行為特性，而對于數據精化方面的支持則比較弱，缺乏同時考慮數據精化特性和行為屬性的形式化模型和驗證研究。

3.3 缺乏對交互環境的建模與驗證

當前的分區操作系統的形式化模型并沒有區分“環境”和“系統”，基本上都是將環境和系統放到一起，構成一個封閉的系統。所謂“環境”就是會和操作系統產生交互的系統，如硬件系統和應用軟件?，F有的研究成果或者是沒有考慮這些因素，或者是將這些因素作為了分區操作系統模型的一部分，混淆了系統所處的環境模型和系統本身的模型，這些模型對于驗證規范和標準是可行的，但對于需要根據模型生成最終代碼的工程師來說則是不可接受的。

4 分區操作系統建模及驗證的新思路

針對當前分區操作系統建模及驗證的研究工作中存在的問題，本文提出以下三種新的思路，以期對未來研究工作有所借鑒。

4.1 從“設計后驗證”到“Correct-by-Construct”方法

傳統的形式化方法只考慮了軟件壽命周期的需求規約階段和最終的測試驗證階段，而沒有控制中間的設計和實現過程。Correct-by-Construct方法是近年來學界所提倡的新的、更科學的形式化方法。其含義為“構建即正確”，即軟件的正確性應該是通過正確的“設計(構建)”來保證的，而不是通過驗證來保證。Correct-by-Construct方法能夠從需求規約開始，逐步精化規約模型，得到設計模型，直到生成最終的實現代碼，并保證整個精化過程的正確性。對于安全關鍵的機載分區操作系統來說，必須采用這種方法“構建”出正確的分區操作系統。

4.2 從規約模型到契約模型

現有的分區操作系統模型未能區分系統模型和系統所處的“環境”的模型，完整的建模分區操作系統和其所處的“環境”的模型會讓模型的規模變得極為復雜也是不現實的。因此，可以采用契約式設計與驗證的思路，建立系統和環境的“契約”，有效地分離系統模型和環境模型，即定義系統和環境之間的接口。只要分區操作系統滿足這個契約，就是可行的實現方案。在實際操作的過程中，可以建立底層硬件應該滿足的行為的契約，甚至是分區操作系統的底層支撐操作系統所提供的接口模型作為分區操作系統的環境模型。

4.3 組合運用多種形式化建模方法

形式化建模語言因其專用性的特點，很難同時考慮系統的多方面的屬性建模與驗證。例如，某些建模語言主要擅長建模系統的行為方面的屬性，而另一些建模語言則專注于時間屬性的建模。為應對這個問題，研究人員通常會根據實際需求對某些形式化建模語言進行擴充，使其能夠表達更多方面的屬性。但事實上是不存在能夠表達系統所有方面屬性的形式系統的，而且很多形式系統中有大量不需要的語法元素。一種比較靈活的且更為現實的做法是根據實際的系統建模與驗證需求，組合運用多種形式化方法，這樣，建模者只需要選擇合適的形式系統用來滿足建模和驗證需求，就可以將研究重點轉向系統模型的構建、精化和屬性驗證上。

5 結語

本文通過分析國內外關于機載分區操作系統建模及驗證方面的研究成果，指出了其研究工作中存在著驗證工作不充分性、建模與驗證方法單一性、缺乏對交互環境的建模與驗證等問題，并針對這些問題，提出了從“設計后驗證”到“Correct-by-Construct”、從規約模型到契約模型、組合運用多種形式化建模三種新的研究方法及解決方案，為進一步開展機載分區操作系統建模及驗證工作提供了指南。