Page 149 - 《软件学报》2025年第8期

3572 软件学报 2025 年第 36 卷第 8 期

理、同步和通信、时钟管理等相比, 权能访问控制的数据结构复杂得多. 在实现中, 每个任务的权能空间涵盖指针、
数组、结构体、联合体等数据结构的嵌套; 同时, 所有具有继承关系的任务的权能空间递归形成一颗树状的结构,
而权能访问控制模块需要时刻维护这颗树, 用于追踪任务的原始权能和派生权能之间的关系. 例如, 当撤回一个任
务的某个权能时, 必须要递归删除其所派生出的所有子任务具有的对应权能. 因此, 复杂的共享数据结构访问和修
改、递归函数调用是权能访问控制实现中常见的操作, 是对其进行形式验证必须解决的问题.
在本文中, 我们将对权能的数据结构进行形式建模, 针对权能中的不同结构体、数组、联合体等分别定义断
言进行描述. 这样做的一个优势是, 可以针对权能的特殊数据结构定义统一的引理, 有助于权能函数中共性操作的
验证, 包括临界区内对任务某个权能值的修改或删除、递归删除树中某个类型的权能等. 我们将权能数据结构在
高层抽象为一个映射, 省略了权能树、指针、数组等具体结构信息, 用于权能 API 函数的抽象规范的定义. 具有父
子关系的任务权能之间的关系、底层权能结构和高层权能映射之间的一致关系, 由全局不变式来定义. 此不变式
在验证过程中, 在临界区外是时刻保持成立的, 这保证了权能数据结构的良构性以及高层规范和底层实现的一致
性. 系统 API 函数通常通过调用内部函数来完成功能, 因此, 我们首先定义并验证了内部函数的前后条件规范, 在
此基础上验证了 API 函数的功能正确性, 即 API 函数的具体实现和其抽象规范满足精化关系. 以上的形式化定义
和验证均在 Coq 定理证明器中进行. 我们在验证过程中发现了权能访问控制实现中存在的问题并得到了该微内
核操作系统设计方的确认和修改.
本文第 1 节介绍操作系统内核形式验证的研究现状. 第 2 节介绍本文所需的基础知识, 包括 Coq 定理证明和
并发精化分离逻辑. 第 3 节介绍权能访问控制的设计. 第 4 节展示权能访问控制的形式验证, 包括形式建模、全局
不变式、内部函数和 API 函数的形式规范和验证. 第 5 节分析验证过程中发现的问题和经验. 最后总结全文和下
一步工作.

1 操作系统内核验证相关工作

基于定理证明对操作系统进行形式化验证是近年来学术研究的主要关注点之一, 并已经取得多个成功的应
[3]
用. seL4 隶属于 L4 [12] 微内核家族, 是第 1 个完全形式化证明了功能正确性的操作系统微内核, 验证的内核代码
8 000 多行, Isabelle 证明代码 20 万行左右. seL4 分为 3 层: 抽象规范层, 执行规范层, C 代码实现. 它从设计需求出
发, 定义了描述操作系统性质的抽象规范, 使用 Haskell 语言实现了操作系统内核的执行规范, 此执行规范可以自
动翻译到 Isabelle 中进行定理证明, 同时由于效率方面的原因, 重新手动实现了操作系统内核的 C 代码. seL4 验证
了 Haskell 执行规范是抽象规范的精化, 而 C 代码实现是执行规范的精化, 从而验证了操作系统实现的功能正确
性. seL4 考虑由中断带来的执行不确定和交错并行行为, 但是它处于内核态时并不实时响应中断需求, 而是采取
轮询 (polling) 制, 从内核态显示返回用户态并将中断看作一个新的内核事件进行调用. seL4 还是第 1 个同时支持
并验证了细粒度的权能访问机制的操作系统内核. 与本文相比, seL4 在设计时把权能作为基本对象, 对于权能控
制和访问直接由底层系统支撑, 通过一套消息传递的系统调用来实现; 而本文所研究的微内核权能访问控制是通
过在现有的内核上提供插桩式模块实现的, 提供权能管理基础服务, 并在此之上对现有的功能模块分别添加权能
管理部分, 实现权能控制和管理. 两者相比, 前者执行效率比较高, 而后者通用性和可移植性较强.
耶鲁大学 Gu 等人 [4] 研制了一个经过验证的安全云计算操作系统内核 CertiKOS, 之后 Gu 等人 [13] 提出深层规
范 (deep specifications) 的概念, 将操作系统验证分为不同的抽象层次并提供相应的语言和工具实现不同层次规范
的定义、模块化组合和精化验证. 作为应用, 他们形式验证了 mCertiKOS 内核 (CertiKOS 内核 [4] 的简化单处理器
版本) 的功能正确性, 花费人月数与 seL4 相比有很大降低, 此外还利用深层规范框架验证了带中断的设备驱动程
序的正确性 [5] . 在 CertiKOS 项目基础上, 他们实现了 CCAL 工具集 [6,14] , 提出新的技术来支持多线程和多核的并行
抽象层, 成功设计并验证了一个基于细粒度锁的并行操作系统内核 mC2. 然而, 基于深层规范的验证框架需要引
入大量的函数调用, 来达到具体实现和调用之间的抽象分层, 当应用于已有的操作系统内核的验证时, 如何重新进
行抽象分层和定义深层规范是一个很难的问题.
为了处理并行程序的验证, Liang 等人 [15–17] 提出了基于依赖-保证 (rely-guarantee) 的模拟关系 RGSim, 同时支