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

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

隆操作的前置条件. post_clone s s' 是克隆操作的后置条件. own γ(· (Excl' s')) 表示当前线程拥有的全局状态. inv
γ(valid_ref_count s' ∗valid_ownership s' ∗valid_locked s') 表示全局状态的不变式.

4.3 safe 代码段形式化
除去在第 4.1 节已经完成的, 还有 safe 代码段需要形式化. 本文不同于 CertiKOS 的分层验证思路, 而是采用
逐步建模形式化的方式, 主要在于 Rust 的正常 safe 代码块已经满足了内存的安全性, 从验证的角度出发, 我们无
需额外考虑内存安全的形式化验证, 只需考虑代码逻辑方面的正确性. 从而简化了验证的过程. 在本节中, 我们一
共建模 277 行 Rust 代码. 涉及 Definition、RA 以及 proof 的 Iris 代码共 1 900 余行. 在本节我们简要介绍某内核的
任务管理和调度模块并简要介绍模块建模以及其与 GhostFunc 的接口的形式化叙述.

4.3.1 数据结构的建模验证
在任务管理与调度模块中, 参与验证的数据结构为全局的线程集合, 某内核在任务管理中维护这个对象:
THREAD_DEQUE: Lazy<Mutex<VecDeque<Option<Arc<Thread>>>>>, 其中 Arc: 进程引用计数, 一个线程可能
在 THREAD_DEQUE 或者所属进程的线程队列中有多份引用, VecDeque: 线程队列, 可以在队列两端执行插
入、删除操作. 在当前内核版本中的调试运行中, 线程队列暂时没有双端操作, 功能与普通队列相同. 结构如图 3
所示.

… Arc<Thread> Arc<Thread> Arc<Thread> …
Mutex<Thread Queue>

图 3 全局线程队列

在验证数据结构时, 首先需要验证数据结构整体的正确性, 所以需要对数据结构做简化, 我们此处将队列中
的 Arc<Thread> 简化为 Lock<Thread, Key>, 将队列中 Mutex<Thread> 简化为 Lock<Thread Queue, Key>, 表示将
Mutex 和 Arc 都简化为锁 Lock, 但访问受保护的内容时, 需要提供凭证 Key, 这样可达到数据结构的基本功能, 而
Arc 和 Mutex 本身的验证, 我们会在 GhostFunc 中完成. 基于此, 我们在 Coq 中对该结构进行建模与验证.
关于 lock 的建模, 主要涉及 3 个操作, 分别是获取锁, 释放锁和新建锁, 并为锁定义了两个状态分别为 is_lock
和 locked, 这些建模不详细解释, 方法比较传统. 下面介绍我们定义的不变式.
定义 11. 全局队列不变式.

lock_inv(γ,ι,κ,arr,c,ap,nextPtr,R) = ∃(o,i : nat)(xs : list bool) ,

lengthxs = cap




 ∧nextPtr 7→ #(o+i)





 ∧ is_array(arr, xs)







∧ invitation(ι,i,cap)

 ,

 ∧ own(γ,?(Excl o,GS et(set_seqoi)))
′





  ◦ ′
 (own(γ, (Excl o,GS et(∅)))∧R∧both(κ)∧ xs = list_with_one(cap,(o mod cap)))

 
 
 
 

∧  ∨(issued(γ,o)∧right(κ)∧ xs = replicate(cap, false))

 
 
 
 
∨(issued(γ,o)∧le ft(κ)∧ xs = list_with_one(cap,(o mod cap)))

其中, o 和 i 是自然数, 分别表示当前锁持有者的位置和等待队列中的线程数. xs 是一个布尔列表, 表示锁的状态数
组. arr 是锁状态队列的位置. nextPtr 是指向下一个 key 的位置. cap 是锁的容量, 即锁状态数组的大小. R 是临界
区资源. 第 1 个算子表示锁的状态数组 xs 的长度必须等于锁的容量 cap, 第 2 个算子表示 nextPtr 存储当前 key,
即等待队列的长度, 第 3 个算子表示锁的状态数组存储在位置 arr, 并且当前状态为 xs. 第 4 个算子表示当前锁持
有的 key 数量为 i, 总容量为 cap. 第 5 个算子表示锁的拥有者是 o, 当前的队列范围是 [o, o + i), 通过 auth 机制确