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

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

数据结构具有如下的形式定义.

Definition CSpacePrioTbl l ptrvl vl cspacels :=
G& CSpacePrioTbl @ (Tarray (Tptr CSPACE) 64) == l **
Aarray l (Tarray (Tptr CSPACE) 64) ptrvl **
CSpaceAarrayTptr 64 ptrvl vl cspacels
end

其中, 全局变量 CSpacePrioTbl 指向长度为 64 的 CSPACE 类型的数组起始地址 l, cspacels 是从任务权能空间指针
到其优先级的反向映射 (它将在定义不变式中的一致关系时使用, 此处可先不考虑), Aarray 表示带类型和长度的
数组, 它存储指向任务权能空间的指针, 指针值的序列为 ptrvl. CSpaceAarrayTptr 是所有任务的权能空间数据结构
的并, 使用分离合取表示, vl 是所有任务权能的值序列. 递归地, 每个任务的权能数据结构由如下的结构断言 CSpace
定义, 其中参数 l 和 vl 分别表示该任务的权能空间的指针和值.

Definition CSpace l vl cspacels :=
match vl with
| (cnode, childnum, lv, v) =&
let (b, i) := l in
Cnode (b, i) cnode **
PV (b, i + typelen(Cnode) @Tint32| → Vint32 childnum **
Aarray (b, i + typelen(Cnode) + 4) (Tarray (Tcom_ptr cspace) MaxChildNum) lv **
PV (b, i + typelen(Cnode) + 4 + Int.mul MaxChildNum typelen(Tcom_ptr cspace)) @Tcom_ptr CSpace| → v
end

在以上的定义中, 为了突出关键结构定义, 我们省略了一些类型信息和表示关系的纯断言信息 (以下同). 可以
看到, 每个任务的权能空间包括 4 部分, 存储在起始地址为 l (由内存块号 b 和偏移量 i 组成) 的一段内存内: 权能
节点 Cnode, 两个 PV 断言定义基本类型的值和指针, 分别表示子任务的个数和下一个权能空间指针, Aarray 定义
当前任务演化出的子任务的权能空间指针所组成的序列. 可以看到, 每个断言对应的偏移量都是起始量 i 和前面
断言所占的内存的累加和. 权能节点 Cnode 对应的断言如下.

Definition Cnode l cnode :=
match cnode with
| (slotnum, slots)
=> let (b, i) := l in
PV (b, i)@Tint32 | → Vint32 slotnum **
Slots (b, i + 4) SlotNum slots
end
Cnode 定义的方式类似, 但是与 CSpace 具有不同的结构, 包括类型为整型的权能槽 slot 的数目和存储权能值
slot 序列的 Slots 断言. 每一个 slot 表示一个权能, 它由一个 union 类型定义, 有两种不同的类型的权能, 由 Cap 断
言定义. 以下定义中, cap_type 表示权能的类型, 两个整型值 x 和 y 构成一个 category 权能, x 和指针 z 构成一个
object 权能.
Definition Cap l v :=
match v with