SpaceOS中若干全局性質(zhì)的形式化描述和驗證

顧海博,付 明,喬 磊,馮新宇

1(中國科學技術(shù)大學 計算機科學與技術(shù)學院,合肥 230027)2(中國科學技術(shù)大學 蘇州研究院軟件安全實驗室,江蘇 蘇州 215123)3(華為上海研究所 2012實驗室-OS內(nèi)核實驗室,上海 201206)4(北京控制工程研究所,北京 100190)5(南京大學 計算機軟件新技術(shù)國家重點實驗室,南京210023)

1 引 言

如今計算機系統(tǒng)正在各行業(yè)各領(lǐng)域得到越來越廣泛的應(yīng)用.操作系統(tǒng)作為底層軟件平臺,是計算機系統(tǒng)穩(wěn)定運行的關(guān)鍵.國內(nèi)外由于操作系統(tǒng)軟件缺陷而導(dǎo)致的災(zāi)難和事故屢見不鮮.軟件工程中常用的軟件測試方法無法保證通過測試的軟件一定不存在缺陷和錯誤.相比之下,形式化程序驗證可以提供比測試更強的保障,它使用形式語言將軟件的正確性等性質(zhì)描述和定義為數(shù)學命題,并運用相應(yīng)的程序邏輯來證明命題的正確性.

航天領(lǐng)域是典型的安全攸關(guān)領(lǐng)域,保障航天器操作系統(tǒng)的安全可靠性具有重要意義.目前我國航天器上廣泛使用的是北京控制工程研究所研發(fā)的SpaceOS操作系統(tǒng)[1].SpaceOS在設(shè)計時,提出了一些系統(tǒng)應(yīng)滿足的全局性質(zhì),例如,系統(tǒng)中任務(wù)的優(yōu)先級必須始終處于指定的范圍內(nèi).這些性質(zhì)不只是單個模塊具有的,而是系統(tǒng)整體在運行過程中應(yīng)始終滿足的.形式化證明系統(tǒng)具有這些性質(zhì)是保證系統(tǒng)正確可靠的重要方法.目前國內(nèi)針對我國航天器系統(tǒng)軟件開展了多項形式化驗證工作,如文獻[10]驗證了SpaceOS的內(nèi)存管理模塊,文獻[3]驗證了用于我國登月著陸器的一個著陸控制程序,文獻[2]為月球車控制軟件進行了形式化建模,證明其滿足一個時間有關(guān)的關(guān)鍵性質(zhì).但這些工作要么著眼于單個內(nèi)核組件,要么針對的是具體應(yīng)用場景,尚缺乏對系統(tǒng)整體性質(zhì)的驗證.

由于操作系統(tǒng)本身的復(fù)雜性,當前絕大多數(shù)操作系統(tǒng)驗證工作的目標系統(tǒng)都是專為驗證項目本身而定制開發(fā),難以支持第三方獨立開發(fā)的操作系統(tǒng)的驗證,因此相關(guān)技術(shù)難以直接用來驗證SpaceOS.最近,Certi-μC/OS項目[7]開發(fā)了一個支持第三方操作系統(tǒng)的驗證框架,其高層建模部分能夠表達和驗證系統(tǒng)全局性質(zhì),為本文的工作提供了可能.本文基于該框架,為SpaceOS建立了抽象模型,在模型上驗證了若干與內(nèi)核任務(wù)管理和信號量相關(guān)的全局性質(zhì).本文的貢獻有:

1)為SpaceOS內(nèi)核狀態(tài)建立了抽象模型,描述內(nèi)核數(shù)據(jù)結(jié)構(gòu),為主要模塊的系統(tǒng)調(diào)用和中斷處理程序編寫了抽象規(guī)范.

2)擴展了Certi-μC/OS驗證框架,設(shè)計了一套證明全局性質(zhì)的推理規(guī)則,克服了原有框架對全局性質(zhì)驗證的支持不夠成熟、代價較高的問題.還開發(fā)了一組Coq證明策略,進一步提高證明效率.

3)結(jié)合需求說明文檔和源代碼,提取并形式化編碼了8條與內(nèi)核任務(wù)管理和信號量相關(guān)的全局性質(zhì),證明了SpaceOS滿足這些性質(zhì).所有建模和驗證工作都在Coq1中完成.

本文的驗證工作在抽象模型上進行,抽象模型上的性質(zhì)描述不依賴于具體實現(xiàn)細節(jié),這比直接在C語言代碼層面進行驗證更加簡單.本文建立的抽象模型還可用于內(nèi)核功能正確性的精化驗證,精化關(guān)系可以將抽象模型上驗證的全局性質(zhì)傳遞到C語言具體實現(xiàn)上.

相關(guān)研究工作

