SpaceOS中若干全局性质的形式化描述和验证

2019-01-24 09:30顾海博冯新宇

小型微型计算机系统 2019年1期

顾海博,付明,乔磊,冯新宇

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语言具体实现上.

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编写抽象规范,并验证更多的性质.此外,还将考虑扩展内核建模的表达力.目前验证的全局性质本质上是不变式,要在系统每一步执行前后保持成立.而有些性质往往会在个别时刻,如任务调度前不成立,还有一些则在系统执行特定步骤时才成立,这样的性质目前无法验证.我们希望能够放宽全局性质的定义,并且能够在内核建模或者性质中表达系统执行过程,这样将能验证更多形式的性质.