2020, Vol. 31
2. 上海市高可信计算重点实验室(华东师范大学), 上海 200062;
3. 软硬件协同设计技术与应用教育部工程研究中心(华东师范大学), 上海 200062
2. Shanghai Key Laboratory of Trustworthy Computing (East China Normal University), Shanghai 200062, China;
3. Software/Hardware Co-design Engineering Research Center (East China Normal University), Ministry of Education, Shanghai 200062, China
软件系统作为信息技术的核心, 其安全可靠性在轨道交通、汽车电子、航空航天以及国防安全等安全攸关领域是非常重要的.其中基础软件, 如操作系统的安全是整个软件系统的重中之重.近年来, 在国内外因基础软件安全问题而导致的恶劣事件屡见不鲜.2017年上半年的WannaCry[1, 2]勒索病毒全球大爆发, 给全球超过150个国家、30万名网络用户带来了超过80亿美元的经济损失.该病毒是由不法分子利用操作系统的漏洞, 入侵他人Windows操作系统用户, 将大量重要资料进行加密, 使得众多受感染的用户无法正常工作, 影响十分恶劣. 2018年1月份, 国外安全机构曝出的CPU安全漏洞:熔断[3]和幽灵[4].该漏洞容易导致敏感数据被泄露, 在全球范围内引起了广泛的关注, 尤其是对云服务厂商产生了极大的影响[5].
操作系统作为软件系统的核心, 其安全性与可靠性是构造高可信软件的最为关键的一步.嵌入式实时操作系统因其具有并发、可抢占的特性以及代码的复杂性给验证工作带来了巨大挑战.
近些年来, 学术界有诸多关于将形式化方法运用到操作系统内核验证的研究中, 著名的有澳大利亚研究中心NICTA的seL4项目[6, 7], 在2009年, seL4项目组使用Isabelle[8]工具完成了sel4的形式化验证, 该项目是第一个成功地完成了对操作系统内核的完全形式化验证.由德国联邦教育与研究部资助的Verisoft项目[9-11]提出了一个命名为CVM的验证框架, 通过CVM验证框架验证了一个实际运行的操作系统内核.其后续项目Verisoft-XT项目[12, 13]使用由微软研究院研发的推理证明工具VCC[14]对PikeOS[15]进行了形式化的验证.美国耶鲁大学Zhong Shao团队运用Coq[16]工具对其自行开发的mCertiKOS[17]操作系统进行了端到端的完整形式化验证.Flint研究组关于操作系统内核的验证[18-20]以及华盛顿大学Hyperkernel的项目[21]等在操作系统验证中都做了大量的工作.
国内关于操作系统内核的形式化验证研究也处于较高的水平.中国科技大学的冯新宇团队[22-24]运用Coq对商用实时操作系统内核μC/OS-Ⅱ[25]进行了一个较为完整的形式化验证.除此之外, 赵永望团队建立了符合ARINC653的分区内核模型, 采用了Event-B对系统所有的功能和服务进行了形式化建模, 该模型实现了ARINC653的完整功能和接口.同时, 他们利用Isabelle工具对操作系统功能规范进行了安全性分析与验证[26].中国科学院软件研究所的周巢尘院士和詹乃军团队成功地开展了对中国铁路控制系统CTCS-3的建模和模型层面的验证工作[27].
操作系统内核的验证涉及诸多方面.
●操作系统内核的系统调用正确性.操作系统内核将具体的硬件结构进行了抽象, 只给上层应用开放系统调用接口, 上层应用通过系统调用开发各种应用, 极大地简化了开发过程.因此, 系统调用所提供的功能与其规范一致性是保证上层应用正确性的关键.
●C语言和汇编语言的混合应用.操作系统在对硬件访问时, 为了提高效率, 通常利用汇编语言来实现, 实现与硬件无关的功能则采用C语言编写.因而操作系统内核是由C语言和汇编语言互相嵌套来实现的.对由C语言和汇编语言构成的混合程序验证是一个难题.
●程序支持中断和抢占.实时操作系统是一个可抢占式的, 能随时被中断服务程序中断的系统, 由于系统的可抢占性和中断服务机制使得系统的执行具有不确定性, 针对中断机制的验证仍是一个难点.
基于以上3个问题, 本文提出了一种通用的自动化验证框架, 借助于相关工具, 使用本验证框架可对由C语言和汇编语言实现的实时操作系统内核进行自动化验证, 从而实现了C和汇编的混合代码验证的目标.与此同时, 由于操作系统底层代码与硬件平台相关性, 本文所提出的验证框架稍加改动, 就可以运用到不同硬件平台上的内核验证中, 极大地提高了验证工作的效率.
本文第1节详细介绍本文提出的操作系统内核验证框架, 首先对所要验证的操作系统内核μC/OS-Ⅱ进行概述, 接着叙述操作系统中的C和汇编的混合程序的验证方法.第2节介绍对混合语言抽象建模的方法, 提出为汇编语言建立抽象模型的方法, 针对操作系统内核中的混合程序给出抽象建模的步骤.第3节是抽象模型的实现, 介绍模型实现语言的语法定义, 解释运用该语言对抽象模型的实现方法, 说明如何保证抽象模型和C代码之间数据的一致性问题.第4节描述将该验证框架应用μC/OS-Ⅱ内核的验证中, 并分析验证结果.第5节介绍本验证框架在其他硬件平台上的验证情况, 并对比不同平台上的验证结果, 对该验证框架做出有效性分析.最后是总结及对未来工作的展望.
1 操作系统内核验证框架操作系统绝大多数都是采用C语言和汇编语言编写的, 对操作系统的验证需要分析C语言、汇编语言和混合语言的验证.本文以μC/OS-Ⅱ为研究对象, 提出了一个通用的自动化验证框架[28].该框架如图 1所示.
|
Fig. 1 Automatic verification framework of OS kernel 图 1 操作系统内核自动化验证框架 |
验证工作分为两个部分:一部分对由高层语言(如C语言)构成的系统调用进行验证, 通过自动化验证工具VCC检查系统调用的源代码与其规范的一致性; 在另一部分中, 对由高层语言和底层语言(如C语言和汇编语言)构成的内核服务程序进行验证, 通过将汇编语言转换成抽象模型, 并实现与C语言的粘合, 形成符合基于C语言的验证工具(如VCC)能够接收的模型, 再利用该工具验证新混合代码.
1.1 μC/OS-Ⅱ介绍μC/OS-Ⅱ[25]是一款开源的基于优先级可抢占式的嵌入式实时操作系统, 最早是由美国嵌入式系统专家Labrosse在1992年发布, 因其代码整洁、注释详尽、利于阅读等特点, 目前已广泛应用于嵌入式领域, 例如航空电子、医疗设备及汽车电子等行业.μC/OS-Ⅱ的代码组成结构如图 2中所示.
|
Fig. 2 Code constructure of μC/OS-Ⅱ 图 2 μC/OS-Ⅱ代码结构 |
μC/OS-Ⅱ包括库文件、平台无关的代码和平台有关代码3部分.μC/OS-Ⅱ绝大部分是由ANSI C语言编写的, 源代码中只有关于上下文的切换、中断的控制、寄存器的访问等功能是由汇编语言编写.汇编代码总量不超过200行, 因此其具有极高的可移植性.
μC/OS-Ⅱ在不同平台的移植过程中, 只需要修改与平台硬件相关的代码文件即可, 也就是关于寄存器的访问、上下文切换以及中断控制等功能的实现代码.系统调用的实现与硬件无关, 它包括了任务管理、时钟管理、信号量、互斥量、邮箱、消息队列、事件标志、内存管理等部分.
本文提出的验证框架应用到了飞思卡尔的ColdFire和ARM Cortex-M3这两种不同硬件平台中, 在此对其硬件结构做一简单介绍.
1.1.1 Freescale MCF平台飞思卡尔的MCF5441x(简称MCF)系列[29, 30]是一个32位的处理器内核, 由8个32位的通用数据寄存器(D0~D7)、8个通用地址寄存器(A0~A7)、1个16位状态寄存器和一些其他的组件构成.
●这8个数据寄存器可以存储相应的数据, 它们的数据类型可以是一个字节(8位)、字(16位)或者是双字(32位).
●8个地址寄存器可用作软件栈指针、索引寄存器以及基地址寄存器, 其中, 基地址寄存器只能对字和双字类型进行操作.A7寄存器是地址寄存器中最为特殊的一个, 可用作栈指针.
●状态寄存器是用于存储处理器状态、中断优先级掩码以及其他控制位.其中, 第8位~第10位属于中断优先级掩码, 该掩码用于定义当前中断优先级.中断优先级掩码设定了中断请求优先级的界限, 即在有中断请求发生的时候, 凡是小于等于当前优先级的所有中断都将予以屏蔽.
1.1.2 ARM Cortex-M3平台ARM架构下的Cortex-M3(简称CM3)[31]和MCF一样, 也属于32位处理器内核, 有1个寄存器组(R0~R15)、中断屏蔽寄存器组(PRIMASK, FAULTMASK, BASEPRI)、中断控制及状态寄存器(ICSR)以及其他组件构成.
在寄存器组(R0~R15)中的16个寄存器, 其中13个(R0~R12)为32位通用目的寄存器, 其他3个有特殊用途. R0~R7被称作低寄存器(16位指令只能访问低寄存器), R8~R12被称作高寄存器.R13(SP)有两个堆栈指针, 它们是互斥的, 在任意时刻都只能使用其中的1个, 通过PUSH和POP操作实现堆栈的访问.R14是链接寄存器(LR), 用于函数或子程序调用时返回地址的保存; 在函数或子程序结束时, 程序控制可以通过将LR的数值加载到PC中, 返回到调用程序并继续执行.R15是程序计数器(PC), 指向下一条要取指的指令地址.
PRIMASK是只使用1个位的寄存器, 可以关掉除NMI和硬fault之外所有的异常; FAULTMASK是只使用1个位的寄存器, 当其被置位为1时, 除了NMI能够响应, 其他的异常都被屏蔽.BASEPRI寄存器最多使用9位, 它用于定义被屏蔽优先级的阈值, 即当其设为某个值时, 所有小于等于此优先级的中断都会被屏蔽(优先级号越高, 优先级越低).
中断控制及状态寄存器ICSR可以对NMI、SysTick定时器以及PendSV进行手动悬挂, 其中, PendSV是为系统设备而设的“可悬挂请求”.
PendSV是一种中断服务, 一般设置其为最低的优先级, 当其他的所有的中断服务执行完之后才对其进行处理.典型的使用场景是运用于上下文切换中, 将PendSV进行悬起, 以实现延缓执行上下文的切换.
1.2 高层语言程序的验证方法绝大多数操作系统内核(如本文中的μC/OS-Ⅱ)的系统调用都是由高层语言实现的, 例如C语言.在μC/OS-Ⅱ的源代码中, 系统调用是用C语言编写的, 被分为8个类别.针对系统调用, 验证方法分为3步:(1)从系统调用的自然语言规范中提取性质, 并将提取的性质采用霍尔逻辑进行描述; (2)将霍尔逻辑表达式以注释的形式插入到系统调用的源程序相应位置, 这中间也涵盖了循环不变式等; (3)利用验证工具VCC对插入后C代码进行验证.如果通过验证, 则表示该程序满足性质; 如果验证失败, 则需要分析反例, 对验证代码进行修正, 重新验证直至验证通过.
1.3 混合语言程序的验证方法为了提高操作系统的性能及对计算机硬件的访问, 操作系统内核中有一部分采用汇编语言编写.混合语言程序的验证大多采用对两种语言的代码分别验证, 或者采用将高层语言映射到底层语言上验证.
μC/OS-Ⅱ核心服务程序是用C语言和汇编语言编写, 而汇编代码的执行通常是内嵌到C语言中, 因此, 这里采取了一种自下而上的策略, 通过将底层汇编程序抽象, 映射到高层语言中, 然后在一致的框架中验证.具体的验证流程如图 3所示.
|
Fig. 3 Verification flow of mixed programs 图 3 混合程序的验证流程 |
首先, 对核心服务程序中的汇编语言代码和C语言代码进行分离; 其次, 对汇编语言代码进行抽象和建模, 对抽象模型采用高层可验证的语言进行实现; 然后, 将抽象模型的实现和原混合程序中的C代码进行粘合, 形成新的混合可验证的高层模型; 接着, 将内核核心服务的性质从其自然语言规范中提取出来, 其中包括C语言和汇编语言程序需满足的性质, 并采用霍尔逻辑描述; 最后, 将所要验证的性质插入到新的高层模型中, 运用自动化验证工具对其验证.若提示验证错误, 则需根据反例, 对程序进行分析修正, 直至验证通过.若提示验证通过, 则表示所验证的程序满足提取的性质.
2 混合语言的抽象建模操作系统是对资源的管理, 不可避免地需要对硬件资源进行访问操作.为提高效率, 特别是在上下文切换、中断机制中, 通常得使用汇编语言.针对μC/OS-Ⅱ内核代码, 存在两种混合形态:(1) C代码内嵌汇编的混合程序, 即在C语言编写的程序中调用汇编代码; (2)汇编内嵌C混合程序, 即在由汇编语言编写的程序中调用C代码.
对于混合代码的验证, 有两种方法:一种是将C语言编译, 然后反汇编, 形成汇编代码, 在汇编代码的基础上验证; 一种是将汇编代码抽象, 形成高层模型, 能够与C语言的代码在基于C的验证工具上完成验证.本文将采用第2种方法, 以便能够使用验证工具VCC进行验证.
为了能够对包含汇编代码的混合代码进行验证, 需要将汇编程序转换成抽象模型, 使其能够在基于C程序验证的工具VCC中表示, 并与C程序共同验证.
2.1 汇编语言的抽象建模为了能够在基于C语言程序的验证工具上验证汇编和C语言的代码, 需要将汇编程序抽象, 建立了一个抽象状态机来模拟指令的执行.提取在μC/OS-Ⅱ中使用汇编指令, 并针对μC/OS-Ⅱ中使用的语义对汇编指令抽象, 得到一个抽象的汇编语言, 这个抽象的汇编语言可以认为是原汇编语言的一个子集.根据抽象的汇编语言, 给出了汇编语言的操作语义, 然后在操作语义的基础上通过VCC建立了他的抽象机模型, 以模拟抽象的汇编语言指令的执行.
抽象模型定义为
| $\tau :\mathit{Pro}{\mathit{g}_{C + ASM}} \mapsto \mathit{Pro}{\mathit{g}_{C + Model}}. $ |
这里, ProgC+ASM表示C语言和汇编语言的混合程序.混合代码经过转换后, 形成了C代码和抽象模型混合程序, 用ProgC+Model符号表示, 转换后的程序可以通过基于C语言的验证工具VCC验证, 解决了由C语言和汇编语言构成的混合程序无法直接验证的问题.
2.1.1 汇编语言语法为了对汇编程序进行抽象建模, 需要定义所使用的汇编语言的子集.针对不同的操作系统, 对应的使用汇编语言的子集也是不同.这里针对μC/OS-Ⅱ中所使用的汇编语言来提取子集.由于不同硬件平台的汇编语言是不相同的, 但对汇编程序抽象建模的方法始终是不变的.在此, 以MCF平台上运行的内核代码为例阐述建立抽象模型的方法.下面给出了μC/OS-Ⅱ内核代码中所使用到的MCF汇编语言子集的BNF表示.
| $\begin{array}{l} Instr :: = Opcode src, des|MOVE.P (sp) + , des|MOVE.P src, - (sp)\\ Opcode :: = ORI|LEA\\ P :: = B|W|L\\ src :: = Dgpr|Agpr|[X]|SR|(Val)Agpr|Val\\ des :: = Dgpr|Agpr|[X]|SR|(Val)Agpr\\ Var :: = Byte|Word|Int \end{array} $ |
MCF汇编语言采用的是三段式结构, 从左至右依次为操作符(Opcode)、源操作数(src)和目的操作数(des).语法定义中的操作符涵盖了MOVE指令、ORI指令和LEA指令.
在MCF汇编语言中, 源操作数可以是一个立即数Val、一个内存区域[X]、一个数据通用寄存器(Dgpr)、一个带字节偏移或不带字节偏移的地址通用寄存器(Agpr)、或者一个状态寄存器(SR).目的操作数和源操作数类似, 但不能为立即数.在MCF汇编语言中, 源操作数和目的操作数不能同时为内存区域.
MOVE指令是将源操作数的值赋给目的操作数.MOVE指令分为MOVE.B、MOVE.W、MOVE.L这3种形式, 那么P可以是B, W或L, 分别用于对字节类型(8位)、字类型(16位)和双字类型(32位)的操作数进行处理.
MCF汇编指令中没有pop指令和push指令来对堆栈操作, 而是借用MOVE指令来实现堆栈的入栈和出栈. MCF平台上的堆栈增长方向是从高地址到低地址.MCF平台规定了A7可用作硬件堆栈指针sp.将源操作数写为(sp)+是出栈操作, 即将堆栈顶部值赋给目的操作数, 然后将堆栈指针向下移动一个数据类型单元.同理, 将目的操作数写为-(sp)是压入堆栈, 此时, 堆栈指针向上移动一个数据单元.
ORI指令是将两个操作数进行按位或, 其中, 源操作数应为立即数, 目的操作数为数据通用寄存器.
LEA指令将有效地址加载到其目标地址中.
2.1.2 辅助函数的定义抽象建模中, 由于汇编语言和高级语言的差异性, 以及汇编语句会涉及到诸多关于硬件的操作, 我们需要定义一些辅助函数用于建立准确的抽象模型.
MCF平台的汇编程序中对数据的操作都是在固定长度的寄存器中进行的, 最终传递给相应的C语言程序变量.但C语言程序中具有不同类型的变量, 其所对应的存储长度也不一致, 因此在对汇编程序中数据与C语言变量交互的过程进行建模时, 势必存在着数据转换步骤.
定义1(MCF数据类型定义).变量x可以为自然数和整型, 其中, 自然数定义为下列3种数据类型之一.
| $\begin{array}{l} {\mathbb{N}_{32}}(x)\mathop = \limits^{{\rm{def}}} 0 \le \;x\; < \;{2^{32}}{\rm{, }}\\ {\mathbb{N}_{16}}(x)\mathop = \limits^{{\rm{def}}} 0 \le \;x\; < \;{2^{16}}{\rm{, }}\\ {\mathbb{N}_8}(x)\mathop = \limits^{{\rm{def}}} 0 \le \;x\; < \;{2^8}{\rm{.}} \end{array} $ |
整型可以定义为下列两种数据类型之一.
| $\begin{array}{l} {\mathbb{Z}_{32}}(x)\mathop = \limits^{{\rm{def}}} {2^{ - 31}} \le \;x\; < \;{2^{31}}{\rm{, }}\\ {\mathbb{Z}_8}(x)\mathop = \limits^{{\rm{def}}} {2^{ - 7}} \le \;x\; < \;{2^7}{\rm{.}} \end{array} $ |
定义2(数据转换).下面两个函数分别用于将自然数转换为整数以及将整数转换为自然数.
| $\begin{array}{l} {\mathbb{N}_n}2{\mathbb{Z}_z}(x)\mathop = \limits^{{\rm{def}}} \left\{ {\begin{array}{*{20}{l}} {x - {2^z}, {\rm{ }}{2^{z - 1}} \le x < {2^n} \wedge n \ge z}\\ {x, {\rm{其他}}} \end{array}} \right.{\rm{, }}\\ {\mathbb{N}_z}2{\mathbb{Z}_n}(x)\mathop = \limits^{{\rm{def}}} \left\{ {\begin{array}{*{20}{l}} {x, {\rm{}}(0 \le x < {2^n} \wedge z > n) \vee (0 \le x < {2^{z - 1}} \wedge z \le n)}\\ {Invalid, {\rm{其他}}} \end{array}} \right.{\rm{.}} \end{array} $ |
其中, n和z的值可以是8, 16, 32中的一个.函数的输出如果为Invalid, 则表示转换过程中发生了数据溢出.
硬件访问是由汇编程序进行, μC/OS-Ⅱ内核的汇编语句中的操作数全部为整数.寄存器中存储的数据用以下的形式描述, 其中, GPR表示通用的寄存器:
| $Type(GPR)\mathop = \limits^{{\rm{def}}} {\mathbb{Z}_{32}}. $ |
谓词逻辑用于对寄存器的个数及其能处理的数据类型进行了描述.在下面的谓词逻辑公式中, GPR(A)代表地址通用寄存器, GPR(D)代表数据通用寄存器.谓词逻辑的表述如下所示.
| $\begin{array}{l} Type(GPR(A))\mathop = \limits^{{\rm{def}}} (|A| = 8) \wedge (\forall i < 8):{\mathbb{Z}_{32}}(A[i]){\rm{, }}\\ Type(GPR(D))\mathop = \limits^{{\rm{def}}} (|D| = 8) \wedge (\forall i < 8):{\mathbb{Z}_{32}}(D[i]){\rm{.}} \end{array} $ |
定义3(GPR的读写).对通用寄存器组r的第i个寄存器的读写操作由以下函数定义:
| $\begin{array}{l} GPR{\rm{ - }}read(r, i)\mathop = \limits^{{\rm{def}}} \left\{ {\begin{array}{*{20}{l}} {r[i], {\rm{ }}0 \le i < 8}\\ {0, {\rm{ }}其他} \end{array}} \right.{\rm{, }}\\ GPR{\rm{ - }}write(r, i, x)\mathop = \limits^{{\rm{def}}} \left\{ {\begin{array}{*{20}{l}} {x \Rightarrow r[i]{\rm{, }}0 \le i < 8}\\ {invalid, {\rm{ }}其他} \end{array}} \right.{\rm{.}} \end{array} $ |
汇编程序抽象模型的建立与硬件的结构相关, 主要是CPU所涉及到的寄存器.
汇编程序的执行涉及寄存器、堆栈和内存, 而对于内存的读写, 是通过C语言的变量来实现的.因此, 为汇编程序建立的抽象模型类似于状态机, 涉及到了程序状态、堆栈指针、以及状态转移关系等.
定义4(抽象模型).基于汇编语言子集和MCF的硬件组件, 其抽象模型MCFASM是一个三元组的结构:
| $MC{F_{ASM}}\mathop = \limits^{{\rm{def}}} (S, sp, \delta ). $ |
其中, S代表抽象模型的状态, sp表示堆栈指针, δ表示状态转移关系.
定义5(抽象模型的状态).抽象模型状态是一个三元组, 它的定义为
| $S\mathop = \limits^{{\rm{def}}} Dgpr \times Agpr \times SR {\rm{.}} $ |
抽象模型的状态包括数据通用寄存器Dgpr、地址通用寄存器Agpr、状态寄存器SR.数据和地址通用寄存器的类型都是32位的整型, 状态寄存器是16位的自然数.数据通用寄存器不仅可以用于存储整数和位域字段, 还可以用作索引寄存器.地址通用寄存器可以用作堆栈指针, 索引寄存器和基地址寄存器.状态寄存器是一个16位寄存器, 存储着处理器的状态、中断优先级掩码和其他一些控制位.
定义6(栈操作).通过对堆栈指针sp可以进行入栈与出栈的操作, 入栈和出栈的行为可以由下面两个函数来描述:
| $MC{F_{push}}(GPR)\mathop = \limits^{{\rm{def}}} - - sp \wedge (sp) \Leftarrow GPR $ | (1) |
| $MC{F_{pop}}(GPR)\mathop = \limits^{{\rm{def}}} GPR \Leftarrow (sp) \wedge + + sp $ | (2) |
其中,
●定义6中的(1)描述了将通用寄存器中的数据压入到堆栈的过程:第1步, 先将堆栈指针sp向上移动一个单位; 第2步, 将将通用寄存器中的数据存入到当前堆栈指针sp所指向的位置.
●定义6中的(2)描述了出栈的过程:第1步, 将当前堆栈指针sp所指向的区域位置中所存的值取出, 并传放置到通用寄存器中; 第2步, 再将堆栈指针sp的指向向下移动一个单位.
定义7(转移关系).转移关系δ描述了整个汇编程序的执行, 其定义如下.
| $\delta \mathop = \limits^{def} S \times sp \times Instr \to S \times sp $ | (3) |
定义7中的表达式(3)描述了抽象模型状态S和堆栈指针sp在执行了汇编指令Instr后发生的变化.表 1中定义了汇编语言的子集的操作语义, 通过操作语义定义抽象模型的转移关系.总共分为7种情况.
|
Table 1 Transition relation of abstract model 表 1 抽象模型的转移关系 |
表 1列出了内核代码中汇编程序所涉及到的所有指令的操作语义, 通过操作语义, 给出在抽象模型中状态转移关系.另外, 在汇编程序中还应用了跳转指令, 即JSR跳转指令.关于对JSR指令的含义及抽象, 我们将在后文中单独进行介绍.
在编号为1的转移中, MOVE指令将源操作数src的值传递给目的操作数des, 其中, src和des均不能为sp.在编号为2的转移中, src是带有偏移值的堆栈指针, 且des不能是堆栈指针, MOVE指令从堆栈的指定地址中读取数据.例如, 堆栈结构如图 4所示:在执行MOVE.W 10(A7), D1汇编指令之前, 如图 4中左方所示的堆栈指针指向A7+0, 且D1=0;而在执行该指令之后, 状态s已经发生了变化, 即D1=5, 但堆栈指针并没有移动, 如图 4中右方所示.类似地, 在编号为3中, src不是堆栈指针, 此时的des是带有偏移值的堆栈指针, 将源操作数存储到堆栈的指定地址上, 堆栈指针的指向不发生改变.
|
Fig. 4 Direction of stack pointer after instruction MOVE 图 4 指令MOVE后栈指针指向 |
在编号为4的转移中描述了出栈的操作, 其中, 源操作数为堆栈指针后偏移一个单位, 目的操作数不能同时为堆栈指针.size(P)表示一个数据单位, 即当前指令所处理数据的字节长度.这一汇编语句表述了先将堆栈指针指向的数据传给目的操作数, 然后堆栈指针向下偏移size(P)个字节长度.同样地, 在编号为5的转移中描述了入栈操作, 其中, 源操作数不是堆栈指针, 目的操作数是一个堆栈指针且要上移一个单位.与出栈不同的是, 入栈过程中先将栈指针向上偏移size(P)个字节长度后, 再将源操作数的数据存储到当前堆栈指针所指向的地方.
编号为6的转移中描述了按位逻辑或的操作, 源操作数应是一个立即数.执行完逻辑或语句后, 将结果存储到目的操作数中.编号为7的转移中描述了如何对指针进行调节的操作, 其中, x源操作数是一个带有偏移量的堆栈指针, 目的操作数为堆栈指针.如图 5所示的堆栈结构执行LEA 4(A7) A7语句, 图 5中A7+0表示堆栈指针所指向的地方.在执行语句之前, 堆栈指针指向的是数字21的正上方; 在语句执行之后, 堆栈指针向下偏移4个字节, 堆栈指针指向了数字21的正下方, 且堆栈中存储的数据没有发生任何变化.注意:在MCF硬件平台中, 地址寄存器A7用作硬件堆栈指针.
|
Fig. 5 Direction of stack pointer after instruction LEA 图 5 指令LEA后栈指针的指向 |
2.3 汇编语言子集与抽象模型的一致性问题
抽象模型MCFASM的状态是建立汇编语言的可编程模式, 对任何一种汇编语言, 它的可编程模式包括通用寄存器和状态寄存器.另外, 由于堆栈寄存器是一个比较特殊的寄存器, 这里把该寄存器单独出来, 在后面的上下文切换中可以更清楚地表示.这样, 在抽象模型MCFASM中的状态S和堆栈就建模了汇编语言的可编程模式.
状态转移关系δ实际描述了在该编程模式下, 汇编语言子集的操作语义.
抽象模型建立了一个抽象机, 通过抽象机模拟硬件的汇编语言的执行环境.由于这里用到的汇编语言的子集并不涉及特殊硬件, 那么汇编语言子集构成的汇编程序在抽象机上的运行与在具体硬件上的执行是一致的.
2.4 混合语言的建模过程μC/OS-Ⅱ内核的混合代码中的C语言程序和汇编语言程序并不是互相独立存在的, 而是通过两种代码的交叉协作执行来保证内核的正常运行.我们采用将混合代码中的底层汇编程序抽象到上层来同C代码形成新的可验证的高层模型.
在μC/OS-Ⅱ内核中, C语言和汇编程序的交叉协同执行过程如图 6所示.μC/OS-Ⅱ中的混合语言程序分为两种形式:(1) C内嵌汇编程序; (2)汇编内嵌C程序.在C语言的代码中, 调用汇编语言函数的程序称为C内嵌汇编程序, 如图 6所示的task.c文件中的main(·)函数调用在汇编语言函数OSCtxSw.在汇编程序中调用C语言函数则称之为汇编内嵌C程序, 例如图 6中的汇编函数OSCtxSw中调用了由C语言编写的OSTaskSwHook函数.我们将分别介绍对这两种形式的混合语言程序建模的步骤.
|
Fig. 6 Program calling sequence 图 6 程序调用顺序 |
2.4.1 C内嵌汇编程序的建模
在图 6中, C语言程序中的main(·)函数调用了汇编函数OSCtxSw属于C内嵌汇编程序.μC/OS-Ⅱ内核在创建了多个任务后, 一个任务在执行完后或者被另一个任务所抢占, 操作系统进行任务切换.在任务运行时, CPU中的寄存器存储当前任务的相关数据, 切换任务后, CPU的寄存器存储下一个即将执行的任务所需要的数据.为此, 执行OSCtxSw函数进行上下文切换.
图 7展示了对图 6中的C内嵌汇编程序建模的过程:先从C内嵌汇编的混合程序中将汇编程序剥离出来; 再对剥离出来的汇编程序建立三元组的抽象模型; 然后对汇编程序进行分析, 建立其状态转移关系, 至此抽象模型建立完成; 最后对抽象模型用工具实现, 替代原来混合程序中的汇编代码, 形成新的可验证的高层语言.
|
Fig. 7 Modeling of C inline assemble program 图 7 C内嵌汇编程序的建模过程 |
2.4.2 汇编内嵌C程序的建模
在图 6中, 汇编函数OSCtxSw内部中有一个无条件跳转指令JSR, 执行该汇编指令后, 将立即跳转到JSR指令制定的地址, 即C函数OSTaskSwHook所在的位置, 执行完该C函数后, 立即返回到原JSR指令的下一条指令处继续执行汇编程序.实际上, 这段代码是汇编函数OSCtxSw对C函数OSTaskSwHook的调用, 即汇编内嵌C程序, 而OSTaskSwHook函数是一个C内嵌汇编的函数, 这里存在着多层的混合调用的关系.
对图 6中的汇编内嵌C程序建模的流程如图 8中所示.首先, 需要对汇编内嵌C程序中的OSTaskSwHook代码剥离出来; 其次, 由于剥离出来后的OSTaskSwHook代码是一个C内嵌汇编代码, 对OSTaskSwHook代码采用前面提到的“C内嵌汇编程序建模”的方法, 将其转化为C代码混合抽象模型; 接着, 将C代码混合抽象模型内联到OSCtxSw汇编代码中, 形成了汇编内嵌C代码混合抽象模型; 最后, 由于混合代码又被顶层的C代码进行调用, 因此, 结合上层的C代码后又可以将其视为C内嵌汇编混合程序, 再次采用C内嵌汇编建模方法, 使其最终成为C代码混合抽象模型.
|
Fig. 8 Modeling process of assemble inline C program 图 8 汇编内嵌C程序的建模过程 |
这里定义了汇编程序抽象模型, 针对内核代码中两种形态的混合代码, 给出了它们抽象建模的方法.
3 抽象模型的实现有了汇编程序的抽象模型以及混合语言的建模方法, 如何将其转换为能够在基于C语言的验证工具上实现呢?这里使用自动化验证工具VCC对抽象模型实现.
VCC[14, 32]是源代码级并发C程序的自动化推理验证工具, 用于证明C语言程序其功能规范的正确性.VCC工具链允许使用函数合约和数据结构的不变量对并发C程序进行模块化验证.函数合约由前置条件和后置条件指定.VCC是基于注释的系统, 即合约和不变量作为注释插入在源代码中, 其方式对于常规的非验证的编译器是透明的.验证工作过程分两个步骤.
●第1步, VCC工具将注释的C代码转换为用于验证的BoogiePL[33]中间语言, 然后通过Boogie[34]工具将其转化为一阶逻辑表达式.其中, BoogiePL是一种带有嵌入式断言的简单命令式语言, 它很容易生成一组一阶逻辑公式, 表明程序应该满足性质, 并以断言的形式呈现.
●第2步, 利用Z3求解器对转换后的一阶逻辑表达式进行验证.Z3求解器会返回两种结果:(1)一阶逻辑表达式通过验证; (2) Z3返回一个反例或者提示超时.
3.1 VCC中Ghost语句语法从VCC的视角, 一切都被视为对象.每一个对象都是彼此独立的, 它们的类型和地址都是唯一定义的, 每个对象都有一组字段.这些字段也彼此独立, 每个字段都有其类型.对象类别分为两种:一种是具体类型, 另一种是Ghost类型.
具体类型对象对应运行程序中实际存在的变量或数据结构.具体类型对象拥有固定的存储区域, 且任意两个具体类型对象的存储区域都不会发生重叠.具体类型对象对应的是C程序的一部分.Ghost类型对象只存在于验证的过程中, 该对象不是C程序的一部分.
Ghost类型对象是验证工程师为了验证而手动添加的辅助代码, 添加的这段代码称为Ghost代码, 通常写为_(ghost …)形式.其中, Ghost代码无法直接改变具体类型对象的值, C代码也不能直接更改Ghost类型对象的值.
在VCC中, 如果定义一个Ghost函数, 可使用_(def …)语句, 这个语句被称为“纯函数”, 其对整个程序的执行没有副作用.Ghost代码和C代码的关系类似于汇编代码与C代码的关系, 因此本文利用Ghost语言实现汇编语言的抽象模型.Ghost语言是一种类C的语言, 它的语法定义如下.
| $\begin{array}{l} program:: = ghost\;stmt1|def\;stmt2|typedef\;stmt3\\ stmt1:: = X = Exp\;stmt1|Type*ptr\;stmt1 \\ stmt2:: = FunctionName(Type\;Id).Block\;stmt2\\ stmt3:: = struct\;varDeclaration* Id\;stmt3|Type{\rm{\;}}X\;stmt3\\ Exp:: = n|X|{e_0} + {e_1}|{e_0} - {e_1}|{\rm{true}}|NOT e|{e_0}|{e_1}|{e_0} \ll n \end{array} $ |
Ghost定义以ghost、def、typedef为关键字的宏注释代码中.
Exp声明是在Ghost中的表达式, 可以是一个立即数、一个变量、多个原子表达式的加减或者逻辑运算、移位运算等.
关键字ghost的宏注释代码可以定义赋值、变量申明语句.关键字为def的宏注释代码用于定义相关的Ghost辅助函数.关键字为typedef的宏注释用来定义一个新的Ghost数据类型或者结构体.
3.2 抽象模型的实现汇编程序的抽象模型是包含状态S、堆栈指针sp以及转移关系δ的三元组.程序状态S用Ghost结构体MCF_c表示.MCF_c结构体中的3个元素依次对应了数据寄存器、地址寄存器和状态寄存器, 抽象模型的状态S和堆栈指针sp的定义如下.
1. _(typedef struct MCF_Hardware_struct{
2. MCF_B32t D[8];
3. MCF_B32t A[8];
4. MCF_B16t SR;
5. }MCF_c; )
6. _(ghost MCF_B32t *SP)
在μC/OS-Ⅱ通过只使用一个硬件指针实现了将即将运行的任务控制块(OSTCB)的内容从内存区域中加载到寄存器中, 或者将当前正在运行任务的内容存储到相应的任务控制块中.
MCF_B16t类型和MCF_B32t类型是我们自定义类型, 它们分别对应了无符号16位整型和无符号32位整型, 通过使用关键字typedef定义, 如下:
_(typedef unsigned short MCF_B16t)
_(typedef unsigned long MCF_B32t)
抽象模型中的状态S包括数据通用寄存器、地址通用寄存器和状态寄存器, 这3个成员在实现中分别对应于数组D[8]和A[8]和变量SR, 抽象模型的堆栈指针sp对应于实现中的*SP.在Ghost语句中, 使用了关键字ghost对指针*SP进行了定义.
抽象模型中的状态转移关系δ表示了抽象模型执行汇编语句前后状态变化.在第2.2节中给出了内核汇编代码中所涉及到的7种状态转移关系.这7种状态转移关系的实现见表 2中.
|
|
Table 2 Code implementation of state transition 表 2 状态转移的代码实现 |
表 2中, src和des对应MCF_c结构体里的成员, 即数组D和数组A.表 2中, 名为val的变量代表了一个立即数.变量SP表示了一个全局的堆栈指针, 定义的堆栈指针SP指向单位长度为4字节的存储区域.Ghost变量对应着不同的数据类型, 不同的数据类型的长度也是不同的, 且只能对符合类型的数据进行操作.因此, 抽象模型的实现存在着数据类型的转换过程.在Ghost代码实现中, 堆栈指针SP指向的是一个4字节的数据, 数组成员D[1]也是存储4字节的数据.如果要实现汇编指令取出2字节的操作, 需要进行两次数据转换:第1步, 先将SP指向的4字节数据转换为2节的数据; 然后, 再将2字节的数据转换成4字节数据, 并将它传递给MCF_c抽象模型的结构成员D[1]中.另外, \old(E)在VCC的环境中用于记录表达式E在函数入口处的值.在验证工作中, 通常会利用\old(E)来计算循环次数, 或者用来证明在程序执行之前和之后的状态转移关系的正确性.
下面代码中给出了这种转换的过程.第2行、第3行定义了两个Ghost临时变量, 16位的Temp整型变量和32位的Temp32整型变量.首先, 将堆栈中指定地方的值取出来放到Temp32变量中; 其次, 将Ghost变量Temp32传递给Ghost辅助变量类型转换函数Conv_to_B16(MCF_B32t), 该函数的输入为一个32位的整型数值, 输出的结果为一个16位的整型数值.在Ghost语句中, 将Conv_to_B16(MCF_B32t)的输出值赋给变量Temp; 最后, 利用Ghost辅助变量类型转换函数Conv_to_B32(MCF_B32t)将Temp变量的值转化为32位整型数值并将该数值赋给MCF的D[1]成员.
1. _(ghost MCF_c *MCF)
2. _(ghost MCF_B16t Temp)
3. _(ghost MCF_B16t Temp32)
4....
5. _(ghost Temp32=*(SP+10))
6. _(ghost Temp=Conv_to_B16(Temp32))
7. _(ghost MCF→D[1]=Conv_to_B32(Temp))
8....
3.3 C代码和抽象模型的粘合在μC/OS-Ⅱ的内核代码中, 汇编程序和C程序分别定义在两种不同类型的文件中.C语言定义的程序具有高移植性, 汇编语言定义的程序可以对内核运行的硬件平台进行访问控制, 内核的正常运转离不开这两种语言程序的协作运行.这两种不同语言程序的协作, 是通过在各自程序中调用另一语言定义的函数完成的.
在VCC设计理念中, Ghost语言只存在于验证过程中, 不能直接影响原程序的执行.本文采用了Ghost代码模拟了汇编程序的执行.但在OS实际运行过程中, 汇编语言程序与C语言程序之间存在数据的交换.为了解决抽象模型Ghost代码与C代码数据交换的问题, 提出了在纯函数中添加VCC合约语句, 见下面的代码.
1. _(def INT32U Assignment(MCF_B32t p))
2. _(ensures \result==p)
3....)
第1行的关键字def定义了一个Ghost纯函数Assignment(·), 其返回值为无符号32位整数.第2行Ghost纯函数的入口处添加了后置条件_(ensures\result==p), 该后置条件表述了Ghost纯函数Assignment(·)的返回值应为p.
通常在VCC中, 函数入口处的前置条件和后置条件是函数应该满足的性质.但是在函数体不为空时, 直接在验证函数的入口处添加前置条件或后置条件, VCC认为该性质描述语句是重言式, 然后可以通过Ghost语句将Assignment(·)的返回值赋给一个具体类型对象.例如, 在C语言程序中的有一个类型为无符号32位的StoreValue变量, 需要将抽象模型中D0的值赋值给C语言的变量StoreValue, 此时使用下列语句就可以实现汇编指令与C语言代码的通信.
1. _(ghost StoreValue=Assignment(MCF→D[0]))
同理, 也可以通过Ghost纯函数Assignment(·)将具体变量的值传递给Ghost类型变量.借助于在定义的Ghost纯函数中添加断言的形式, 成功地模拟出C代码和抽象模型之间的数据通信.这样, 抽象模型的实现模拟了汇编指令的执行, 并可以与C代码一起在VCC上运行.
这部分给出了高层实现语言Ghost代码的语法定义, 通过该Ghost语言对抽象模型中三元组的各个元素进行具体实现, 最后介绍了如何将抽象模型的实现, 以及抽象模型与内核中C代码的粘合.
4 验证μC/OS-Ⅱ及其分析我们运用前面提出的验证框架验证了基于μC/OS-Ⅱ的商用实时操作系统内核, 包括近8 000行的C代码和100多行的汇编代码(去除了空格和注释), 分为系统调用8个模块的验证和混合语言实现核心服务程序的验证.
4.1 VCC的基础知识前面已经提到, VCC是基于C语言代码的验证, 其所要验证的性质是以注释的形式给出的, 如下面的代码, 在函数体内只含有1条注释语句.
1. #include 〈vcc.h〉
2. int main(void){
3. int a, b, c;
4. if (a≥b)
5. c=a;
6. else c=b;
7. _(assert c≥a)
8. return 0;
9. }
注意到, 在VCC验证环境中, 每个程序都包含vcc.h头文件, 该头文件给出关于VCC相关宏、函数的定义.该程序中第7行使用了语句_(assert E), 并通过注释定义的, 其中, assert是标记; E是一个表达式, 表示尝试在程序的当前点证明表达式是否成立.如果验证程序成功, 则表示该表达式在程序的每次执行中都成立.这和C语言中的断言函数不一样, 因为C语言中断言函数运行成功, 表示这次的运行是满足该断言的, 并不意味着它将在下次执行时能再次成功.
4.2 系统调用的验证μC/OS-Ⅱ内核中一共74个系统调用, 分别为任务管理、内存管理、消息队列、信号量、邮箱、互斥量信号量、时间管理和事件标志等8大模块.在验证过程中, 根据需求提取出每个系统调用需要满足的性质, 性质是基于Hoare逻辑的形式给出的, 并采用VCC提供的合约或者断言的形式, 以注释的方式插入到源代码中.在系统调用的验证中, 所要验证的性质大体可分为下列3个大类:类型检查、安全性和边界检查.系统调用的验证性质见表 3.系统调用的8个模块列于表 3的第1列中, 相对应的每个模块中所验证的系统调用个数列于表的第2列, 每一个模块所提取的性质列在了表的第3列.在74个系统调用中添加了共653条性质, 并完成了验证.
|
|
Table 3 Property extraction of system call 表 3 系统调用性质提取 |
4.2.1 性质的提取
VCC通过验证C语言程序与其性质的一致性, 来证明程序的功能正确性.在μC/OS-Ⅱ的需求规范中, 面临着以下3个问题:(1)自然语言易产生二义性, 造成因不同人的理解而导致代码功能实现的差异; (2)自然语言规范的书写没有一个严格的标准, 导致不同的人对需求规范的表述存在着较大的差异; (3)还没有一种工具能够直接完全的将自然语言规范转换为工具能够识别的性质.因此, 在性质的提取过程中, 还是人手工抽象的.
VCC验证时, 需要从自然语言规范中提取性质并转换, 并将其插入到C语言程序的适当位置.这里以创建任务的系统调用OSTaskCreate的验证为例, 给出如何提取性质, 并将性质添加到源代码中.
系统调用OSTaskCreate(task, p_arg, OS_STK, ptos, prio), 其接口的自然语言规范表述如下.
(1) task是一个指向任务代码的指针.
(2) p_arg是指向一个可选择数据区域的指针, 用于给相应任务初次运行时传递所需的参数.
(3) ptos是指向任务栈栈顶的指针, 这个栈是用于在中断时存储本地变量、函数参数、返回地址以及CPU寄存器.当OS_STK_GROWTH设置为1时, 认为指针是从高地址往低地址移动, 为0的时候则反向.
(4) prio是任务的优先级, 一个优先级最多只能对应一个任务且数字越低表示越高的优先级.
由于task是指向任务代码的指针, 对于该规范这里抽象为指向代码段的指针, 即若该指针是指向代码段的某个地址, 则认为其是正确的.针对上述4个参数的自然语言规范, 转化后的性质描述见表 4.
|
|
Table 4 Parameter property description of API OSTaskCreate() 表 4 OSTaskCreate(·)参数性质描述 |
对于所有输入参数的约束, 都是属于前置条件, 对于它们的验证语句都是放置在_(requires …)的前置条件语句中, 前置条件语句应插入至函数的入口处.这里的code是抽象地表示了指当前验证的指针所应指向的代码段区域, zone也是表示了相应的数据区域块.针对不同的硬件架构, 代码段区域和数据段区域是不同的, 因此在验证不同架构的函数过程中, code和zone是需要验证人员根据该架构的存储地址的分配进行手动配置的.
除了对入口参数进行性质的提取, 还需要在验证中添加相应的性质.如在系统调用xQuery(arg1, arg2)(查询互斥信号量的当前状态)中, arg1参数是要查询的信号量, arg2参数是用于存放查询到的状态信息, 性质添加见下面的代码.
1. INT8U OSMutexQuery(OS_EVENT*pev, OS_MUT_DATA*p_mut_data)
2. _(requires is_pointer2ECB(pev, Ecb_mut))
3. _(maintains \arrays_disjoint(p_mut_data→OSEventTbl,
4. OS_EVENT_TBL_SIZE, pev→OSEventTbl, OS_EVENT_TBL_SIZE))
5. _(writes \span(p_mut_data))
6. _(ensures \result==OS_NO_ERR$\Rightarrow$\forall unsigned m;
7. m < OS_EVENT_TBL_SIZE$\Rightarrow$
8. p_mut_data→OSEventTbl[m]==pev→OSEventTbl[m])
9. {
10....
11. for (i=0; i < OS_EVENT_TBL_SIZE; i++)
12. _(invariant psrc== & pev→OSEventTbl[0]+i)
13. _(invariant pdest== & p_mut_data→OSEventTbl[0]+i)
14. _(invariant \forall unsigned n; n < i$\Rightarrow$
15. p_mut_data→OSEventTbl[n]==pev→OSEventTbl[n])
16. {
17. *pdest++=*psrc++;
18. }
19....
20. }
第2行的前置条件要求pev是一个指向某个已有的互斥量的指针.第3行、第4行的表达式描述了所要查询的信号量当前的存储区域与用于存放信号量的存储区域在函数执行前后都没有发生重叠.第5行表达了存放信号量的区域在本函数中是可写的.第6行~第8行的式子是一个后置条件, 该表达式描述了当函数的返回值为OS_NO_ERR时, 要查询互斥量的相关信息已经成功复制到所要储存的区域中.第12行~第15行是我们从规范中提取的3条循环不变式语句, 它们表述了每执行一次循环, 当前的源地址和目的地址始终是初始地址加上当前的循环控制量i.对于已经赋过值的元素, 其值应该是相等的.OSMutexQuery(arg1, arg2)函数所需要验证的性质位于第2行~第8行、第12行~第15行, 添加完所有必要的注释代码后, 则可以将注释C程序放置于VCC环境中进行验证.
4.3 核心服务程序的验证μC/OS-Ⅱ内核的核心服务程序是以混合语言(即C语言和汇编语言)实现, 其中, 汇编语言完成有关中断控制、上下文切换以及寄存器读写的操作.为了实现对混合语言程序的验证, 将汇编程序转换为抽象建模, 并在VCC中实现.而对性质的提取、性质的形式化描述与系统调用的方法是相同的.我们在验证中是针对程序是否严格满足所要求的需求规范进行分析验证.如果满足, 则表示功能正确; 反之, 表示软件存在缺陷.在本文中, 需求规范亦是需要证明是否完全充分和正确, 关于需求规范的验证则不是本文所研究的范围.
这里以函数OSIntExit(·)为例介绍混合语言程序的验证过程, 该函数同时包含了第2.4节中介绍的两种形式的混合语言程序.
OSIntExit(·)函数用于通知操作系统中断服务程序已经完成了执行, 需要退出中断服务程序.它通常与进入中断服务程序OSIntEnter(·)函数成对出现.每次调用OSIntEnter(·)都会对中断嵌套深度变量IntNesting加一, 而OSIntExit(·)是对该变量进行减一操作, 其中, 中断嵌套的深度IntNesting是一个全局变量.当最后一层的中断服务执行完后, 如果当前就绪队列中有一个任务的优先级高于原被中断任务的优先级, 则启动任务调度功能.此时, 中断执行完成后将返回到就绪队列中优先级最高的任务, 而不一定是返回到最初被中断的任务.
在执行OSIntExit(·)程序的临界区代码段之前, 应禁用外部中断以保证其临界区代码的执行不会被打断.这里将状态寄存器作为抽象模型中状态S的一个成员, 它是MCF_c结构体类型的SR变量成员.函数OSIntExit(·)的验证代码如下.
1. void OSIntExit(void)
2. _(writes OSIntNesting & & ...)
3. _(requires OSIntNesting > 0)
4. _(maintains \arrays_disjoint(SP, 16, MCF→D, 8)
5. & & \wrapped(MCF))
6. _(ensures OSIntNesting==0 & & OSLockNesting==0
7. $\Rightarrow$OSCtxSwCtr==\old(OSCtxSwCtr)+1
8. & & OSPrioCur==OSPrioHighRdy)
9. {
10. _(unwrap MCF)
11. _(ghost SaveSR_DisableInt(MCF))
12. _(ghost cpu_sr=Assignment(MCF→D[0]))
13....//Dec. 1 of OSIntNesting
14....//If OSIntNesting==0 & & OSLockNesting==0
15....//Switch to highest priority task
16. OSTaskSwHook(·);
17. _(ghost MCF→D[0]=OSPrioHighRdy)
18. _(ghost OSPrioCur=Assignment(MCF→D[0]))
19. _(ghost SP=OSTCBHighRdy→OSTCBStkPtr)
20. _(ghost MCF→D[0]=*SP++)
21....//Restore registers from stack
22....//Restore SR from D0
23. _(wrap MCF)
24. }
源程序在执行临界区代码之前需要关掉中断, 即在第11行, 通过调用纯函数SaveSR_DisableInt(·)来实现. SaveSR_DisableInt(·)函数先将当前状态寄存器的值存储到数据寄存器D0中, 然后更新状态寄存器中的中断控制位以屏蔽中断请求.OSIntExit(·)函数从此处开始执行临界区代码.由于抽象模型MCF成员的值会被SaveSR_ DisableInt(·)修改, 使得抽象模型的对象不变性无法保持, 因此需要将MCF切换到open状态才能进行有关成员的修改, 即我们在第10行中添加了一个unwrap的子句.在再次包裹MCF之前(第23行), 应该恢复状态寄存器的中断控制位(第22行), 从而MCF的对象不变性又得以保持(第23行).
每次执行OSIntExit(·)函数, 都会使得OSIntNesting的值减1.当中断嵌套深度为0(即OSIntNesting==0)、调度程序已解锁(即OSLockNesting==0), 并且被中断的任务不是就绪队列中优先级最高的任务(第11行~第14行)时, 则发生任务切换.然后将当前任务优先级参数设置为最高可运行优先级(OSPrioCur=OSPrioHighRdy), 并从新任务的任务栈中的信息恢复至CPU寄存器中(第16行~第20行).第2行~第6行中列出了性质规范.
4.4 验证结果与分析验证包括了13个C语言文件、2个头文件以及1个汇编语言文件, 共计6 446行C语言程序和100行的汇编语言程序(除去了代码中所有的注释和空行), 添加了936行性质验证代码和205行的抽象模型的代码实现, 抽象模型实现与汇编代码的比例约为2:1.
μC/OS-Ⅱ内核总共验证出10个缺陷, 分布于7个功能函数中.验证出的缺陷可分为两类.
●类型不匹配.在程序代码中难免会存在一些数据类型的转换, 不同数据类型之间的赋值操作需要进行强制转换.例如, 在某段程序中的计算赋值语句spoke=Match%SIZE, 经过验证发现两边数据类型不一致.我们定位到源代码中发现赋值语句左侧的类型是INT16U, 而右侧是INT32U, 这条语句计算的结果可能会导致spoke变量发生类型溢出.
●数据溢出.该类缺陷出现的原因在于程序的需求规范缺少对相关的数据的详细约束说明.比如, 调度函数OS_Sched(·)中的全局变量OSCtxCtr是一个上下文切换计数器.OS_Sched(·)每执行一次, OSCtxCtr变量加1, 但是整个内核系统代码中没有一处可以对这个全局变量OSCtxCtr进行重置的操作.因此, 该变量会一直累加下去, 程序运行到某个时刻, 此变量会发生溢出.
我们将以上验证结果反馈给企业的开发人员, 得到了他们的认可.
5 验证框架的评估针对μC/OS-Ⅱ内核, 上述工作是基于MCF平台上的内核代码进行的.由于内核可能运行在不同的硬件平台上, 本文提出的验证框架具有通用性, 可以运用于不同平台上的操作系统内核的验证.为此, 我们验证了ARM Cortex-M3平台上的μC/OS-Ⅱ内核代码.由于硬件平台的不同, 内核的汇编代码部分的不同, 发现在CM3版本的内核代码中存在优先级反转问题.
5.1 ARM平台下的验证为了证明该验证框架的可行性和可扩展性, 我们还尝试将其应用于CM3平台.由于μC/OS-Ⅱ内核具有高可移植性, 因而大多数代码与硬件无关, 只有少量汇编代码与硬件平台相关.在验证CM3平台时, 需要抽象一个新的汇编程序的抽象模型.有关CM3硬件结构的详细说明, 请参考文献[35].同样地, CM3平台的抽象模型仍是一个三元组, 但是三元组的每个成员发生了变化.其中, 状态S变成了16个寄存器; 状态寄存器SR也发生了变化, 不是一个16位的状态寄存器, 而是一个中断控制相关的特殊寄存器的组合; 状态转移关系δ也因汇编语句的变化而发生了变化.尽管抽象模型发生了变化, 但是建立抽象模型的方法和MCF平台上的方法一样, 只是外在的表现形式不同而已.
表 5将两个平台上的验证结果进行了对比.由于系统调用代码与硬件无关, 因此系统调用验证的可重用性达到100%.核心服务程序的可重用率达到67.6%, 操作系统的总可重用性为83.8%.根据表 5中的内容显示, 本验证框架具有验证其他任意平台上的μC/OS-Ⅱ内核的能力.
|
|
Table 5 Verification and comparison of different platforms 表 5 不同平台的验证比较 |
5.2 缺陷分析
在系统调用中检测到的缺陷, 在不同的平台验证都是一样的, 因为C语言编写的代码是与平台无关的.但是CM3平台发现了两个与优先级反转相关的缺陷, 而出现优先级反转的原因是与CM3平台的硬件架构有关.
相比较之下, 在MCF平台上没有出现优先级反转的原因在于, 其与CM3平台采用了不同方式实现上下文切换.CM3平台通过PendSV实现上下文切换, 即可悬挂请求.PendSV是一个中断驱动程序, 为系统级服务的最低优先级, 因此它也受硬件中断控制位控制.而MCF平台使用陷阱指令实现上下文切换.MCF陷阱指令不受中断控制位控制, 即使中断被禁止也可立即执行上下文切换.
在对任务队列的建模过程中, 可以将所有的任务抢占过程分解为为两个任务或者3个任务抢占.所以本文采用了两步走的方法来建模任务切换过程:第1步, 假设当前有一个任务A正处于运行的状态, 并且任务队列中只有另外一个任务B处于就绪状态, 就绪任务B会去抢占任务A的运行, 通过验证抢占过程来验证程序的调度性问题; 第2步, 假设当前有一个任务A正处于运行的状态, 并且任务队列中存在两个任务处于就绪状态, 即任务B和任务C, 通过验证这3个任务同时抢占的过程来验证抢占调度机制的正确性.
图 9阐述了在CM3上发生优先级反转的情况:一开始, 高优先级任务A处于运行状态, 低优先级任务B处于就绪状态; 然后任务A被延时, 此时立即调用调度器进行任务切换.在执行任务调度之前, 需要禁用中断控制位, 并更新相关信息, 使得任务B在上下文切换后顺利进入到运行状态.
|
Fig. 9 Priority inversion of platform CM3 图 9 CM3平台优先级反转示例 |
此时运行的状态是OSPrioCur=H, OSTCBCur=A, OSPrioHighRdy=H, OSTCBHighRdy=B, 其中, OSPrioCur为当前运行任务的优先级, OSTCBCur是当前运行任务的任务控制块, OSPrioHighRdy是就绪队列中可运行的最高优先级任务的优先级, OSTCBHighRdy是就绪队列中可运行的最高优先级任务的任务控制块.
但是在禁用中断的情况下, 不能立即执行上下文切换.如果在中断禁用期间有新的中断使任务A进入到就绪状态, 该中断会调用调度器, 再次更新信息.此时的运行的状态是OSPrioCur=H, OSTCBCur=A, OSPrioHighRdy=L, OSTCBHighRdy=B.这样, 就绪队列中最高优先级任务为A, 但是最高优先级任务的任务控制块为任务B的.因此, 中断位使能后, 并且没有除PendSV之外的其他的中断等待执行, 则PendSV立即执行.执行的代码是OSPrioCur=OSPrioHighRdy, OSTCBCur=OSTCBHighRdy, 也就是OSPrioCur=H, OSTCBCur=B.发现系统运行的是B任务, 但它的优先级变成了A的, 导致A任务从此以后一直无法得到执行.
VCC的验证原则是将验证合同转换为BoogiePL中间语言, 最后转换为一阶谓词逻辑, 可使用Z3求解器进行求解.Z3求解器是基于SMT, 具有强大而有效的推理和分析功能.有许多公式可以使用VCC的推理功能进行验证, 例如等式、不等式、加法、减法、常数乘法和布尔连接词.但是涉及非线性的计算、位矢量证明.例如位相关的验证, VCC不能进行验证.MCF平台上验证μC/OS-Ⅱ时遇到了无法直接对位进行验证的问题, 为此我们提出了比较有技巧性地验证位操作的方法, 详细见下面代码.
1. _(ghost MCF→SR=OS_INITIAL_SR)
2....
3. _(ghost MCF→SR=MCF→SR|0x0700) //Disable interrupt
4. _(assert \forall int x, y; Bv_lemma(x|(y & MCF→SR), 8)
5. ==(Bv_lemma(x, 8)|Bv_lemma(y, 8)))
原汇编程序的运行中, 机器状态(SR)会经常需要进行置位和复位的操作, 例如, 通过修改机器状态的相应控制位来使能和禁止外部中断.而在程序验证过程中, 由于VCC引擎对相应的位矢量验证存在着缺陷, 在验证的过程中需要验证人员采用一定的手段告知引擎相应的位已被修改, 如此才能确保Ghost代码准确地模拟了汇编程序的执行过程.我们在验证过程中使用Ghost语句的宏定义定义了Bv_lemma的纯函数, 用于取出数据中相应的位, 然后采用一阶逻辑公式表述位矢量应满足的关系.
6 总结本文工作主要的目的是将形式化方法应用于工业界, 也就是在项目开发的过程中, 采用了一边开发、一边采用形式化方法进行验证的方法.在业界, 软件的开发是根据需求规范而来的, 最终开发的软件如果严格满足需求, 则认为开发的软件不存在问题.因而, 我们的验证团队根据判断开发的程序是否严格满足所要求的需求规范:如果满足, 则表示功能正确; 反之, 则表示软件存在缺陷.在项目开发中, 需求规范亦需要证明是否完全充分和正确, 关于需求规范的验证则不是本文所研究的范围.我们所使用的规范, 对程序中每一个变量进行了详细的说明, 如果程序中多定义, 或者存在规范未描述的状态, 我们亦认为代码功能不正确.
本文提出了一个通用的嵌入式操作系统内核自动化验证框架, 该验证框架支持对C语言程序和C语言与汇编语言混合程序的验证.为了检验本框架的可行性, 以商用实时操作系统μC/OS-Ⅱ的内核作为研究对象, 运用本验证框架, 通过验证工具VCC, 完成了该内核的系统调用及混合代码的验证.本框架分别应用于μC/OS-Ⅱ的两个不同硬件平台上, 以证明本验证框架的有效性和通用性.并且通过验证发现了一些系统缺陷, 包括系统调用的缺陷和与硬件平台不同而出现的缺陷.
操作系统内核的高可靠性是非常重要的, 今后将把重点放在以下3个方面的分析与验证上.
●规范层面上的形式化验证.规范是用于描述一个系统应该具备的功能, 然而对于规范的书写大多采用的是自然语言.一个程序的正确性与其规范息息相关, 规范的正确性是程序正确性的前提.
●内存保护机制和信息流安全.当前的工作涉及对调度机制、中断处理、操作系统内核的资源管理的功能验证.为了实现μC/OS-Ⅱ的全面验证, 内存保护机制和信息流安全是内核的重要组成部分, 对其进行验证分析也是非常重要的.
●时间属性的分析.由于μC/OS-Ⅱ是一个实时操作系统, 时间特性也是需要关注的方面.
| [1] |
Ehrenfeld JM. Wannacry, cybersecurity and health information technology: A time to act. Journal of Medical Systems, 2017, 41(7): Article No.104.
[doi:10.1007/s10916-017-0752-1] |
| [2] |
Mohurle S, Patil M. A brief study of wannacry threat: Ransomware attack 2017. Int'l Journal of Advanced Research in Computer Science, 2017, 8(5): 1938-1940.
http://cn.bing.com/academic/profile?id=85c16e424ef14af40f0876f98d82ee47&encoded=0&v=paper_preview&mkt=zh-cn |
| [3] |
Lipp M, Schwarz M, Gruss D, et al. Meltdown. arXiv preprint arXiv: 1801.01207, 2018.
|
| [4] |
Kocher P, Genkin D, Gruss D, et al. Spectre attacks: Exploiting speculative execution. arXiv preprint arXiv: 1801.01203, 2018.
|
| [5] |
Simakov NA, Innus MD, Jones MD, et al. Effect of meltdown and spectre patches on the performance of HPC applications. arXiv preprint arXiv: 1801.04329, 2018.
|
| [6] |
Klein G, Elphinstone K, Heiser G, et al. seL4: Formal verification of an OS kernel. In: Proc. of the Symp. on Operating Systems Principles. ACM, 2009, 207-220.
http://d.old.wanfangdata.com.cn/NSTLQK/NSTL_QKJJ0223674090/ |
| [7] |
Klein G, Andronick J, Elphinstone K, et al. Comprehensive formal verification of an OS microkernel. ACM Trans. on Computer Systems (TOCS), 2014, 32(1): 1-70.
http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=2872bd98f4a3401167763dc5fb749fd3 |
| [8] |
Paulson LC. Isabelle: A Generic Theorem Prover. Springer Science & Business Media, 1994.
http://d.old.wanfangdata.com.cn/Periodical/jfjlgdxxb200805010 |
| [9] |
der Rieden TI, Tsyban A. CVM—A verified framework for microkernel programmers. Electronic Notes in Theoretical Computer Science, 2008, 217: 151-168.
[doi:10.1016/j.entcs.2008.06.047] |
| [10] |
Baumann C, Beckert B, Blasum H, et al. Formal verification of a microkernel used in dependable software systems. In: Proc. of the Int'l Conf. on Computer Safety, Reliability, and Security. Berlin, Heidelberg: Springer-Verlag, 2009, 187-200.
http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=CC0210036506 |
| [11] |
Daum M, Schirmer NW, Schmidt M. Implementation correctness of a real-time operating system. In: Proc. of the 7th IEEE Int'l Conf. on Software Engineering and Formal Methods. IEEE, 2009, 23-32.
http://cn.bing.com/academic/profile?id=61b00806308507177d2e169bf0c9be17&encoded=0&v=paper_preview&mkt=zh-cn |
| [12] |
Baumann C, Beckert B, Blasum H, et al. Lessons learned from microkernel verification—Specification is the new bottleneck. arXiv preprint arXiv: 1211.6186, 2012.
|
| [13] |
Baumann C, Beckert B, Blasum H, et al. Better avionics software reliability by code verification. In: Proc. of the Embedded World Conf. Nuremberg, 2009.
|
| [14] |
Cohen E, Dahlweid M, Hillebrand M, et al. VCC: A practical system for verifying concurrent C. In: Proc. of the TPHOLs., 2009, 23-42.
http://d.old.wanfangdata.com.cn/Periodical/bjyddx201202024 |
| [15] |
Kaiser R, Wagner S. Evolution of the PikeOS microkernel. In: Proc. of the 1st Int'l Workshop on Microkernels for Embedded Systems., 2007, 50-57.
https://www.researchgate.net/publication/285592141_Evolution_of_the_PikeOS_Microkernel |
| [16] |
Chlipala A. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, 2013.
|
| [17] |
Gu R, Koenig J, Ramananandro T, et al. Deep specifications and certified abstraction layers. ACM SIGPLAN Notices, 2015, 50(1): 595-608.
[doi:10.1145/2775051.2676975] |
| [18] |
Costanzo D, Shao Z, Gu R. End-to-end verification of information-flow security for C and assembly programs. ACM SIGPLAN Notices, 2016, 51(6): 648-664.
[doi:10.1145/2980983.2908100] |
| [19] |
Gu R, Shao Z, Chen H, et al. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In: Proc. of the 10th USENIX Symp. on Operating Systems Design and Implementation (OSDI 2016)., 2016, 653-669.
http://cn.bing.com/academic/profile?id=d155a792b3ea0929fac87a04989867ae&encoded=0&v=paper_preview&mkt=zh-cn |
| [20] |
Chen H, Wu XN, Shao Z, et al. Toward compositional verification of interruptible OS kernels and device drivers. ACM SIGPLAN Notices, 2016, 51(6): 431-447.
[doi:10.1145/2980983.2908101] |
| [21] |
Nelson L, Sigurbjarnarson H, Zhang K, et al. Hyperkernel: Push-button verification of an OS kernel. In: Proc. of the 26th Symp. on Operating Systems Principles. ACM, 2017, 252-269.
http://d.old.wanfangdata.com.cn/Periodical/jsjkx200812039 |
| [22] |
Xu F, Fu M, Feng X, et al. A practical verification framework for preemptive OS kernels. In: Proc. of the Int'l Conf. on Computer Aided Verification. Cham: Springer-Verlag, 2016, 59-79.
http://cn.bing.com/academic/profile?id=170486b9cc9d98fcbc0671b99c890252&encoded=0&v=paper_preview&mkt=zh-cn |
| [23] |
Xu FW. Design and implementation of a verification framework for preemptive OS kernels [Ph.D. Thesis]. Hefei: University of Science and Technology of China, 2016(in Chinese with English abstract).
|
| [24] |
Ma JB, Fu M, Feng XY. Formal verification of the message queue communication mechanism in μC/OS-Ⅱ. Journal of Chinese Computer Systems, 2016, 37(6): 1179-1184(in Chinese with English abstract).
[doi:10.3969/j.issn.1000-1220.2016.06.012] |
| [25] |
Labrosse JJ. C/OS-Ⅱ The Real-Time Kernel User's Manual. Rev.2.92.17, 2019. https://doc.micrium.com/pages/viewpage.action?pageId=10753158&preview=/10753158/20644170/100-uC-OS-II-003.pdf
|
| [26] |
Zhao Y, Sanan D, Zhang F, et al. Refinement-based specification and security analysis of separation kernels. IEEE Trans. on Dependable and Secure Computing, 2017, 16(1): 127-141.
http://cn.bing.com/academic/profile?id=c1942c90e8b3b52d9485e6fb8d65995d&encoded=0&v=paper_preview&mkt=zh-cn |
| [27] |
Zou L, Lv JD, Wang SL, et al. Verifying Chinese train control system under a combined scenario by theorem proving. In: Proc. of the Working Conf. on Verified Software: Theories, Tools, and Experiments. Berlin, Heidelberg: Springer-Verlag, 2013, 262-280.
http://cn.bing.com/academic/profile?id=058528c6e60a85f4fa1c98d47e7e6fed&encoded=0&v=paper_preview&mkt=zh-cn |
| [28] |
Ding JZ. Formal verification and analysis of RTOS kernel [MS. Thesis]. Shanghai: East China Normal University, 2019(in Chinese with English abstract).
|
| [29] |
Freescale Semiconductor. Mcf5441x Reference Manual. Rev.4, 2012.
|
| [30] |
Freescale Semiconductor. Coldfire Family Programmer's Reference Manual. Rev.303, 2005.
|
| [31] |
Yiu J. The Definitive Guide to ARM® Cortex®-M3 and Cortex®-M4 Processors. Newnes, 2013.
|
| [32] |
Moskal M, Schulte W, Cohen E, Hillebrand MA, et al. Verifying C programs: A VCC tutorial. 2012. https: //archive.codeplex.com/?p=vcc
|
| [33] |
DeLine R, Leino KRM. BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report, 2005. https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2005-70.pdf
|
| [34] |
Barnett M, Chang BYE, DeLine R, et al. Boogie: A modular reusable verifier for object-oriented programs. In: Proc. of the Int'l Symp. on Formal Methods for Components and Objects. Berlin, Heidelberg: Springer-Verlag, 2005, 364-387.
http://d.old.wanfangdata.com.cn/NSTLHY/NSTL_HYCC025313578/ |
| [35] |
ARM® Cortex®-M3 Processor Technical Reference Manual. Rev.r2p1, 2015. https://static.docs.arm.com/100165/0201/arm_cortexm3_processor_trm_100165_0201_01_en.pdf?_ga=2.256657411.904144181.1588151964-699243147.1588151964
|
| [23] |
许峰唯.抢占式操作系统内核验证框架的设计和实现[博士学位论文].合肥: 中国科学技术大学, 2016.
|
| [24] |
马杰波, 付明, 冯新宇. μC/OS-Ⅱ中消息队列通信机制的形式化验证. 小型微型计算机系统, 2016, 37(6): 1179-1184.
[doi:10.3969/j.issn.1000-1220.2016.06.012] |
| [28] |
丁继政.实时操作系统内核的形式化验证与分析[硕士学位论文].上海: 华东师范大学, 2019.
|