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

丁繼政 上?？匕惭邪l(fā)中心研究員

版塊 | 鑒源論壇 · 觀模

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

01

操作系統(tǒng)內(nèi)核驗證框架

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

圖1 操作系統(tǒng)內(nèi)核自動化驗證框架

驗證工作分為兩個部分：在第一部分中，對由高層語言（如C語言）構(gòu)成的系統(tǒng)調(diào)用進(jìn)行驗證，通過自動化驗證工具VCC檢查系統(tǒng)調(diào)用的源代碼與其規(guī)范的一致性；在另一部分中，對由高層語言和底層語言（如C語言和匯編語言）構(gòu)成的內(nèi)核服務(wù)程序進(jìn)行驗證，通過將匯編語言轉(zhuǎn)換成抽象模型，并實現(xiàn)與C語言的粘合，形成符合基于C語言的驗證工具（如VCC）能夠接收的模型，再利用該工具驗證新混合代碼。

02

基于驗證框架的μC/OS-II內(nèi)核驗證

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

（1）C代碼內(nèi)嵌匯編的混合程序，即在C語言編寫的程序中調(diào)用匯編代碼；

（2）匯編內(nèi)嵌C混合程序，即在由匯編語言編寫的程序中調(diào)用C代碼。

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

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

2.1抽象模型的實現(xiàn)

匯編程序的抽象模型是包含狀態(tài)S、堆棧指針sp以及轉(zhuǎn)移關(guān)系δ的三元組。程序狀態(tài)S用Ghost結(jié)構(gòu)體MCF_c表示。MCF_c結(jié)構(gòu)體中的三個元素依次對應(yīng)了數(shù)據(jù)寄存器、地址寄存器和狀態(tài)寄存器，抽象模型的狀態(tài)S和堆棧指針sp的定義如下：

圖 2

在μC/OS-II通過只使用一個硬件指針實現(xiàn)了把即將運行的任務(wù)控制塊（OSTCB）的內(nèi)容從內(nèi)存區(qū)域中加載到寄存器中，或者將當(dāng)前正在運行任務(wù)的內(nèi)容存儲到相應(yīng)的任務(wù)控制塊中。

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

_(typedef unsigned short MCF_B16t)

_(typedef unsigned long MCF_B32t)

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

抽象模型中的狀態(tài)轉(zhuǎn)移關(guān)系δ表示抽象模型執(zhí)行匯編語句前后狀態(tài)變化，狀態(tài)轉(zhuǎn)移關(guān)系的實現(xiàn)見表1。

表1狀態(tài)轉(zhuǎn)移的代碼實現(xiàn)

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

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

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

圖 3

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

圖 4

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

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

03

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

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

3.1 系統(tǒng)調(diào)用的驗證

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

表2系統(tǒng)調(diào)用性質(zhì)提取

系統(tǒng)調(diào)用的8個模塊列于表3的第一列中，相對應(yīng)的每個模塊中所驗證的系統(tǒng)調(diào)用個數(shù)列于表的第二列，每一個模塊所提取的性質(zhì)列在了表的第三列。在74個系統(tǒng)調(diào)用中添加了共653條性質(zhì)，并完成了驗證。

3.2 核心服務(wù)程序的驗證

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

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

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

04

總結(jié)

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

審核編輯 黃昊宇