μC/OS-Ⅲ任務調度器在Coq中的驗證

羅爾聰,郭 宇

(1.中國科學技術大學計算機科學與技術學院,合肥230026;

2.中國科學技術大學蘇州研究院軟件安全實驗室,江蘇蘇州215123)

μC/OS-Ⅲ任務調度器在Coq中的驗證

羅爾聰1,2,郭 宇1,2

(1.中國科學技術大學計算機科學與技術學院,合肥230026;

2.中國科學技術大學蘇州研究院軟件安全實驗室,江蘇蘇州215123)

以μC/OS-Ⅲ內核中的任務調度器為研究對象,選取調度相關的核心代碼,驗證調度器代碼滿足優先調度最高優先級任務的性質。基于分離邏輯與SCAP驗證理論,利用Coq輔助證明工具,通過定義機器模型、操作語義、邏輯斷言以及推導規則構建驗證框架。在驗證框架中,定義內核數據結構和內核相關性質的邏輯描述,模塊化地對內核代碼進行推理。驗證結果表明,μC/OS-Ⅲ任務調度器滿足可靠性要求,并且可以通過機器的自動檢查。

任務調度器;形式化驗證;分離邏輯;Coq證明工具;最高優先級

1 概述

嵌入式操作系統負責管理系統軟硬件資源,在工業控制、移動設備等領域中處于非常關鍵的位置。為確保這部分完成任務調度的代碼能夠正確地運行,本文采用邏輯驗證的形式化方法,在輔助證明工具Coq［1］中驗證μC/OS-Ⅲ［2］內核中的任務調度器代碼。μC/OS-Ⅲ任務調度器的形式化工作主要有以下難點:

(1)調度器代碼涉及到諸多系統數據結構,驗證之前需要描述其系統數據結構的性質和它們相互之間應該滿足的關系。

(2)任務(Task),作為操作系統中運行的基本單元,具有描述其重要程度的優先級(Priority)屬性。在任務調度過程中,內核需要完成對最高優先級(Highest Priority)任務的選取,然后進行任務上下文切換。驗證需要保證在執行調度函數代碼前后,內核中描述任務優先級的變量能夠正確讀寫。

本文從μC/OS-Ⅲ任務調度器選取相關代碼,將其編譯后的匯編級指令進行形式化建模,然后為這部分指令給出形式化的規范(Specification)描述,并證明這部分代碼滿足最高優先級調度性質:從任意一個合法機器狀態集合出發,任務調度程序執行調度相關代碼,之后到達一個新的狀態。在這個新狀態中,相關

全局變量記錄正確的最高優先級與被選任務。

本文驗證的內核調度代碼基于一個形式化的簡化機器模型,采用分離邏輯［3］描述內核規范,同時采用SCAP［4］邏輯對內核指令進行推理。本文的所有形式化工作都基于交互式定理證明工具Coq,主要工作如下:

(1)驗證μC/OS-Ⅲ任務調度器相關代碼以下關鍵性質(內存安全性、部分指令代碼的功能正確性和最高優先級)。

(2)使用證明輔助工具Coq實現邏輯系統和驗證選取代碼,所有定義和證明都可以接受機器自動檢查。

2 相關工作

文獻［5］提出了一種基于C語言的FreeRTOS任務調度器的自動化證明方法。本文統一使用匯編語言進行建模,使得程序斷言能夠實現對機器狀態的精確描述,且稍加擴展便可驗證操作系統底層代碼。

使用Coq交互式驗證工作量巨大,文獻［6-7］提供了可供參考的自動化或半自動化驗證策略。文獻［8］以SCAP框架為基礎提出一種含有模擬關系的虛擬機構造和驗證方案,可以作為本文改進的借鑒。

3 驗證方法

本文選取μC/OS-Ⅲ任務調度器中的2個重要函數OSSched()和OSIntExit()進行實現代碼級驗證。本節介紹它們所涉及的內核數據結構及其執行流程。

3.1 系統就緒表與系統優先級表

在μC/OS-Ⅲ中,任務通過任務控制塊(TCB)來描述其狀態。TCB含有前向指針、后向指針和優先級3個域。通過前2個域,優先級相同的TCB構成雙鏈表。系統就緒表將分離的具有不同優先級的TCB雙鏈表組織起來,在內存中由一個全局的一維數組表示。數組元素由頭指針、尾指針和元素計數3個域構成,如圖1所示。

圖1 系統就緒表與系統優先級表

系統優先級表是另外一個全局一維數組,其設立的目的是為了快速獲得系統就緒表中的狀態,數組元素取值與系統就緒表中對應TCB雙鏈表元素數量相關。

為了確保調度過程的正確執行,調度代碼對兩表進行操作時必須滿足以下4個關鍵性質:

性質1(良形雙鏈表) 雙鏈表中的每一個節點都正確地指向其前驅和后繼節點,此外雙鏈表中的TCB還擁有共同的優先級。本文將此類雙鏈表稱之為良形雙鏈表。

性質2(良形系統就緒表數組元素) 以良形雙鏈表共同優先級為系統就緒表索引,獲得的數組元素的頭指針指向雙鏈表隊首,尾指針指向雙鏈表隊尾,元素計數與雙鏈表中TCB數量相等。本文稱之為良形數組元素。

性質3(系統就緒表與系統優先級表的一致性)

以系統就緒表任意數組元素都是良形為前提,對于任意索引,指向雙鏈表的元素數量與系統優先級表對應元素取值存在雙射關系:元素數量為0(不為0),當且僅當系統優先級表對應元素為0(為1)。本文稱之為一致性。

性質4(最高優先級) 優先級p是最高優先級,當且僅當系統就緒表中索引為p的數組元素指向的雙鏈表元素數量不為0(系統優先級表對應元素為1),索引小于p的數組元素指向的雙鏈表元素數量為0(系統優先級表對應元素為0)。

3.2 任務調度函數驗證

函數OSSched()和OSIntExit()是任務調度器的核心代碼,前者實現任務級任務調度,后者實現中斷級任務調度。OSSched()在任務實現代碼里被主動調用,OSSched與OSIntExit的函數流程如下:

函數入口是一系列任務調度條件判斷語句,以及關中斷進入臨界區的指令,之后函數通過系統優

先級表和系統就緒表分別獲取最高優先級與待切換任務,最后在退出臨界區之前進行任務級上下文切換。OSIntExit()通常在系統中斷服務程序中被調用,函數主體都在臨界區內。

對比上述執行流程可知,2個函數采用相同代碼實現獲取最高優先級與待切換任務。在形式化過程中,性質3描述的一致性是這段代碼正確性的保證。同時驗證被調用的OS_PrioGetHighest()函數時需要使用性質4的內容。

4 硬件機器模型與推理邏輯系統

本文選取Intel i386架構的一個簡化子集作為運行μC/OS-Ⅲ內核的硬件平臺,并采用程序邏輯SCAP推理本文所研究的任務調度器代碼。

4.1 機器模型與操作語義

機器配置(mach)在Coq中被定義為四元組:

其中,代碼code是地址到機器指令的映射;內存mem是地址到機器字的映射,寄存器文件regfile是從寄存器到機器字的映射;pc表示指令指針。

Inductive reg:Set:=eax:reg|edx:reg|ebp:reg|esp:reg |irf:reg|zf:reg.

注意這里的寄存器不僅包括通用寄存器eax和edx等,還包含一個中斷寄存器irf和獨立的標志位寄存器zf。在Coq中,寄存器通過歸納定義reg實現。

機器模型中指令集是i386機器指令集的一個子集,包含常見的指令,包括移位、算數、比較等指令。在Coq中,指令instruction也采用歸納定義:

指令的執行指令語義采用2個關系謂詞來定義,NextS與NextPC。前者描述在指令執行前后,內存與寄存器的改變,而后者描述控制流的走向。

以MOV指令為例,謂詞NextS首先從寄存器文件R中獲取寄存器單元rs的值,暫存到變量x,然后通過函數rf_update更新R中的rd寄存器,新的寄存器文件為R′。

謂詞NextPC定義了指令指針的變化:在執行MOV指令之后,指令指針加一,指向下一條指令。

限于篇幅,這里不再贅述其余的指令。其形式化語義大部分遵守Intel手冊中的描述。

4.2 斷言語言與推理邏輯系統

為了描述函數規范,本文采用分離邏輯的斷言語言來描述。后文中將要使用到的部分邏輯連接詞如下:

其中,p??q表示分離合取;為了描述不依賴于任何存儲的斷言,本文用!標記純斷言(pure assertion); l|-＞w表示地址為l的內存單元存儲值為w。在Coq實現時,本文采用淺嵌入［9］的方式來定義斷言語言。

程序邏輯SCAP(Stack-based Certified Assembly Language)是用來推理帶有結構化堆棧操作的機器指令的類似Hoare邏輯［10］的推理系統。SCAP邏輯的推理過程以指令序列為單位。函數由一些指令序列構成,程序規范以函數為單位定義。程序規范是一個二元組,包含一個前條件與一個描述函數前后狀態變化的二元關系:

程序規范集合PSpec是一個從一個指令序列的起始地址到函數規范的定義。下面列出SCAP推理規則在Coq中的定義框架:

可以看出,推理規則被定義成一個多元關系WFcomm,根據接受的指令進行分情況展開,每一個分支對應不同指令的推導規則。

5 驗證實現

本節介紹符合性質1和性質2的內核數據結構,以及符合性質3和性質4的內核性質的斷言構

造過程。

5.1 內核數據結構的表示

為表示相同元素組成的有序序列,本文以Coq標準庫中多態list作為形式化的基礎歸納構造類型,以實現核心數據與特定數據結構的分離。以圖1中OSPrioTbl索引0～4的片段為例,定義抽象優先級表如下:

Definition l:list TID:=(0::0::1::1::0::nil).

由前文可知系統就緒表中TCB存在2種序關系:優先級上有序和優先級內有序。因此,本文以list復合構建抽象系統就緒表。圖1中OSRdyList索引0～4片段的具體定義如下所示(設TCB地址為1～5):

在定義抽象內核數據之后,本文通過4個步驟實現針對μC/OS-Ⅲ系統特定數據結構斷言的構造。

(1)TCB斷言。其中,PrevPtr,NextPtr和Prio為相對TCB起始地址的偏移常量。任意TCB起始地址不能為0。

(2)良形雙鏈表斷言。根據性質1描述,通過具有同一優先級的抽象系統就緒表進行歸納構造:

(3)良形系統就緒表數組元素斷言。根據性質2描述進行構造,其中函數length的作用是返回list長度。

(4)系統就緒表斷言。參數p為系統就緒表內存起始地址(相鄰單元地址偏移為12),參數ll為抽象系統就緒表,參數prio為優先級迭代的起始值,通常為0。

系統優先級表斷言的定義過程與系統就緒表類似,在此不再贅述。

5.2 內核性質的表示

性質3描述了具有同一索引的系統就緒表數組元素與系統優先級表元素的一一映射關系。利用上一節定義的抽象內核數據,本文采用斷言函數Correspondence描述一致性:

Correspondence的核心規則是當兩表不為空時,取得各表頭元素,遞歸構造滿足性質3的合取范式。根據性質4,本文通過函數HighestPriority實現優先級p是否為抽象系統就緒表最高優先級的判斷:

HighestPriority本質為系統就緒表從O～p索引元素斷言的合取范式。同理,本文構造系統優先級表的最高優先級斷言函數HighestPriorityHash如下:

以上描述內核性質的3個斷言函數,滿足關系如下:

引理1 對于任意抽象系統就緒表與系統優先級表,若滿足一致性,那么對于任意優先級p,它是系統就緒表最高優先級當且僅當亦是系統優先級表最高優先級。

證明過程略。

此外,本文還定義了判斷某一TCB是否在抽象系統就緒表中的斷言函數InRL:

InRL本質為依次對每個元素判斷的析取范式。存在關系斷言與系統就緒表最高優先級斷言存在如下關系:

引理2 對于任意TCB與抽象系統就緒表,如果TCB存在于抽象系統就緒表中,那么此抽象系統就緒表存在最高優先級。

5.3 內核實現代碼的推理

本文3.2節中兩函數共有的調度代碼(下劃線部分),轉換成匯編指令后形式化推理過程如下:

調度代碼的推理過程如下:

關于調度代碼的驗證工作,有以下3點需要補充說明:

(1)當前任務指針和當前優先級分別由全局變量OSTCBCurPtr和OSPrioCur記錄,被選取的任務指針和最高優先級分別由全局變量OSTCBHighRdyPtr和

OSPrioHighRdy記錄。對比調度代碼執行前后斷言可以發現后兩者的變化。

(2)斷言函數K描述任務棧上的存儲,有3個參數:第1個參數為基地址b,第2個和第3個參數都為list。其功能是分別將兩list映射到b-4n至b-4和b至b+4(m-1)的內存地址空間(n,m分別為兩list長度)。

(3)函數OS_PrioGetHighest()獲取最高優先級,保存在eax寄存器中返回。以一致性和存在關系為前提,OS_PrioGetHighest()前斷言中的系統優先級表最高優先級性質可以通過引理1、引理2推導出來。

5.4 驗證結果

根據以上內容,本文形式化定義并驗證了最高優先級調度性質如下:

以本文定義的機器模型為基礎,從任一滿足一致性與存在性質的合法狀態(C,M,R,pc)出發,系統在運行任務調度相關代碼后,到達一個新狀態(C,M′,R′,pc′),新狀態里全局變量OSPrioHighRdy記錄最高優先級,全局指針OSTCBHighRdyPtr記錄待切換的TCB。

除此之外,本文還形式化驗證了內存安全性、部分指令代碼的功能正確性,以及推理規則可靠性等性質。表1展示了本文驗證的內核調度函數列表。整個證明工作共花費數月時間,Coq代碼總量為5萬多行。

