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

徐家乐 等: 操作系统内核权能访问控制的形式验证 3575

供权能管理基础服务, 包括权能内核对象和权能操作, 并在此之上分别对微内核其他功能模块, 如分区管理、任务
管理、通信和时间管理的资源和服务进行权能管理. 以任务管理为例, 是对任务管理的各个任务程序上, 分别添加
权能管理部分, 配合权能管理基础服务, 实现权能控制和管理. 前面提到的 seL4, 在设计时将权能作为基本对象,
权能和系统调用深度绑定, 所有的系统操作都是基于一套消息传递的系统调用, 系统调用在执行时需要先确认所
需的权能合法. 两者相比, seL4 对于权能控制可以直接得到底层系统支撑, 执行效率比较高; 而本文插桩式的权能
访问机制部署起来比较灵活, 通用性和可移植性更强. 下面我们对本文所研究的权能访问控制设计进行介绍.
权能访问控制实现对微内核资源的细粒度访问控制. 系统每创建一个任务时, 会同时创建一个与该任务绑定
的权能空间, 该权能空间中存储当前任务对于内核各种资源访问的权限. 当任务在运行过程中调用 API 接口时, 权
能访问控制组件会通过当前任务的优先级获取其对应的权能空间指针, 并进入存放 API 服务对应权能的地址, 查
看当前任务是否具有该 API 服务所对应的权能. 如果是, 将可以正常使用该内核服务, 调用 API 接口执行操作; 否
则将被拒绝, 返回无权限错误码. 为了防止用户对权能空间的修改, 所有与权能相关的数据结构对象都被放置在内
核空间.
微内核权能机制提供基础的权能操作, 包括权能的移动、复制、删除、撤回等, 实现对任务权能空间的管理.
系统初始化后会创建一个根任务, 其权能空间包括对所有内核资源的操作权限. 其他任务的权能都是根任务权能
的子集. 具体来说, 当一个父任务派生一个子任务时, 子任务通过权能操作从父任务继承权能, 因此子任务权能是
父任务权能的子集.
我们从权能数据结构、权能操作函数和其他功能模块 API 函数的权能扩展这 3 个方面进行介绍.

3.1 权能数据结构
图 2 中定义了任务的权能数据结构, 由结构体 cspace 定义. 节点 cnode 存储任务的权能信息, 由结构体 cte 定
义, 其中数组 slots[SlotNum] 中每个元素 (slot 被称为槽) 存储该任务的一个权能. 结构体 slot 定义了槽的类型和权
能, 权能有两种不同类型的权能: 函数权能 (对应于 category 类) 和对象权能 (对应于 object 类), 它们的内容和值统
一由联合体 content 定义. 函数权能表示是否具有调用某个内核函数的权限, 而对象权能管理系统运行过程中生成
的各个内核对象的权限, 包括任务控制块对象、信号量对象、互斥量对象、消息队列对象等. 每个任务的权能空
间还存储由其演化出的子任务的权能空间指针, 由 cspacechildren[MaxChildNum] 表示. 从子任务又可以递归地演
化出多个其子任务, 它们的权能空间形成一棵树的结构.

cspace cte capability
cnode slotnum type
childnum slots[SlotNum] content
cspacechildren[MaxChildNum]
category
OSCSpaceNext
content
slot right
type
cspace_1
object
capability
right
... objectptr

cspace_CNum

图 2 任务权能数据结构