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

丁繼政 上海控安研發(fā)中心研究員

版塊 | 鑒源論壇 · 觀模

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

01

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

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

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

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

02

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

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

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

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

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

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

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

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

圖 2

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

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

_(typedef unsigned short MCF_B16t)

_(typedef unsigned long MCF_B32t)

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

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

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

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

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

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

圖 3

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

圖 4

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

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

03

驗(yàn)證μC/OS-II及其分析

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

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

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

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

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

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

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

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

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

04

總結(jié)

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

審核編輯 黃昊宇