表1 內核調度相關函數

6 結束語

操作系統任務調度器由于其結構復雜是驗證工作難點。本文以嵌入式內核μC/OS-Ⅲ的任務調度器為研究對象,基于相關框架和模型,利用Coq輔助證明工具,最終形式化驗證了調度代碼滿足相關性質,并且得到可以經過機器自動檢查的證明。

本文對μC/OS-Ⅲ任務調度器的關注重點集中在最高優先級如何被正確選取,利用文獻［11］提出的相關邏輯和文獻［12］提出的上下文切換驗證框架,將μC/OS-Ⅲ任務級和中斷級上下文切換整合進μC/OS-Ⅲ任務調度器形式化工作,是下一步的研究方向。

［1]Micriμm.μC/OS-Ⅲ用戶手冊［EB/OL］.［2014-05-01］.https://doc.micrium.com/pages/viewpage.action?pageId= 10753180.

［2]Coq開發團隊.Coq證明輔助工具參考手冊［EB/OL］.［2014-05-01］.http://coq.inria.fr.

［3]Reynolds J C.Separation Logic:A Logic for Shared Mutable Data Structures［C］//Proceedings of the 17th AnnualIEEESymposiumonLogicinComputer Science.［S.l.］:IEEE Computer Society,2002:55-74.

［4]Feng X,Shao Z,Vaynberg A,et al.Modular Verification of Assembly Code with Stack-based Control Abstractions［J］.ACMSIGPLANNotices,2006,41(6): 401-414.

［5]Ferreira J F,He G,Qin S.Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK［C］//Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering.［S.l.］:IEEE Press,2012:51-58.

［6]Berdine J,CalcagnoCO,HearnPW.Symbolic Execution with Separation Logic［M］//Jhala R,Igarashi A.ProgrammingLanguagesandSystems.Berlin, Germany:Springer,2005:52-68.

［7]McCreight A.Practical Tactics for Separation Logic［M］// Seidenberg A.Theorem Proving in Higher Order Logics.Berlin,Germany:Springer,2009:343-358.

［8]董 淵,任 愷,王生原,等.字節碼虛擬機的構造和驗證［J］.軟件學報,2010,21(2):305-317.

［9]Garillot F,Werner B.Simple Types in Type Theory: Deep andShallowEncodings［M］//SchneiderK, Brandt J.Theorem Proving in Higher Order Logics.Berlin,Germany:Springer,2007:368-382.

［10]Hoare C A R.AnAxiomaticBasisforComputer Programming［J］.Communications of the ACM,1969, 12(10):576-580.

［11]Feng X,Shao Z,Dong Y,et al.Certifying Low-level Programs withHardwareInterruptsandPreemptive Threads［J］.ACM SIGPLAN Notices,2008,43(6): 170-182.

［12]Guo Y,Feng X,Shao Z,et al.Modular Verification of Concurrent Thread Management［M］//Jhala R,Igarashi A.Programming Languages and Systems.Berlin,Germany: Springer,2012:315-331.

編輯 金胡考

Verification of μC/OS-ⅢTask Scheduler in Coq

LUO Ercong1,2,GUO Yu1,2
(1.College of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China;
2.Software Security Laboratory,Suzhou Institute for Advanced Study, University of Science and Technology of China,Suzhou 215123,China)

This paper studies the task scheduler in a widely used embedded μC/OS-Ⅲkernel.After selecting core parts from the scheduler,it specifies the properties of the scheduler formally.Based on the separation logic and SCAP,it builds a verification framework including a machine model,operational semantics,assertion languages,and inference rules.In the framework,assertions specifying system data structures and properties are defined,and system code is able to be reasoned about modularly.Finally,the properties of the task scheduler in μC/OS-Ⅲare formally proved,and the entire proof provided by the work are machine checkable.

task scheduler;formal verification;separation logic;Coq proof tool;highest priority

羅爾聰,郭 宇.μC/OS-Ⅲ任務調度器在Coq中的驗證［J］.計算機工程,2015,41(3):53-58.

英文引用格式:Luo Ercong,Guo Yu.Verification of μC/OS-ⅢTask Scheduler in Coq［J］.Computer Engineering, 2015,41(3):53-58.

1000-3428(2015)03-0053-06

:A

:TP309

10.3969/j.issn.1000-3428.2015.03.010

國家自然科學基金資助青年項目(61202052);國家自然科學基金海外及港澳學者合作研究基金資助項目(61229201)。

羅爾聰(1989-),男,碩士研究生,主研方向:形式化驗證,軟件安全;郭 宇,副教授。

2014-05-05

:2014-05-28E-mail:ecluo@mail.ustc.edu.cn