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

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

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

1 引 言

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

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

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

1)為SpaceOS內核狀態建立了抽象模型,描述內核數據結構,為主要模塊的系統調用和中斷處理程序編寫了抽象規范.

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

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

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

相關研究工作

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

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

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

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

2 SpaceOS

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

圖1 SpaceOS任務狀態轉換圖Fig.1 Task state transition diagram of SpaceOS

2.1 任務管理

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

2.2 任務調度策略

SpaceOS采用基于固定優先級的可搶占式的時間片輪轉調度算法.每個任務有一個優先級,數值在0-63之間.系統選擇優先級最高的任務執行,如果最高優先級的任務有多個,則這些任務會按照時間片輪轉運行.在任務執行過程中,如果有更高優先級的任務轉為就緒態,那么系統會打斷當前任務,調度執行高優先級的任務,被搶占的任務在高優先級任務執行完畢后恢復運行.

2.3 任務間通信

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

2.4 時間管理

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

3 操作系統驗證框架

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

高層建模將操作系統內核抽象為一個狀態機,內核中的各個數據結構構成內核狀態.內核狀態是抽象的,不關心數據結構的具體實現.系統調用由高層建模提供的規范語言來實現,通過描述內核狀態如何轉移來刻畫系統調用的功能.中斷被抽象為可在任意時刻發生的外部事件,程序員無法控制.和系統調用一樣,中斷處理程序的功能也用規范語言描述.應用程序用C語言實現,不允許直接訪問和修改內核狀態,可以調用內核提供的系統調用.

3.1 抽象規范語言和抽象狀態

圖2 抽象規范語言定義和抽象狀態Fig.2 Abstract specification language and abstract state

抽象程序狀態

3.2 操作語義

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

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

4 SpaceOS建模

4.1 內核狀態

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

圖4 SpaceOS抽象內核狀態Fig.4 Abstract kernel state of SpaceOS

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

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

4.2 抽象規范

下面以任務調度器和任務創建系統調用OSTaskSpawn為例,介紹內核函數的抽象規范.圖5給出了調度策略的抽象規范.在一個內核狀態下,調度程序選擇滿足下列條件的任務作為被調度到的任務:FirstTask要求該任務處于就緒隊列的隊首,HighestPrio要求該任務所在就緒隊列是優先級最高的.

圖5 SpaceOS任務調度策略的抽象規范Fig.5 Specification code for the scheduler of SpaceOS

OSTaskSpawn根據指定的參數創建新任務.如果指定的優先級超出規定范圍則或者為新任務分配內存空間失敗則退出.內存分配成功后,初始化任務控制塊中各個域的值,設置優先級為參數中指定的值.接著將任務控制塊放到全局任務控制塊列表中,并將任務標識符插入優先級對應的就緒隊列尾部.最后執行任務調度.

圖6 OSTaskSpawn的抽象規范Fig.6 Specification code for OSTaskSpawn

編寫完抽象規范后,得到了由抽象規范構成的抽象內核,如圖7所示.本文為任務創建和刪除,信號量創建,互斥信號量刪除、申請和釋放,時鐘中斷服務函數以及任務調度器編寫了抽象規范.

圖7 建模后的系統內核Fig.7 Abstract model of the SpaceOS kernel

5 全局性質描述和證明

5.1 全局性質定義

下面給出操作系統全局性質的正式定義.

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

1)Σ│=p成立;

2)對于任意的應用程序A,內核狀態Σ和Σ′,任務池T和T′,應用程序狀態Δ和Δ′,如果WFInitConfig(A,T,Σ)和(A,)┠成立,那么Σ│=p成立.

其中,

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

SpaceOS系統初始狀態

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

圖8 SpaceOS系統初始狀態定義Fig.8 Initial state definition of SpaceOS

5.2 SpaceOS 全局性質描述

內核中的各個數據結構不是獨立的,之間往往存在耦合關系.例如,任務控制塊記錄了任務的優先級和狀態,而每個優先級都有對應的就緒隊列,記錄了就緒態任務的標識符.任務控制塊和就緒隊列之間的關系可以用下面兩個性質來描述:

性質1.就緒隊列中的任務一定處于就緒態,且優先級與隊列的優先級一致.

性質2.就緒態的任務一定處于其優先級對應的就緒隊列中.

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

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

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

性質3.沒有任務會等待一個可用的互斥信號量.

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

性質4.信號量等待隊列中的任務一定處于阻塞態,且等待的是該信號量.

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

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

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

性質8.信號量的等待隊列按任務優先級從高到低排序.

5.3 推理規則

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

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

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

圖9 全局性質推理規則Fig.9 Inference rules

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

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

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

InitTasks(T0,A,Σ0)∧├

在新定義的基礎上做歸納,在歸納步利用歸納假設,最終證明:

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

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

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

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

引理3.對于任意的內核,應用程序A,內核狀態Σ,任務池T,應用程序狀態Δ,如果WFConfig((A,),T,Δ,Σ)成立,那么WFTasksH(,T)成立.

其中,

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

5.4 一個例子

經過驗證,本文第4節為SpaceOS建立的抽象模型具有第5.2節描述的全部8條性質.Coq文件proof.v含有相關定理和證明腳本.下面以驗證性質1,即就緒隊列中的任務一定處于就緒態并且優先級與隊列的優先級一致為例,介紹全局性質的證明步驟.

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

證明:根據TOPRULE,將待證目標轉換為4個子目標:

1)系統初始狀態滿足p1.回顧5.1.1節初始狀態的定義,優先級63對應的就緒隊列中只存在一個空閑任務,其狀態是就緒態,且優先級是63,符合性質要求;其余就緒隊列都為空,所以此時性質成立.

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

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

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

6 總 結

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

表1 Coq文件和代碼行數統計
Table 1 Coq file and line count

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

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