seL4項目[4]在驗證seL4內(nèi)核時,證明了150多個描述內(nèi)核性質(zhì)的不變式,如空閑任務(wù)始終處于空閑態(tài)等.這些不變式是作為內(nèi)核正確性精化驗證的一部分證明的,而本文的全局性質(zhì)驗證則可以獨立于精化驗證單獨進行.

Certi-μC/OS項目[7]設(shè)計和實現(xiàn)了一個支持搶占式內(nèi)核的操作系統(tǒng)驗證框架,并基于該框架驗證了商用實時操作系統(tǒng)μC/OS-II核心模塊的功能正確性.該項目還在高層抽象模型上證明了μC/OS-II的互斥信號量不會發(fā)生優(yōu)先級反轉(zhuǎn)(PIF),展示了驗證框架具有表達和驗證系統(tǒng)整體性質(zhì)的能力,但他們的證明需要對整個機器的執(zhí)行過程進行歸納推理,含有較多重復(fù)冗余步驟,并且約有1/4證明代碼是在證明操作語義相關(guān)的定理,自動化程度也不高.本文設(shè)計的全局性質(zhì)推理系統(tǒng),可以直接將證明模塊化分解到對每個內(nèi)核函數(shù)關(guān)鍵步驟的驗證上,避免歸納證明中的重復(fù)冗余步驟,不必關(guān)心操作語義的細枝末節(jié);同時,開發(fā)的Coq證明策略能夠自動完成一些證明中頻繁瑣碎的步驟.這些對驗證框架的擴展顯著提高了SpaceOS全局性質(zhì)的驗證效率.

Nelson等人開發(fā)和驗證了一個叫做Hyperkernel的操作系統(tǒng)內(nèi)核[5],展示了一套高效構(gòu)建和驗證操作系統(tǒng)內(nèi)核的方案.他們除了給內(nèi)核系統(tǒng)調(diào)用編寫數(shù)學規(guī)范外,還定義了另一種更高層次的聲明式規(guī)范(Declarative specification).這種規(guī)范著眼于描述橫跨多個內(nèi)核模塊的性質(zhì)[6],形式上比具體系統(tǒng)調(diào)用的功能規(guī)范更簡單易讀,能夠直觀體現(xiàn)內(nèi)核編寫者的思想和意圖,和本文的全局性質(zhì)是非常相似的.他們用Python語言來編碼規(guī)范,用自動定理求解器Z3完成證明,驗證自動化程度高,但代價是對內(nèi)核做出了特殊限制.例如,Hyperkernel的內(nèi)核接口在設(shè)計和實現(xiàn)時是必須是有限的,不能含有無限循環(huán)和遞歸,而SpaceOS中的一些復(fù)雜功能,如時鐘中斷需要遞歸遍歷系統(tǒng)中的一些數(shù)據(jù)結(jié)構(gòu),這是Hyperkernel無法表達和驗證的;Hyperkernel要求內(nèi)核接口的執(zhí)行是原子的,不能被打斷,以便模塊化獨立驗證各接口,而SpaceOS作為實時操作系統(tǒng),任務(wù)和系統(tǒng)調(diào)用之間能夠交替并發(fā)執(zhí)行,這為自動驗證帶來了更大的挑戰(zhàn),手工證明是不可避免的.

除此以外,還有其他一些操作系統(tǒng)驗證項目也研究了系統(tǒng)級性質(zhì)的驗證,如文獻[8]研究了隔離內(nèi)核的信息流安全性,文獻[9]驗證了mCertiKOS系統(tǒng)內(nèi)核的信息流安全性.這些工作研究的是信息流安全性,而本文關(guān)注的則是反映系統(tǒng)功能正確性的性質(zhì).

2 SpaceOS

SpaceOS是北京控制工程研究所研發(fā)的嵌入式多任務(wù)實時操作系統(tǒng),主要功能包括任務(wù)管理、中斷管理、任務(wù)間通信、動態(tài)內(nèi)存管理、時間與定時器管理.SpaceOS的多任務(wù)環(huán)境允許一個實時應(yīng)用作為一系列獨立的任務(wù)來運行,各任務(wù)擁有各自的線程和系統(tǒng)資源,多任務(wù)間可通過信號量、消息隊列、共享內(nèi)存等方式進行交互.SpaceOS能夠高效處理硬件中斷,快速、可靠地響應(yīng)中斷.下面主要介紹本文的工作涉及到的任務(wù)管理、任務(wù)間通信、時間管理等模塊.

圖1 SpaceOS任務(wù)狀態(tài)轉(zhuǎn)換圖Fig.1 Task state transition diagram of SpaceOS

2.1 任務(wù)管理

