鉴源论坛 · 观模丨µC/OS内核的形式化验证技术

作者 | 郭建上海控安可信软件创新研究院特聘专家

丁继政上海控安研发中心研究员

版块 | 鉴源论坛 · 观模

操作系统作为软件系统的核心，其安全性与可靠性是构造高可信软件最为关键的一步。嵌入式实时操作系统因其具有并发、可抢占以及代码复杂性的特征，给验证工作带来了巨大挑战。我们提出了一种通用的自动化验证框架，借助相关工具，使用本验证框架可对由C语言和汇编语言实现的实时操作系统内核进行自动化验证，从而实现C和汇编的混合代码验证的目标。

01 操作系统内核验证框架

操作系统绝大多数都是采用C语言和汇编语言编写的，对操作系统的验证需要分析C语言、汇编语言和混合语言的验证。我们以µC/OS-II为研究对象，提出了一个通用的自动化验证框架，该框架如图1所示。

图1 操作系统内核自动化验证框架

验证工作分为两个部分：在第一部分中，对由高层语言（如C语言）构成的系统调用进行验证，通过自动化验证工具VCC检查系统调用的源代码与其规范的一致性；在另一部分中，对由高层语言和底层语言（如C语言和汇编语言）构成的内核服务程序进行验证，通过将汇编语言转换成抽象模型，并实现与C语言的粘合，形成符合基于C语言的验证工具（如VCC）能够接收的模型，再利用该工具验证新混合代码。

02 基于验证框架的μC/OS-II内核验证

操作系统是对资源的管理，不可避免地需要对硬件资源进行访问操作。为了提高效率，特别是在上下文切换、中断机制中，通常得使用汇编语言。针对μC/OS-II内核代码，存在两种混合形态：

（1）C代码内嵌汇编的混合程序，即在C语言编写的程序中调用汇编代码；

（2）汇编内嵌C混合程序，即在由汇编语言编写的程序中调用C代码。

为了实现对μC/OS-II内核代码的验证，这里使用自动化验证工具VCC对抽象模型实现。

VCC是源代码级并发C程序的自动化推理验证工具，用于证明C语言程序功能规范的正确性。VCC工具链允许使用函数合约和数据结构的不变量对并发C程序进行模块化验证。函数合约由前置条件和后置条件指定。VCC是基于注释的系统，即合约和不变量作为注释插入在源代码中，其方式对于常规的非验证编译器是透明的。

2.1 抽象模型的实现

汇编程序的抽象模型是包含状态S、堆栈指针sp以及转移关系δ的三元组。程序状态S用Ghost结构体MCF_c表示。MCF_c结构体中的三个元素依次对应了数据寄存器、地址寄存器和状态寄存器，抽象模型的状态S和堆栈指针sp的定义如下：

图 2

在μC/OS-II通过只使用一个硬件指针实现了把即将运行的任务控制块（OSTCB）的内容从内存区域中加载到寄存器中，或者将当前正在运行任务的内容存储到相应的任务控制块中。

MCF_B16t类型和MCF_B32t类型是我们自定义类型，它们分别对应了无符号16位整型和无符号32位整型，通过使用关键字typedef定义，如下：

_(typedef unsigned short MCF_B16t)

_(typedef unsigned long MCF_B32t)

抽象模型中的状态S包括数据通用寄存器、地址通用寄存器和状态寄存器，这三个成员在实现中分别对应于数组D[8]和A[8]和变量SR，抽象模型的堆栈指针sp对应于实现中的*SP。在Ghost语句中，使用了关键字ghost对指针*SP进行了定义。

抽象模型中的状态转移关系δ表示抽象模型执行汇编语句前后状态变化，状态转移关系的实现见表1。

表1 状态转移的代码实现

2.2 C代码和抽象模型的粘合

在μC/OS-II的内核代码中，汇编程序和C程序分别定义在两种不同类型的文件中。C语言定义的程序具有高移植性，汇编语言定义的程序可以对内核运行的硬件平台进行访问控制，内核的正常运转离不开这两种语言程序的协作运行。这两种不同语言程序的协作是通过在各自程序中调用另一语言定义的函数完成的。

在VCC设计理念中，Ghost语言只存在于验证过程中，不能够直接影响原程序的执行。我们采用了Ghost代码模拟了汇编程序的执行。但在OS实际运行过程中，汇编语言程序与C语言程序之间存在数据的交换。为了解决抽象模型Ghost代码与C代码数据交换的问题，提出了在纯函数中添加VCC合约语句，见下面的代码：

