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

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

系统的权能空间维护已分配的任务权能空间和待分配权能空间. 微内核在启动之后, 将初始化一个权能空间
链表和一个保存所有已创建任务的权能空间指针的数组 CSpacePrioTbl. 在任务相继创建后, 系统的权能空间信息
由多个数组和链表维护, 包括已分配任务的权能空间链表 CSpaceList、待分配权能空间的链表 CSpaceFreeList、
任务优先级映射到任务权能空间指针的数组 CSpacePrioTbl, 以及任务优先级映射到任务权能空间中 slot 数组的
空位置的数组 CSpaceObjectPointer. 上面我们提到, 每当任务使用内核服务时, 将检查它所对应的权能, 而对其权
能的查找则是从它的优先级出发, 通过 CSpacePrioTbl 数组索引, 到达它的权能空间. 而对任务赋予新的对象权能
时, 也是从其优先级出发, 通过 CSpaceObjectPointer 数组索引, 到达该任务权能 slot 数组的第 1 个空位置, 将其存
储在该位置并同时将该指针移向下一个空位置.
从图 2 及以上介绍可以看出, 权能空间比较复杂, 包括结构体、数组、指针、联合体、链表等不同类型的数
据结构以及它们的嵌套, 而且, 不同任务的权能空间构成多个树结构, 以维护任务及其后代之间权能的一致关系.
本文中, 我们将对 CSL-R 逻辑框架提供的数据结构断言进行扩展, 对权能数据结构进行形式建模.

3.2 权能操作函数
微内核操作系统允许任务调用权能函数, 实现赋予权能、移动权能、删除权能等操作, 其中每个操作都需要
当前任务具备相关的权能操作的权限, 以及当不同任务之间移动或拷贝权能时, 需要源任务与目标任务之间存在
父子关系. 微内核权能操作的概述如表 1 所示, 其中每个权能 API 函数都是通过调用对应的内核函数 (文中也称
为内部函数) 来实现.

表 1 权能函数的 7 种操作

操作 API函数 描述
赋予 grant_cap 为任务赋予新的权能
铸造 cnode_mint 用指定的权能当作模板, 铸造一个新的权能, 这个权能的权限只能变小
复制 cnode_copy 将源任务的权能复制到目标任务对应的权能中
移动 cnode_move 将源任务的权能复制到目标任务对应的权能中, 然后将源任务的这个权能清空
铸造并移除 cnode_mutate Mint+Move, 然后将源任务中的权能删除
删除 cnode_delete 删除源任务中特定 slots中的权能
撤销 cnode_revoke 删除当前权能节点所具备的权能以及递归地删除当前权能的后代节点具有的权能

3.3 其他功能模块 API 函数的权能扩展
在以上权能访问机制基础上, 操作系统内核其他涉及内核对象的功能模块需要进行权能管理扩展, 例如任务
管理、信号量、互斥量、消息队列、定时器等模块. 具体扩展方法是, 在调用内核函数进行操作前, 必须检查执行
操作的任务是否具备该操作相应的权限; 当具备相应权限时, 具体功能的实现与扩展前一致.
本文中我们关注的权能性质包括以下 3 类: 全局资源不变式, 即在任务执行过程中, 临界区之外, 权能数据结
构总是满足一定的不变式; 功能正确性, 即权能操作实现了正确的功能; 其他函数的权能扩展性质, 即相应内核函
数的调用只在任务具备相应权限时才能成功进行.

4 权能访问控制模块的形式验证

从权能访问控制模块的 C 代码实现出发, 我们在定理证明器 Coq 中开展了权能访问控制模块的形式建模和
验证. 以下将从权能数据结构建模、权能全局不变式、权能内核函数和 API 函数的规范与验证这 3 个方面进行
展开.

4.1 权能数据结构建模
我们由顶向下介绍权能数据结构的形式建模. 通过分析权能模块 C 代码的实现, 对于任务权能的查找和修改
都是从全局数组变量 CSpacePrioTbl 出发, 经过优先级索引到达任务的权能空间进行操作. 因此, 与代码一致, 权能