系統(tǒng)使用任務(wù)控制塊(TCB)來管理任務(wù).任務(wù)控制塊包括了任務(wù)的當前狀態(tài)、優(yōu)先級、等待的事件或資源、任務(wù)程序代碼的起始地址、堆棧指針等信息.任務(wù)有五種基本狀態(tài):就緒態(tài)、運行態(tài)、阻塞態(tài)、掛起態(tài)和睡眠態(tài),其中掛起態(tài)可以和阻塞態(tài)、睡眠態(tài)疊加.圖1描述了各個任務(wù)狀態(tài)之間的轉(zhuǎn)換關(guān)系.

2.2 任務(wù)調(diào)度策略

SpaceOS采用基于固定優(yōu)先級的可搶占式的時間片輪轉(zhuǎn)調(diào)度算法.每個任務(wù)有一個優(yōu)先級,數(shù)值在0-63之間.系統(tǒng)選擇優(yōu)先級最高的任務(wù)執(zhí)行,如果最高優(yōu)先級的任務(wù)有多個,則這些任務(wù)會按照時間片輪轉(zhuǎn)運行.在任務(wù)執(zhí)行過程中,如果有更高優(yōu)先級的任務(wù)轉(zhuǎn)為就緒態(tài),那么系統(tǒng)會打斷當前任務(wù),調(diào)度執(zhí)行高優(yōu)先級的任務(wù),被搶占的任務(wù)在高優(yōu)先級任務(wù)執(zhí)行完畢后恢復(fù)運行.

2.3 任務(wù)間通信

SpaceOS提供了信號量和消息隊列來實現(xiàn)任務(wù)間通信和互斥,其中信號量又分為計數(shù)型信號量、二值信號量和互斥信號量.系統(tǒng)分別使用信號量控制塊(SCB)和消息隊列控制(MQCB)來管理信號量和消息隊列.信號量控制塊記錄了信號量的計數(shù)值和擁有者(對于互斥信號量而言),消息隊列控制塊記錄了消息隊列中每個消息的長度、能夠存儲的最大消息數(shù)量、當前存儲的消息數(shù)等信息.阻塞在同一信號量或消息隊列的任務(wù)構(gòu)成一個優(yōu)先級隊列,高優(yōu)先級的任務(wù)優(yōu)先被解除阻塞.

2.4 時間管理

時間管理模塊負責任務(wù)的時間片輪轉(zhuǎn)、延時等功能.時鐘中斷發(fā)生時,要增加系統(tǒng)中時鐘的值;減少當前任務(wù)的輪轉(zhuǎn)時間片,時間片為0時進行任務(wù)輪轉(zhuǎn);遍歷系統(tǒng)延時隊列,減少其中任務(wù)的等待計時,如果任務(wù)的延時時間到則根據(jù)任務(wù)是否處于掛起、阻塞或者就緒狀態(tài)進行相應(yīng)的操作.

3 操作系統(tǒng)驗證框架

本文使用的操作系統(tǒng)驗證框架由三個部分構(gòu)成:操作系統(tǒng)內(nèi)核的形式化建模;一個支持多級中斷的并發(fā)精化程序邏輯;自動證明策略.其中后兩個部分主要是用來驗證上下文精化關(guān)系的,本文的工作基于內(nèi)核建模部分中的高層建模,本節(jié)簡單介紹高層建模部分.

高層建模將操作系統(tǒng)內(nèi)核抽象為一個狀態(tài)機,內(nèi)核中的各個數(shù)據(jù)結(jié)構(gòu)構(gòu)成內(nèi)核狀態(tài).內(nèi)核狀態(tài)是抽象的,不關(guān)心數(shù)據(jù)結(jié)構(gòu)的具體實現(xiàn).系統(tǒng)調(diào)用由高層建模提供的規(guī)范語言來實現(xiàn),通過描述內(nèi)核狀態(tài)如何轉(zhuǎn)移來刻畫系統(tǒng)調(diào)用的功能.中斷被抽象為可在任意時刻發(fā)生的外部事件,程序員無法控制.和系統(tǒng)調(diào)用一樣,中斷處理程序的功能也用規(guī)范語言描述.應(yīng)用程序用C語言實現(xiàn),不允許直接訪問和修改內(nèi)核狀態(tài),可以調(diào)用內(nèi)核提供的系統(tǒng)調(diào)用.

3.1 抽象規(guī)范語言和抽象狀態(tài)

圖2 抽象規(guī)范語言定義和抽象狀態(tài)Fig.2 Abstract specification language and abstract state

抽象程序狀態(tài)

3.2 操作語義

圖3給出了規(guī)范語言操作語義的主要規(guī)則.操作語義分為三層,全局語義執(zhí)行一步可以是當前任務(wù)執(zhí)行一步HTASK,執(zhí)行任務(wù)調(diào)度SCHD或被外部事件打斷執(zhí)行中斷處理程序PEVENT.SCHD規(guī)則中當前任務(wù)Σ(ct)正要執(zhí)行sched,那么將系統(tǒng)當前任務(wù)ct置為調(diào)度器χ選擇的新任務(wù)t′.

