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

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

7. if(z == success){
8. return revoke_success;
9. }else{
10. return revoke_failure;
11. }
}

内部函数 cnode_revoke_kernel 的函数代码 (实现 2) 首先取值 prio 任务对应的权能节点, 然后在不为空的情况
下, 调用 deleterec 函数进行实际递归撤销操作, 并且返回 success, 其他情况均为错误情况, 返回 failure.
实现 2. 函数 cnode_revoke_kernel 代码.

Int cnode_revoke_kernel (Int8u prio, Int8u type, Int8u capability)
{
1. cspace* pcspace;
2. pcspace = OSCSpacePrioTbl[prio];
3. if(pCSpace != NULL){
4. deleterec(pcspace, type, capability);
5. }else{
6. return success;
7. }
8. return failure;
}

内部函数 deleterec 的函数代码 (实现 3) 先删除当前节点 cspace 对应的权能, 然后初始化一个变量 i 为 0, 将
其用作循环变量, 递归调用 deleterec 函数来删除后代所有节点的权能.

实现 3. 函数 deleterec 代码.

void deleterec (CSPACE* cspace, Int8u type, Int8u capability)
{
1. … /*分为 category 和 object 两种情况分类讨论, 删除 cspace 对应的权能*/
2. Int8u i = 0;
3. while(i < cspace → childnum){
4. deleterec(cspace → cspacechildren[i], type, capability);
5. i++;
6. }
}

基于以上函数调用关系, 实现 1, 2 和 3 共同构成了 cnode_revoke 函数的实现.

4.3.2.2 接口函数 cnode_revoke 的形式规范
由于 API 函数 cnode_revoke 的正确性依赖于内核函数 cnode_revoke_kernel 的正确性, 内核函数 cnode_
revoke_kernel 的正确性依赖于 deleterec 的正确性, 所以我们将按照由底向上的顺序依次建立各个函数的规范.
deleterec 涉及 while 循环和递归调用, 对该函数的规范和验证, 同时具有以下两个需求.
● 使用递归断言来描述函数执行前后权能空间的改变, 对应 while 循环的不变式.