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

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

表 2 Coq 验证代码统计

函数名称 函数代码行数 验证代码行数
grant_cap_kernel 18 709
grant_cap 35 1 160
cnode_mint_kernel 31 2 550
cnode_mint 45 1 305
cnode_copy_kernel 50 4 608
cnode_copy 55 2 480
cnode_move_kernel 55 5 445
cnode_move 57 3 208
cnode_mutate_kernel 31 1 356
cnode_mutate 43 1 580
cnode_delete_kernel 38 1 008
cnode_delete 33 1 940
deleterec 30 2 996
cnode_revoke_kernel 14 336
cnode_revoke 40 1 120
check_cap_type 63 2 390
get_obj_slot 24 1 294
总计 662 35 485

在下一步的工作中, 我们将研究权能验证过程的部分自动化, 为验证过程中大量相似的赋值操作和判断操作
定义证明策略. 我们还考虑进一步将这些封装成通用的接口来供其他验证者使用. 具体思路是, 首先, 将数组、指
针、结构体、联合体等不同类型的数据结构分别定义为统一的断言形式, 支持从特定类型数据结构到断言的自动
生成; 其次, 以上不同数据结构的赋值语句和判断语句实质上都可以分解为求地址和从地址中取值两类操作的组
合, 而又由于这些操作具有普适性, 我们将考虑针对寻址和求值定义统一的证明策略, 提高含有不同数据结构的赋
值和判断语句的证明自动化程度. 以上关于不同数据结构断言的自动生成和自动验证策略的定义, 可以在操作系
统其他模块甚至含有数据结构程序的验证中进行复用.
我们在验证过程中发现了权能访问控制模块代码实现中存在的问题, 并得到设计方的确认, 在新版本中得到
更正并重新验证通过. 错误主要包括以下几种类型.
1) 临界区保护不充分问题. 例如, deleterec 函数的执行完全没有临界区保护, 另一个并行的任务可能在 cap 的
重置过程中, 同时对这个权能结构进行操作, 从而造成数据争用问题. 其他权能函数具有同样的问题.
2) 递归引起的错误删除问题. cnode_revoke 函数在实现中检查并返回在参数 prio 任务中相应的参数 capability
权能的位置, 对当前任务和它的后代都删除这同一个位置的权能. 当 prio 为操作权能时没有问题. 但对于对象权能
来说, prio 任务的 capability 权能的位置, 与它的后代的 capability 权能的位置很可能并不一样, 但是实现中使用相
同的位置. 根据设计需求在 Coq 中定义函数的规范之后, 验证中发现了代码实现与规范的不一致, 于是便发现了
cnode_revoke 函数的实现错误, 提交给设计方进行修改. 在新版本中, 函数加入了一个新的参数, 用来存储权能的
位置, 从而, 针对每个后代, 都可以重新去确认 capability 所存储的位置.
3) 权能操作 move 的判断条件问题. 实现中, 在调用权能移动操作时, 允许父任务和后代之间权能的双向移动. 由
于任何两个任务, 都可以通过根任务相互到达, 那么根据传递性, 任意两个任务之间的权能也是可以互相移动的. 这就
造成了, 证明中父任务和子任务之间权能的子集关系不再成立. 在新版本中已经修改, 只允许父任务操作子任务.
4) 条件判断不完备造成的空指针引用问题. 全局变量 CSpacePrioTbl 维护任务的 cspace, 初始值对于任何优先
级为 i 的任务, 对应值为空指针. 当创建一个新的线程或者任务时, 将对应的 cspace 在 CSpacePrioTbl 中初始化为
非空的值. 因此, 并不是对于所有的优先级, CSpacePrioTbl 都是非空的, 只有目前存在的任务的优先级值为非空.
然而, 每次调用用户权能函数的时候, 都没有对任务的权能的相应检查. 在验证中, 发现没有完备的条件判断, 权能
全局不变式无法成立. 在修改版本中, 在 CSpacePrioTbl[i] 可能为空的地方, 都加上了是否为空的判断, 为空直接返
回错误, 不为空进行操作.