圖3 規(guī)范語言的部分操作語義規(guī)則Fig.3 Selected operational semantic rules

4 SpaceOS建模

4.1 內(nèi)核狀態(tài)

如圖4所示,SpaceOS內(nèi)核狀態(tài)Σsp含有7個部分:抽象任務(wù)控制塊映射α,抽象信號量控制塊映射β,抽象消息隊列控制塊映射ρ,就緒任務(wù)隊列映射,延時任務(wù)隊列Qdly,當前運行任務(wù)標識符t和系統(tǒng)時間tm.

圖4 SpaceOS抽象內(nèi)核狀態(tài)Fig.4 Abstract kernel state of SpaceOS

抽象任務(wù)控制塊映射α由任務(wù)標識符t指向抽象任務(wù)控制塊.任務(wù)控制塊記錄了任務(wù)的舊優(yōu)先級oldpr,當前優(yōu)先級pr,任務(wù)狀態(tài)st,占有的互斥信號量個數(shù)mcnt和收到的消息v.任務(wù)的優(yōu)先級在某些情況下會被修改,這時需要用oldpr保存修改前的優(yōu)先級,以便之后能夠恢復(fù)原有優(yōu)先級.任務(wù)狀態(tài)中的掛起態(tài)可以和其他狀態(tài)疊加,在建模時用標識sflag記錄任務(wù)是否處于掛起態(tài),為true時表示任務(wù)被掛起,為false時表示任務(wù)未被掛起.st′表示任務(wù)可以處于就緒態(tài)、睡眠態(tài)和阻塞態(tài).這樣st′和sflag共同構(gòu)成了任務(wù)狀態(tài)st.

抽象信號量控制塊記錄了信號量類型sty,計數(shù)值cnt和等待隊列Q.由于二值信號量本質(zhì)上是計數(shù)信號量的特例,在建模時將這兩者合并,把信號量類型sty分為計數(shù)型sem和互斥型mutex.mutex w中w記錄了互斥信號量的擁有者.等待隊列Q記錄了申請該信號量被阻塞任務(wù)的標識符.

4.2 抽象規(guī)范

下面以任務(wù)調(diào)度器和任務(wù)創(chuàng)建系統(tǒng)調(diào)用OSTaskSpawn為例,介紹內(nèi)核函數(shù)的抽象規(guī)范.圖5給出了調(diào)度策略的抽象規(guī)范.在一個內(nèi)核狀態(tài)下,調(diào)度程序選擇滿足下列條件的任務(wù)作為被調(diào)度到的任務(wù):FirstTask要求該任務(wù)處于就緒隊列的隊首,HighestPrio要求該任務(wù)所在就緒隊列是優(yōu)先級最高的.

圖5 SpaceOS任務(wù)調(diào)度策略的抽象規(guī)范Fig.5 Specification code for the scheduler of SpaceOS

OSTaskSpawn根據(jù)指定的參數(shù)創(chuàng)建新任務(wù).如果指定的優(yōu)先級超出規(guī)定范圍則或者為新任務(wù)分配內(nèi)存空間失敗則退出.內(nèi)存分配成功后,初始化任務(wù)控制塊中各個域的值,設(shè)置優(yōu)先級為參數(shù)中指定的值.接著將任務(wù)控制塊放到全局任務(wù)控制塊列表中,并將任務(wù)標識符插入優(yōu)先級對應(yīng)的就緒隊列尾部.最后執(zhí)行任務(wù)調(diào)度.

圖6 OSTaskSpawn的抽象規(guī)范Fig.6 Specification code for OSTaskSpawn

編寫完抽象規(guī)范后,得到了由抽象規(guī)范構(gòu)成的抽象內(nèi)核,如圖7所示.本文為任務(wù)創(chuàng)建和刪除,信號量創(chuàng)建,互斥信號量刪除、申請和釋放,時鐘中斷服務(wù)函數(shù)以及任務(wù)調(diào)度器編寫了抽象規(guī)范.

圖7 建模后的系統(tǒng)內(nèi)核Fig.7 Abstract model of the SpaceOS kernel

5 全局性質(zhì)描述和證明

5.1 全局性質(zhì)定義

下面給出操作系統(tǒng)全局性質(zhì)的正式定義.

定義1.(操作系統(tǒng)全局性質(zhì))斷言p是操作系統(tǒng)內(nèi)核的全局性質(zhì),記為│=Initp,當且僅當,對于任意內(nèi)核狀態(tài)Σ,如果Init(Σ)成立,那么:

1)Σ│=p成立;

2)對于任意的應(yīng)用程序A,內(nèi)核狀態(tài)Σ和Σ′,任務(wù)池T和T′,應(yīng)用程序狀態(tài)Δ和Δ′,如果WFInitConfig(A,T,Σ)和(A,)┠成立,那么Σ│=p成立.

