μ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