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

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

本文对于 arch64 中的有关硬件的 unsafe 操作, 没有进行形式化建模, 所以本节的建模主要是针对标准库中的
unsafe 操作. 下面以涉及代码量较多 Arc 和 Mutex 为例, 对 unsafe 代码的形式化过程详细地介绍, 主要针对其具体
功能以及涉及的如生命周期等属性进行建模和不变式的定义.

4.1.1 alloc::sync::Arc
Arc<T> 类型提供了在堆中分配的 T 类型值的共享所有权, 在 Arc 中调用 clone 方法会生成新的实例, 实例指
向堆上源 Arc 所指处, 并增加引用计数. 在某内核中, Arc 的使用非常频繁, 主要是用于进线程以及权能相关的管
理. Arc 的核心机制是引用计数, 它通过原子计数器来跟踪对象有多少个活跃的引用. 下面为 Arc 的 3 个基本定义.
定义 4. Arc 的基本属性定义.

Definition [[Arc(τ)]].size := [[τ]].size+2.
Definition [[Arc(τ)]].own(tid,vl) :=
∃rc l, vl = [#l] ∗
l 7→ 1(rc, [[τ]].own tid) ∗
rc 7→ {1}#1 ∗
□(rc 7→ {1}#1 ⇒ [[τ]].inv tid l).
Definition Arc(τ).shr(κ, tid, l) := ∃rc, rc 7→ κ#1 ∗ [[τ]].shr κ tid l.
这 3 个定义分别是 size、所有权 own 和共享属性, 在不考虑 DST 的情况下, 在类型系统中 [[τ]] 和 own(τ) 在
[[τ]] 的 λ Rust 中的类型如布尔类型, 整形类型, 和类型, 积类
语义上被归为同一类, 所以 size 属性与 own(τ) 相等, 在
型等的 size 属性都为 1, 大于 1 的为复合或嵌套类型, 例如 Arc 需要有引用计数, 在类型上可视为 lock 大类中的需
要额外属性的类型, 所以在其 size 基础上加 2.
接下来介绍 Arc 的包含的 3 种方法的形式化定义: 分别是新建 new(), 克隆 clone(), 删除 drop() .
定义 5. Arc 包含的方法形式化定义.

{[[τ]].own( ¯w)} let x = Arc :: new( ¯w) := fn(τ) → Arc(τ)
{[[Arc τ]].own([x])} let y = x.clone() := fn(&α Arc(τ)) → Arc(τ)
{[[Arc τ]].own([¯e])} let y = x.drop(¯e) := fn(Arc(τ)) → (),
其中, () 表示空, & 表示获取原 Arc 指针的复制. 这 3 个方法对应的后置结果形式如下:

∃ℓ.x = [ℓ]∗ℓ 7→ [1]++ ¯w∗ shared_own(int,ℓ, ¯w,1,1)
[[Arc τ]].own([x])∗[[Arc τ]].own([y])
[[Arc τ]].().
new 对 ℓ 地址处添加了一个拥有共享所有权的变量, 对应于 Arc 的在 Rust 中的含义, clone 将共享所有权拆分
为了两个, 为了简化模型, 没有采用 λ Rust 中的所有权的 token 形式.
除了定义和操作的形式化, 我们还需要为 Arc 定义不变式, 首先我们分析 Arc 在内核中所需保持的不变性质,
Arc 在内核中主要是用于维护全局的线程队列, 所以第 1 个不变性质就是队列的在内存中的位置 ℓ 需要保持, 第 2
是引用的计数正确, 第 3 是正确的销毁. 基于此我们可以定义出 Arc 的不变式 Arc_inv.
定义 6. Arc 不变式定义.

Arc_inv (κ ,ℓ,t) := ℓ 7→ true∨ℓ 7→ false∗κ (∃¯v.(ℓ +1) 7→ ¯v∗[[τ]].own(t, ¯v))∨ℓ 7→ false∗t 7→ (),
′
′
τ
full
其中, κ 用于表示生命周期的快照, t 为线程集合, 第 2 个不变式状态表示若 Arc 处于空闲状态, 可以使其储存的下
′
一个位置储存值对应于当前的线程, 使其获得该复制位置的所有权.

4.1.2 alloc::sync::Mutex
Mutex 为标准库中的互斥锁. 互斥锁阻止等待锁可用的线程. 互斥锁可以通过 new 构造函数创建. 每个互斥锁
都有一个类型参数, 表示它正在保护的数据. 只能通过从 lock 和 try_lock 返回的 RAII 保护来访问数据, 这保证了
只有在互斥锁被锁定时才可以访问数据. 在 Arc 中我们没有详细介绍 Rust 中锁的机制, 在这里将进行介绍. 锁保
护的内容的所有权应当拥有一个完整的借用, 若没有获取到完整的借用, 那他的外层也就是锁本身应当包含这个