其中,

Init是對系統(tǒng)初始狀態(tài)的要求,Init(Σ)成立意味著Σ是合法的初始狀態(tài).WFInitConfig中WFClientCode要求應(yīng)用程序代碼不能含有抽象規(guī)范,InitTasks要求所有任務(wù)尚未執(zhí)行并且任務(wù)池T中的任務(wù)集合和內(nèi)核狀態(tài)Σ中的任務(wù)表是相同的.(A,)├表示執(zhí)行全局操作語義步驟,星號“*”表示執(zhí)行零步或多步,相關(guān)形式化定義均在Coq中給出.定義要求,斷言p是操作系統(tǒng)內(nèi)核的全局性質(zhì),要滿足兩個條件:p在系統(tǒng)初始狀態(tài)下成立;p在系統(tǒng)從初始狀態(tài)執(zhí)行到達的任意狀態(tài)依然保持成立.

SpaceOS系統(tǒng)初始狀態(tài)

圖8給出了SpaceOS系統(tǒng)初始狀態(tài)定義.初始狀態(tài)下,系統(tǒng)只有一個優(yōu)先級為最低優(yōu)先級(63)且為就緒態(tài)的空閑任務(wù);優(yōu)先級63對應(yīng)的就緒隊列只含有該任務(wù)的標識符,其他就緒隊列為空;系統(tǒng)不存在任何信號量和消息隊列.

圖8 SpaceOS系統(tǒng)初始狀態(tài)定義Fig.8 Initial state definition of SpaceOS

5.2 SpaceOS 全局性質(zhì)描述

內(nèi)核中的各個數(shù)據(jù)結(jié)構(gòu)不是獨立的,之間往往存在耦合關(guān)系.例如,任務(wù)控制塊記錄了任務(wù)的優(yōu)先級和狀態(tài),而每個優(yōu)先級都有對應(yīng)的就緒隊列,記錄了就緒態(tài)任務(wù)的標識符.任務(wù)控制塊和就緒隊列之間的關(guān)系可以用下面兩個性質(zhì)來描述:

性質(zhì)1.就緒隊列中的任務(wù)一定處于就緒態(tài),且優(yōu)先級與隊列的優(yōu)先級一致.

性質(zhì)2.就緒態(tài)的任務(wù)一定處于其優(yōu)先級對應(yīng)的就緒隊列中.

形式化描述全局性質(zhì)時,首先將性質(zhì)涉及到的數(shù)據(jù)結(jié)構(gòu)從內(nèi)核狀態(tài)Σ中取出,然后描述這些數(shù)據(jù)結(jié)構(gòu)之間的關(guān)系.在性質(zhì)1的形式化定義中,首先用Σ(α)和Σ(rdyqs)得到任務(wù)控制塊映射和就緒隊列映射,接下來用全稱量詞描述對于任意的優(yōu)先級對應(yīng)的就緒隊列(pr)=Q,以及該隊列中的任意任務(wù)標識t∈Q,任務(wù)控制塊映射中一定存在一個任務(wù),它的優(yōu)先級等于隊列的優(yōu)先級Prio(a)=pr,并且處于就緒態(tài)TaskSt(a)=(rdy(tick),false).

這兩個性質(zhì)對于內(nèi)核設(shè)計和開發(fā)人員來說是非常重要的.回顧前文描述的任務(wù)調(diào)度策略,在選擇任務(wù)時,調(diào)度器從就緒隊列中選擇任務(wù)后,沒有檢查任務(wù)是否是就緒態(tài)的.一旦證明了性質(zhì)1成立,那么可以保證即使不檢查任務(wù)狀態(tài),調(diào)度器也是正確的.

再來看一個互斥信號量的性質(zhì).為互斥信號量API編寫的抽象規(guī)范,具體描述了各個API的功能.而在系統(tǒng)運行起來,任務(wù)不斷調(diào)用這些API使用信號量的過程中能否正確無差錯地實現(xiàn)同步操作,可以通過一些直觀的全局性質(zhì)來刻畫.例如,性質(zhì)3描述了在系統(tǒng)運行時,如果一個互斥信號量尚未被占有的,那么不可能有任務(wù)阻塞在該信號量上.這意味著任務(wù)在申請互斥信號量時,如果信號量可用,那么一定能申請成功;如果一個任務(wù)等待的互斥信號量被釋放了且未被其他任務(wù)占有,那么該任務(wù)一定能夠獲得該信號量.

性質(zhì)3.沒有任務(wù)會等待一個可用的互斥信號量.

下面列舉了本文驗證過的其它5條性質(zhì),相關(guān)形式化定義在Coq文件properties.v中給出,這里不再介紹.