图 3

通常在VCC中，函数入口处的前置条件和后置条件是函数应该满足的性质。但是，在函数体不为空时，直接在验证函数的入口处添加前置条件或后置条件，VCC认为该性质描述语句是重言式，然后可以通过Ghost语句将Assignment()的返回值赋给一个具体类型对象。例如，在C语言程序中的一个类型为无符号32位的StoreValue变量，需要将抽象模型中D0的值赋值给C语言的变量StoreValue，此时使用下列语句就可以实现汇编指令与C语言代码的通讯：

图 4

同理，也可以通过Ghost纯函数Assignment()将具体变量的值传递给Ghost类型变量。借助在定义的Ghost纯函数中添加断言的形式，成功地模拟出C代码和抽象模型之间的数据通讯。这样，抽象模型的实现模拟了汇编指令的执行，并可以与C代码一起在VCC上运行。

这部分给出了高层实现语言Ghost代码的语法定义，通过该Ghost语言对抽象模型中三元组的各个元素进行了具体实现，最后介绍了如何将抽象模型的实现，以及抽象模型与内核中C代码的粘合。

03 验证μC/OS-II及其分析

我们运用前面提出的验证框架验证了基于μC/OS-II的商用实时操作系统内核，包括近8000行的C代码和100多行的汇编代码（去除空格和注释），分为系统调用8个模块的验证和混合语言实现的核心服务程序的验证。

3.1 系统调用的验证

μC/OS-II内核中一共74个系统调用，在验证过程中，根据需求，提取出每个系统调用需要满足的性质，性质是基于Hoare逻辑的形式给出的，并采用VCC提供的合约或者断言的形式，以注释的方式插入到源代码中。系统调用的验证性质见表2。

表2 系统调用性质提取

系统调用的8个模块列于表3的第一列中，相对应的每个模块中所验证的系统调用个数列于表的第二列，每一个模块所提取的性质列在了表的第三列。在74个系统调用中添加了共653条性质，并完成了验证。

3.2 核心服务程序的验证

μC/OS-II内核的核心服务程序是以混合语言（即C语言和汇编语言）实现，其中汇编语言完成有关中断控制、上下文切换以及寄存器读写的操作。为了实现对混合语言程序的验证，将汇编程序转换为抽象建模，并在VCC中实现。而对性质的提取、性质的形式化描述与系统调用的方法是相同的。我们在验证中是针对程序是否严格满足所要求的需求规范进行分析验证。如果满足，则表示功能正确。反之，表示软件存在缺陷。

验证包括了13个C语言文件、2个头文件以及1个汇编语言文件，共计6446行C语言程序和100行的汇编语言程序（除去了代码中所有的注释和空行），添加了936行性质验证代码和205行的抽象模型的代码实现，抽象模型实现与汇编代码的比例约为2:1。

μC/OS-II 内核总共验证出10个缺陷，分布于7个功能函数中。

04 总结

本文提出了一个通用的嵌入式操作系统内核自动化验证框架。该验证框架支持对C语言程序和C语言与汇编语言混合程序的验证。为了检验本框架的可行性，以商用实时操作系统μC/OS-II的内核作为研究对象，运用本验证框架，通过验证工具VCC，完成了该内核的系统调用及混合代码的验证。

参考文献：

[1] 郭建, 丁继政, 朱晓冉. 嵌入式实时操作系统内核混合代码的自动化验证框架[J]. 软件学报, 2020, 31(5): 1353-1373.

[2] Klein G, Elphinstone K, Heiser G, et al. seL4:formal verification of an OS kernel[C]. Symposium on Operating Systems Principles. ACM, 2009:207-220.

[3] Cohen E, Dahlweid M, Hillebrand M, et al. VCC: A Practical System for Verifying Concurrent C. Proceedings of TPHOLs, 2009. 23–42.

[4] The Real-Time Kernel: µC/OS-II. http://micrium.com/rtos/ucosii/overview.

[5] Barnett M, Chang B Y E, DeLine R, et al. Boogie: A modular reusable verifier for object-oriented programs[C]. International Symposium on Formal Methods for Components and Objects. Springer, Berlin, Heidelberg, 2005: 364-387.

[6] 马杰波, 付明, 冯新宇. μC/OS-Ⅱ中消息队列通信机制的形式化验证[J]. 小型微型计算机系统, 2016, 37(6):1179-1184.