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

丁繼政 上海控安研發中心研究員

版塊 | 鑒源論壇 · 觀模

操作系統作為軟件系統的核心，其安全性與可靠性是構造高可信軟件最為關鍵的一步。嵌入式實時操作系統因其具有并發、可搶占以及代碼復雜性的特征，給驗證工作帶來了巨大挑戰。我們提出了一種通用的自動化驗證框架，借助相關工具，使用本驗證框架可對由C語言和匯編語言實現的實時操作系統內核進行自動化驗證，從而實現C和匯編的混合代碼驗證的目標。

01

操作系統內核驗證框架

操作系統絕大多數都是采用C語言和匯編語言編寫的，對操作系統的驗證需要分析C語言、匯編語言和混合語言的驗證。我們以μC/OS-II為研究對象，提出了一個通用的自動化驗證框架，該框架如圖1所示。

圖1 操作系統內核自動化驗證框架

驗證工作分為兩個部分：在第一部分中，對由高層語言（如C語言）構成的系統調用進行驗證，通過自動化驗證工具VCC檢查系統調用的源代碼與其規范的一致性；在另一部分中，對由高層語言和底層語言（如C語言和匯編語言）構成的內核服務程序進行驗證，通過將匯編語言轉換成抽象模型，并實現與C語言的粘合，形成符合基于C語言的驗證工具（如VCC）能夠接收的模型，再利用該工具驗證新混合代碼。

02

基于驗證框架的μC/OS-II內核驗證

操作系統是對資源的管理，不可避免地需要對硬件資源進行訪問操作。為了提高效率，特別是在上下文切換、中斷機制中，通常得使用匯編語言。針對μC/OS-II內核代碼，存在兩種混合形態：

（1）C代碼內嵌匯編的混合程序，即在C語言編寫的程序中調用匯編代碼；

（2）匯編內嵌C混合程序，即在由匯編語言編寫的程序中調用C代碼。

為了實現對μC/OS-II內核代碼的驗證，這里使用自動化驗證工具VCC對抽象模型實現。

VCC是源代碼級并發C程序的自動化推理驗證工具，用于證明C語言程序功能規范的正確性。VCC工具鏈允許使用函數合約和數據結構的不變量對并發C程序進行模塊化驗證。函數合約由前置條件和后置條件指定。VCC是基于注釋的系統，即合約和不變量作為注釋插入在源代碼中，其方式對于常規的非驗證編譯器是透明的。

2.1抽象模型的實現

匯編程序的抽象模型是包含狀態S、堆棧指針sp以及轉移關系δ的三元組。程序狀態S用Ghost結構體MCF_c表示。MCF_c結構體中的三個元素依次對應了數據寄存器、地址寄存器和狀態寄存器，抽象模型的狀態S和堆棧指針sp的定義如下：

圖 2

在μC/OS-II通過只使用一個硬件指針實現了把即將運行的任務控制塊（OSTCB）的內容從內存區域中加載到寄存器中，或者將當前正在運行任務的內容存儲到相應的任務控制塊中。

MCF_B16t類型和MCF_B32t類型是我們自定義類型，它們分別對應了無符號16位整型和無符號32位整型，通過使用關鍵字typedef定義，如下：

_(typedef unsigned short MCF_B16t)

_(typedef unsigned long MCF_B32t)

抽象模型中的狀態S包括數據通用寄存器、地址通用寄存器和狀態寄存器，這三個成員在實現中分別對應于數組D[8]和A[8]和變量SR，抽象模型的堆棧指針sp對應于實現中的*SP。在Ghost語句中，使用了關鍵字ghost對指針*SP進行了定義。

抽象模型中的狀態轉移關系δ表示抽象模型執行匯編語句前后狀態變化，狀態轉移關系的實現見表1。

表1狀態轉移的代碼實現

2.2 C代碼和抽象模型的粘合