性質(zhì)4.信號量等待隊列中的任務(wù)一定處于阻塞態(tài),且等待的是該信號量.

性質(zhì)5.阻塞在信號量上的任務(wù)一定處于該信號量的等待隊列中.

性質(zhì)6.任意兩個信號量的等待隊列沒有相同元素.

性質(zhì)7.可用互斥信號量的等待隊列為空.

性質(zhì)8.信號量的等待隊列按任務(wù)優(yōu)先級從高到低排序.

5.3 推理規(guī)則

證明系統(tǒng)具有一個全局性質(zhì)的方法是按照全局性質(zhì)的定義,證明:1)系統(tǒng)初始狀態(tài)滿足性質(zhì);2)從初始狀態(tài)執(zhí)行任意全局操作語義步驟到達的新狀態(tài)也滿足性質(zhì).絕大部分證明工作發(fā)生在第二步,需要對機器執(zhí)行過程即操作語義做歸納,證明如果性質(zhì)在一個任意狀態(tài)下成立,那么從這個狀態(tài)執(zhí)行一步到達的新狀態(tài)也成立.進行歸納證明效率較低,一方面,操作語義是小步語義,執(zhí)行規(guī)則眾多,而其中的大部分規(guī)則,尤其是執(zhí)行應(yīng)用程序代碼的規(guī)則不會修改內(nèi)核狀態(tài),此時性質(zhì)成立是顯而易見的,每證明一個性質(zhì)都要分析這些情形顯得非常冗余;另一方面,歸納時,還要用到一些關(guān)于操作語義的輔助定理,而文獻[7]只針對μC/OS-II內(nèi)核證明了這些定理的特殊情形,無法直接用到其他內(nèi)核的驗證上.這些定理與具體性質(zhì)和內(nèi)核無關(guān),應(yīng)當給出通用的證明,避免重復(fù)勞動.

在抽象模型中,系統(tǒng)狀態(tài)和應(yīng)用程序狀態(tài)是分離的,操作語義中應(yīng)用程序執(zhí)行步驟只修改應(yīng)用程序狀態(tài);同時,全局性質(zhì)定義中的WFInitConfig限制了應(yīng)用程序代碼不能含有規(guī)范語句,這就保證了系統(tǒng)狀態(tài)只有內(nèi)核代碼可以修改.按照圖3中的操作語義,內(nèi)核代碼執(zhí)行時,只有任務(wù)調(diào)度、抽象規(guī)范的原子狀態(tài)轉(zhuǎn)換等步驟會修改內(nèi)核狀態(tài).所以,證明全局性質(zhì)的核心是證明執(zhí)行這些內(nèi)核步驟時性質(zhì)保持成立.把這種保持成立的特性稱為穩(wěn)定性.基于這一觀察,設(shè)計了如圖9所示的推理規(guī)則.

對于規(guī)范語句s和斷言p,如果p在s從任意狀態(tài)執(zhí)行一步規(guī)范語義步驟到達的新狀態(tài)下保持成立,那么稱p和s滿足規(guī)范穩(wěn)定性,即stablespec(p,s).圖9下面三行針對規(guī)范語句的具體形式給出了相應(yīng)的規(guī)則來推理規(guī)范穩(wěn)定性.原子狀態(tài)轉(zhuǎn)換語句γ直接改變系統(tǒng)狀態(tài),PRIMSTABLE規(guī)則要求如果其執(zhí)行一步前后性質(zhì)p保持成立,那么stablespec(p,γ)成立;assume、end等語句執(zhí)行一步時不改變系統(tǒng)狀態(tài),ASSUMESTABLE和ENDSTABLE規(guī)則要求穩(wěn)定性無條件成立;順序語句s1;s2是遞歸定義的,SEQSTABLE規(guī)則要求其中的子語句也滿足穩(wěn)定性,分支語句s1+s2類似.

圖9 全局性質(zhì)推理規(guī)則Fig.9 Inference rules

對于任務(wù)調(diào)度,SCHEDSTABLE規(guī)則要求如果改變當前任務(wù)為調(diào)度器χ選擇的新任務(wù)后p能夠保持成立,那么p和χ滿足調(diào)度穩(wěn)定性stablesched(p,χ).APISTABLE規(guī)則要求一旦證明了φ中所有API的抽象規(guī)范的穩(wěn)定性,那么能得到API穩(wěn)定性stableapi(p,φ).類似的,INTSTABLE規(guī)則通過證明每個中斷的抽象規(guī)范的穩(wěn)定性來得到中斷穩(wěn)定性stableint(p,ε).頂層規(guī)則TOPRULE將證明系統(tǒng)具有全局性質(zhì)p轉(zhuǎn)化為證明系統(tǒng)初始狀態(tài)滿足性質(zhì)p、API穩(wěn)定性、中斷穩(wěn)定性和調(diào)度穩(wěn)定性.

