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

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

4.3 权能内部函数和 API 函数的规范与验证
操作系统内核的正确性可以归结为, API 函数的实现是其高层规范的精化, 其中高层规范定义相应函数的功
能正确性需求. 在实现中, API 函数会调用内核中的内部函数, 因此 API 函数的正确性依赖于内部函数的正确性.
我们本节将介绍 API 函数和内部函数在 CSL-R 中不同的证明模式.
下面的章节中, 我们将分别选择 grant_cap_kernel 和 cnode_revoke 作为代表, 来介绍我们的验证过程. 前者是
为任务赋予新的权能的内部函数, 包含对某个具体任务的权能进行赋值的操作, 这些操作在其他权能函数中也广
泛存在; 后者是递归删除某个任务及其所有后代的某个给定权能, 涉及递归不变式的定义和递归函数的验证.

4.3.1 grant_cap_kernel 的建模、规范和验证
如代码 1 所示, grant_cap_kernel 赋予任务 destTask 一个新的 CATEGORY 类型的权能 (class, right), 作为内核
函数, 它具有对任务权能数据结构进行访问和修改的权利. 它首先检查参数的合法性, 若不满足, 将返回 grant_
failure; 若满足, 那么将进行下面一系列的赋值操作: 从 CSpacePrioTbl 出发, 先到达任务 destTask 所对应的权能空
间, 然后到达 class 索引的 slot, 最后将对应的权能类型置为 CATEGORY, 内容置为 class, 权能值修改为原来的值
与参数 right 的或, 即添加 right 这个权能. 代码中“→”和“..”分别表示指针取值和结构体成员访问. 以下 grant_cap_
kernel 函数的实现在 Coq 中定义. 我们不难发现, CSL-R 所定义的 C 语言子集语法, 其外观与 C 语言基本类似, 增
强了模型的可读性, 简化了从 C 代码实现到 Coq 模型的翻译过程.

代码 1. 内核函数 grant_cap_kernel 代码.
Int8u grant_cap_kernel·(Int8u destTask; Int32u class; Int32u right){
1. if(…){
2. return grant_failure;
3. }
4. …
5. CSpacePrioTbl[destTask]→cnode..slots[class]..capability..type = CATEGORY;
6. CSpacePrioTbl[destTask]→cnode..slots[class]..capability..content..category..content =class;

7. CSpacePrioTbl [destTask]→cnode..slots[class]..capability..content..category..right &=4095; s
8. CSpacePrioTbl[destTask]→cnode..slots[class]..capability..content..category..category..right ⊨ right;
}
内核函数的功能正确性由前后条件 (pre-/post-conditions) 规范定义, 其中前条件描述该函数顺利执行需要拥
有的资源以及各种类型变量的值, 而后条件描述内核函数执行后对资源的修改. 对于 grant_cap_kernel 成功执行的
情况, 它的功能正确性需求由以下前/后条件规范定义 (仅列出主要的断言).

{ CSpacePrioTbl l ptrvl vl cspacels ** … }
grant_cap_kernel
{CSpacePrioTbl l ptrvl vl' cspacels ** [|vl' = (update_nth_cspace_slots_cap destTask class priotbl
(CATEGORY, (class, (Right &4095) | right, z))|] **… }

前条件表示当前内核函数获得了权能空间资源的访问权限, 对应于 CSpacePrioTbl 断言表示的所有已有任务
的权能空间; 后条件表示执行该操作后, 依旧持有权能资源的使用权限, 而且将权能值序列 vl 修改为 vl', 其中 vl'
和 vl 满足 [|…|] 内定义的纯断言关系, update_nth_cspace_slots_cap 表示 vl'由 vl 更改对应权能得到, 它将任务
destTask 的权能空间中槽 class 对应的权能根据函数传入的参数进行权能类型、内容和值的修改. Right 和 z 都表
示在初始 vl 中对应的权能值, 这里的 z 是占位符, 对 category 类型权能不起作用.
在 Coq 中对以上规范进行验证时, 需要按照第 4.1 节定义权能结构断言 CSpacePrioTbl 的顺序, 逐层按照参