在μC/OS-II的內核代碼中，匯編程序和C程序分別定義在兩種不同類型的文件中。C語言定義的程序具有高移植性，匯編語言定義的程序可以對內核運行的硬件平臺進行訪問控制，內核的正常運轉離不開這兩種語言程序的協作運行。這兩種不同語言程序的協作是通過在各自程序中調用另一語言定義的函數完成的。

在VCC設計理念中，Ghost語言只存在于驗證過程中，不能夠直接影響原程序的執行。我們采用了Ghost代碼模擬了匯編程序的執行。但在OS實際運行過程中，匯編語言程序與C語言程序之間存在數據的交換。為了解決抽象模型Ghost代碼與C代碼數據交換的問題，提出了在純函數中添加VCC合約語句，見下面的代碼：

圖 3

通常在VCC中，函數入口處的前置條件和后置條件是函數應該滿足的性質。但是，在函數體不為空時，直接在驗證函數的入口處添加前置條件或后置條件，VCC認為該性質描述語句是重言式，然后可以通過Ghost語句將Assignment()的返回值賦給一個具體類型對象。例如，在C語言程序中的一個類型為無符號32位的StoreValue變量，需要將抽象模型中D0的值賦值給C語言的變量StoreValue，此時使用下列語句就可以實現匯編指令與C語言代碼的通訊：

圖 4

同理，也可以通過Ghost純函數Assignment()將具體變量的值傳遞給Ghost類型變量。借助在定義的Ghost純函數中添加斷言的形式，成功地模擬出C代碼和抽象模型之間的數據通訊。這樣，抽象模型的實現模擬了匯編指令的執行，并可以與C代碼一起在VCC上運行。

這部分給出了高層實現語言Ghost代碼的語法定義，通過該Ghost語言對抽象模型中三元組的各個元素進行了具體實現，最后介紹了如何將抽象模型的實現，以及抽象模型與內核中C代碼的粘合。

03

驗證μC/OS-II及其分析

我們運用前面提出的驗證框架驗證了基于μC/OS-II的商用實時操作系統內核，包括近8000行的C代碼和100多行的匯編代碼（去除空格和注釋），分為系統調用8個模塊的驗證和混合語言實現的核心服務程序的驗證。

3.1 系統調用的驗證

μC/OS-II內核中一共74個系統調用，在驗證過程中，根據需求，提取出每個系統調用需要滿足的性質，性質是基于Hoare邏輯的形式給出的，并采用VCC提供的合約或者斷言的形式，以注釋的方式插入到源代碼中。系統調用的驗證性質見表2。

表2系統調用性質提取

系統調用的8個模塊列于表3的第一列中，相對應的每個模塊中所驗證的系統調用個數列于表的第二列，每一個模塊所提取的性質列在了表的第三列。在74個系統調用中添加了共653條性質，并完成了驗證。

3.2 核心服務程序的驗證

μC/OS-II內核的核心服務程序是以混合語言（即C語言和匯編語言）實現，其中匯編語言完成有關中斷控制、上下文切換以及寄存器讀寫的操作。為了實現對混合語言程序的驗證，將匯編程序轉換為抽象建模，并在VCC中實現。而對性質的提取、性質的形式化描述與系統調用的方法是相同的。我們在驗證中是針對程序是否嚴格滿足所要求的需求規范進行分析驗證。如果滿足，則表示功能正確。反之，表示軟件存在缺陷。

驗證包括了13個C語言文件、2個頭文件以及1個匯編語言文件，共計6446行C語言程序和100行的匯編語言程序（除去了代碼中所有的注釋和空行），添加了936行性質驗證代碼和205行的抽象模型的代碼實現，抽象模型實現與匯編代碼的比例約為2:1。

μC/OS-II 內核總共驗證出10個缺陷，分布于7個功能函數中。

04

總結

本文提出了一個通用的嵌入式操作系統內核自動化驗證框架。該驗證框架支持對C語言程序和C語言與匯編語言混合程序的驗證。為了檢驗本框架的可行性，以商用實時操作系統μC/OS-II的內核作為研究對象，運用本驗證框架，通過驗證工具VCC，完成了該內核的系統調用及混合代碼的驗證。

審核編輯 黃昊宇