可以看到,推理規(guī)則將全局性質(zhì)驗證歸結(jié)為證明性質(zhì)在執(zhí)行內(nèi)核代碼時的穩(wěn)定性,避免了證明執(zhí)行應(yīng)用程序代碼的情形.推理規(guī)則忽略的這部分實際上被轉(zhuǎn)移到了其可靠性證明中,在證明可靠性時,易證對于任意的系統(tǒng)和斷言,執(zhí)行應(yīng)用程序步驟時性質(zhì)保持成立.對于執(zhí)行內(nèi)核代碼的情形,推理規(guī)則將證明分解到了規(guī)范代碼的原子執(zhí)行步驟上,要求每個步驟都要保持性質(zhì)的成立,并且所有的API、中斷的規(guī)范代碼和任務(wù)調(diào)度都要滿足.這樣,即使系統(tǒng)運行時,API被中斷打斷,API之間交替并發(fā)執(zhí)行,也能保證性質(zhì)成立.定理1給出了推理規(guī)則的可靠性.

定理1.(推理規(guī)則可靠性)├Initp?│=Initp

InitTasks(T0,A,Σ0)∧├

在新定義的基礎(chǔ)上做歸納,在歸納步利用歸納假設(shè),最終證明:

引理1.對于任意的抽象內(nèi)核,內(nèi)核三元組φ、ε和χ,斷言p,應(yīng)用程序A,內(nèi)核狀態(tài)Σ和Σ′,任務(wù)池T和T′,應(yīng)用程序狀態(tài)Δ和Δ′,如果=(φ,ε,χ),stableapi(p,φ),stableint(p,ε),stablesched(p,χ),WFConfig((A,),T,Δ,Σ),(A,)├和Σ│=p成立,那么Σ′│=p成立.

證明時,要對全局語義規(guī)則分情況討論.如果執(zhí)行的是應(yīng)用程序規(guī)則,那么系統(tǒng)狀態(tài)不變,結(jié)論成立.執(zhí)行任務(wù)切換時,stablesched(p,χ)保證了更改當前任務(wù)后的新狀態(tài)也滿足斷言p,結(jié)論成立.困難的是執(zhí)行規(guī)范代碼的情況.

引理2.對于任意的抽象內(nèi)核,內(nèi)核三元組φ、ε和χ,斷言p,應(yīng)用程序A,內(nèi)核狀態(tài)Σ和Σ′,任務(wù)池T和T′,應(yīng)用程序狀態(tài)Δ,規(guī)范語句s、s′,如果=(φ,ε,χ),stableapi(p,φ),stableint(p,ε),Σ(ct)=t,T(t)=(s,_),Σ│=p(s,Σ)-Hs′,Σ′)和WFConfig((A,),T,Δ,Σ)成立,那么Σ′│=p成立.

此時當前執(zhí)行的規(guī)范語句s是任意的,操作語義未對其有約束.為了能夠利用stableapi(p,φ)和stableint(p,ε)這兩個已知條件,首先需要建立s與內(nèi)核代碼抽象規(guī)范的聯(lián)系.由于WFConfig限制了應(yīng)用程序代碼不能含有抽象規(guī)范,所以可以推斷出s應(yīng)當是從某個內(nèi)核函數(shù)的抽象規(guī)范sf執(zhí)行過來的.

引理3.對于任意的內(nèi)核,應(yīng)用程序A,內(nèi)核狀態(tài)Σ,任務(wù)池T,應(yīng)用程序狀態(tài)Δ,如果WFConfig((A,),T,Δ,Σ)成立,那么WFTasksH(,T)成立.

其中,

引理3是整個可靠性證明中最困難的部分,Coq文件psoundess.v給出了相關(guān)定義和證明,這里不再介紹.文獻[7]在驗證μC/OS-II的全局性質(zhì)時,證明了類似的定理,但他們是基于已定義好的μC/OS-II的抽象規(guī)范,窮舉了每個抽象規(guī)范在執(zhí)行時規(guī)范語句可能出現(xiàn)的形式,證明無法直接復(fù)用到其他系統(tǒng)的驗證.本文給出了與具體內(nèi)核無關(guān)的通用定理,相關(guān)證明被包裝在了推理規(guī)則可靠性中,這樣在驗證一個新的系統(tǒng)時,只需知曉推理規(guī)則,無需證明任何與操作語義有關(guān)的定理.

5.4 一個例子

經(jīng)過驗證,本文第4節(jié)為SpaceOS建立的抽象模型具有第5.2節(jié)描述的全部8條性質(zhì).Coq文件proof.v含有相關(guān)定理和證明腳本.下面以驗證性質(zhì)1,即就緒隊列中的任務(wù)一定處于就緒態(tài)并且優(yōu)先級與隊列的優(yōu)先級一致為例,介紹全局性質(zhì)的證明步驟.

