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

何韬 等: GhostFunc: 一种针对 Rust 操作系统内核的验证方法 3503

safe code module
unsafe code module
Ghost Arc Arc< T>
Arc<T>
data:*const T new(w) data:*const T
ref_count:*mut own(tid,value) ref_count:*mut
Atom ic Usize Atomic Usize
increase_ref_count
*mut decrease_ref_count *mut
… …
get_ref_count
get_ownership(tid) new(w)
get_ref_count clone(x)
increase_ref_count drop(e)
decrease_ref_count get_ref_count
图 2 GhostFunc 辅助验证流程

为了显式表达模块间的接口, 我们在 unsafe code module 定义的方法如下.
● get_ownership(tid): 获取特定线程的所有权.
● transfer_ownership(tid_src, tid_dst): 在源线程和目标线程之间转移所有权.
● get_ref_count(): 获取当前的引用计数.
● increase_ref_count(): 增加引用计数.
● decrease_ref_count(): 减少引用计数, 包含减少到 0, 即 drop().
下面具体介绍这些用于 GhostFunc 的接口函数在 Iris 中的形式化定义.
定义 10. GhostArc 形式化定义.

∀τ,ν.[[τ]].own(ν)−∗| ==> [[τ]].size ⇔ ∃l k,l 7→ (k,[[τ]].own)∗k 7→ [[τ]].size (1)

∀τ,ν.[[τ]].size−∗| ==> [[τ]].shr(ν) ⇔ ∃rc,rc 7→ [#1]∗[[τ]].inv(ν) (2)

∀τ, x.[[GhostArc(τ)]](get_re f_count(x))−∗| ==> [[τ]].size ⇔ ∃rc,rc = x.ref_count ∧rc 7→ 1∗[[τ]].shr(x) (3)

∀τ, x.[[GhostArc(τ)]](decrease_re f_count(x))−∗| ==> [[τ]].size ⇔ ∃rc,rc = x.ref_count ∧rc 7→ 1∗[[τ]].inv(x) (4)

∀τ, x,tid.[[GhostArc(τ)]](get_ownership(x,tid))−∗| ==> [[τ]].size ⇔ ∃rc l,rc = x.ref_count∧
l = x.data∧rc 7→ 1∗[[τ]].inv(tid) (5)

∀τ, x,tid_src,tid_dst.[[GhostArc(τ)]](transfer_ownership(x,tid_src,tid_dst))−∗| ==>
[[τ]].size ⇔ ∃rc l,rc = x.re f_count ∧l = x.data∧rc 7→ 1∗[[τ]].inv(tid_src) == ∗[[τ]].inv(tid_dst) (6)

∀τ, x.[[GhostArc(τ)]](clone(x))−∗| ==> [[τ]].size ⇔ ∃rc l,rc = x.ref_count ∧l = x.data∧rc 7→ 1∗[[τ]].inv(x) (7)

∀τ, x.[[GhostArc(τ)]](drop(x))−∗| ==> [[τ]].size ⇔ ∃rc l,rc = x.ref_count ∧l = x.data∧
rc 7→ 1∗[[τ]].inv(x) == ∗(rc 7→ 0 == ∗l 7→ _) (8)
在 GhostArc 中我们共定义了 6 个接口, 分别为获取引用计数, 增加引用计数, 减少引用计数, 转移所有权, 克
隆对象, 删除对象. 公式 (1) 和公式 (2) 描述了 own 所有权和 size 大小属性之间的关系以及 shr 共享属性和 size 之
间的关系. 公式 (3)–公式 (8) 中描述了一系列的 GhostArc 接口函数, −∗| ==> 表示在消耗拥有关系的前提下, 能够
推导出后置的状态; ==*是 Iris 框架中表示更新的逻辑操作符; ℓ 7→ (k,[[τ]])∗k 7→ [[τ]].size 表示 映射到 k 和所有
ℓ
权关系, 并且 k 映射到大小属性.
在 Rust 的 Arc 中, 实际是不存在转移所有权操作的, 在此处的转移所有权是一类辅助操作, 用于在内核中显
示的表达内核对象的转移和所在上下文的变化. 在第 4.1.1 节 Arc 的形式化中, 我们主要介绍了 Arc 相关方法的形
式化, 在 GhostFunc 中我们仍然实现了这些方法的接口, 但添加了有关获取所有权以及增减引用计数的接口, 这是
为了后续在与 safe 代码过程中, 能够更好地与内嵌该数据结构的对象的进行交互和组合.

4.2.2 GhostFunc 状态与不变式
为了保证验证的模块化, 除去全局的不变式性质, 我们在每个 GhostFunc 中都定义了局部的不变式, 主要是保