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

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

def
′
γ cnode_revoke_success (vl) =λΣ,(v,Σ ).∃ prio cspaceid acsapce acspace . ′
vl = (prio :: nil)∧Σ(cspaceid) = acspace∧
′
reset_descendents_cspace_slot_abs prio acspace acspace ∧
Σ = set Σ cspaceid acspace ∧v = success,
′
′
其中, Σ 表示该操作执行之前的抽象状态, v 表示函数返回值. Σ(cspaceid) 表示在抽象状态中获得权能状态 acspace,
由于底层资源进行递归撤销操作, 对应地, 高层资源对高层数据状态进行相同的撤销操作. 函数 reset_descendents_
acspace 对于当前权能节点 prio ′ , ′
cspace_slot_abs 描述高层权能抽象状态 进行递归撤销之后得到 acspace Σ 将 Σ
acspace , 并且返回值为 success.
′
原有的权能状态设置成

4.3.2.3 接口函数 cnode_revoke 的形式验证
下面介绍接口函数 cnode_revoke 的正确性定理表述, 包含该函数的前条件 revokepre 和 revokepost.

def
revokepre =∃v 1 ,v 2 ,v 3 ,v 4 .OS [ ¯ 0,1,nil,nil]∗∗[|vl = (prio :: type :: cap :: z)|]∗∗
PV prio@ Tint32 7→ v 1 ∗∗PV type@Tint32 7→ v 2 ∗∗
PV cap@Tint32 7→ v 3 ∗∗PV z@Tint32 7→ v 4 ∗∗[|cnode_revoke_spec(vl)|]
def
revokepost =λˆv,∃v 1 ,v 2 ,v 3 ,v 4 . OS [ ¯ 0,1,nil,nil]∗∗PV prio@ Tint32 7→ v 1 ∗∗
PV type@Tint32 7→ v 2 ∗∗PV cap@Tint32 7→ v 3 ∗∗
PV z@Tint32 7→ v 4 ∗∗[|end ˆv|],
其中, OS [ ¯ 0,1,nil,nil] 表示当前没有中断发生, 中断使能标志为 1, 这表明 cnode_revoke 函数是由用户程序调用, 中
断可以随时发生. 参数 prio, type, cap 和局部变量 z 均为 int32 类型, 分别指向不同的值, 待执行的抽象规范为 cnode_
⌢
revoke_spec, 与底层函数调用具有同样的参数值列表; 底层函数调用结束后, 返回值为 v, 同时高层规范执行完毕,
返回同样的值.
值得一提的是, API 函数的验证与底层函数的验证相比, 会额外需要证明全局不变式在 API 函数调用后保持
成立. 在 cnode_revoke 的证明中, 以全局不变式 RLH_consistent 为例, RLH_consistent 用来描述底层数据和高层状
态之间的一致关系, 由于内核函数通过 reset_descendents_cspace_slot 对底层数据结构进行了递归撤销操作, 高层
抽象规范通过 reset_descendents_cspace_slot_abs 操作对高层抽象状态进行了递归撤销操作, 证明 RLH_consistent
经过递归撤销操作之后仍然成立是本文验证中一大难点.

4.4 其他函数的权能扩展和验证
系统中关于任务管理、通讯等模块的函数需要对权能进行检查, 具体的做法就是在函数的入口处增加权能权
限判断. 对于当前任务对应的权能槽判断是否有所需要的权能, 如果没有则立即结束调用, 如果有则进行下一步操
作, 这样可以确保系统调用的安全性和可靠性, 阻止未授权的访问. 验证的过程和权能 API 函数非常类似, 都分别
检查不同函数对应的权能. 因此, 这里不再进行详细展开.

5 验证代码规模、发现的问题与经验

本文所研究的航天嵌入式领域某微内核操作系统权能访问控制模块包括内核函数和 API 函数共计 17 个. 我
们对这些函数进行了形式建模和验证, 以下统计了各个函数的代码行数和在 Coq 中验证代码的行数. 从表 2 统计
可以看出, Coq 验证总代码行数大约为 35 000 行, 平均每一行 C 代码大约需要 50 行左右的 Coq 代码. 这需要在将
来进一步自动化验证工作中进行改进并精简证明. 我们分析造成这方面的原因, 主要是: 在不同权能函数的验证
中, 对权能数据结构进行频繁的展开, 尤其当某些操作, 例如 copy、move 等, 涉及当前任务、源任务和目标任务
三方的权能的访问和修改, 因此需要在同一时间, 对系统权能结构进行 3 次展开. 而当这 3 个任务需访问和修改的
权能 slot 下标的值不同时, 全局权能结构的展开更加复杂和庞大. 结束后, 也需要逐层逐个进行合并. 这都造成了
验证代码的冗长.