定理2.(SpaceOS具有性質(zhì)1)sp├Initspp1

證明:根據(jù)TOPRULE,將待證目標轉(zhuǎn)換為4個子目標:

1)系統(tǒng)初始狀態(tài)滿足p1.回顧5.1.1節(jié)初始狀態(tài)的定義,優(yōu)先級63對應(yīng)的就緒隊列中只存在一個空閑任務(wù),其狀態(tài)是就緒態(tài),且優(yōu)先級是63,符合性質(zhì)要求;其余就緒隊列都為空,所以此時性質(zhì)成立.

3)stableint(p1,εsp).使用INTSTABLE規(guī)則,證明每個中斷處理程序的規(guī)范穩(wěn)定性,這和證明API穩(wěn)定性是類似的,這里不再贅述.

4)stablesched(p1,χsp).使用SCHEDSTABLE規(guī)則,證明將系統(tǒng)當前任務(wù)修改為調(diào)度器選擇的任務(wù)后性質(zhì)保持成立.此時內(nèi)核狀態(tài)中只有當前任務(wù)這一全局變量發(fā)生變化,而要證的性質(zhì)并不關(guān)心其具體值,所以此時性質(zhì)保持成立.

在上例的證明過程中,進行了多次分類討論.證明stablespec(p1,γspawn)時,將就緒隊列分為修改的和未被修改的兩類分別證明,相應(yīng)的在Coq中證明時是根據(jù)性質(zhì)中任意的優(yōu)先級pr和新任務(wù)的優(yōu)先級prnew是否相同分成兩種情況.對于pr≠prnew的情況,又要根據(jù)任意t和新任務(wù)的tnew是否相同進一步分情況討論.在描述全局性質(zhì)時會大量使用全稱量詞,如量化一個任意的就緒隊列Q或任意的t來描述對內(nèi)核狀態(tài)的要求,而內(nèi)核函數(shù)會修改內(nèi)核數(shù)據(jù)結(jié)構(gòu),這使得類似的分類證明在全局性質(zhì)驗證過程中非常頻繁,越是復(fù)雜的性質(zhì)和API,需要分析的情形也越多.為了提高Coq證明效率,開發(fā)了一些Coq證明策略,其中最主要的是pcases策略.pcases會自動分析證明上下文,尋找內(nèi)核狀態(tài)中發(fā)生變化的映射,為所有可能的情況生成相應(yīng)的子目標,然后嘗試利用已知條件完成證明,不能自動解決的子目標留給驗證人員手動證明.這些策略在驗證過程中不斷開發(fā)和完善,同驗證初期沒有使用這些策略相比,后期證明的代碼量顯著減少.

6 總 結(jié)

本文基于一個已有的操作系統(tǒng)驗證框架,在Coq中為SpaceOS內(nèi)核建立了抽象模型,形式化定義了8條全局性質(zhì),給出了內(nèi)核具有這些性質(zhì)的機器可檢查的證明.設(shè)計的全局性質(zhì)推理規(guī)則擴展了已有的驗證框架,連同開發(fā)的Coq證明策略一起為全局性質(zhì)驗證提供了更好的支持.這些擴展不僅提高了SpaceOS的驗證效率,也有利于今后驗證其他操作系統(tǒng)的全局性質(zhì).相關(guān)Coq文件和代碼量統(tǒng)計如表1所示:

表1 Coq文件和代碼行數(shù)統(tǒng)計
Table 1 Coq file and line count

文件描述Coq行數(shù)plogic.v全局性質(zhì)定義和推理規(guī)則151psoundness.v推理規(guī)則可靠性證明778ptactic.vCoq證明策略380abs_state.vSpaceOS內(nèi)核狀態(tài)1447abs_spec.vSpaceOS內(nèi)核代碼的抽象規(guī)范836properties.vSpaceOS全局性質(zhì)形式化定義194proof.v全局性質(zhì)的證明腳本 6459總計10281

接下來,我們要把驗證工作推進到其余模塊上,覆蓋更多的API,需要為消息隊列等模塊的API編寫抽象規(guī)范,并驗證更多的性質(zhì).此外,還將考慮擴展內(nèi)核建模的表達力.目前驗證的全局性質(zhì)本質(zhì)上是不變式,要在系統(tǒng)每一步執(zhí)行前后保持成立.而有些性質(zhì)往往會在個別時刻,如任務(wù)調(diào)度前不成立,還有一些則在系統(tǒng)執(zhí)行特定步驟時才成立,這樣的性質(zhì)目前無法驗證.我們希望能夠放寬全局性質(zhì)的定義,并且能夠在內(nèi)核建?；蛘咝再|(zhì)中表達系統(tǒng)執(zhí)行過程,這樣將能驗證更多形式的性質(zhì).