Page 74 - 《软件学报》2025年第8期
P. 74

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



                 Definition incr(ℓ : loc) : expr := #ℓ <– !#ℓ + #1.
                 Definition incr_inv(ℓ : loc) (n : Z) : iProp := ( ∃ (m : Z), ⌜(n ≤ m)%Z⌝ ∗ ℓ  7→ #m)%I.
                 Lemma parallel_incr_spec(ℓ : loc) (n : Z):
                   {{{ ℓ  7→ #n }}} (incr ℓ) ||| (incr ℓ) ;; !#ℓ {{{m, RET #m; ⌜(n ≤ m)%Z⌝ }}}.
                    不变量的主体定义为        counter_inv. 这里使用  %I 告诉  Coq  将逻辑公式解析为    Iris 断言, 这意味着它将把连接
                 词解释为   Iris 连接词. 使用#来将   Coq  命题如变量, 数字等嵌入到       Iris. 在此示例中, 将“≤”作为   Iris 断言. 简单来说,
                 这种嵌入意味着嵌入的断言要么适用于所有资源, 要么不适用. ⌜…⌝ 用于将                      Coq  断言嵌入到    Iris 断言. 现在定义
                 简单并行加法器的证明过程.
                 iIntros(Φ) “Hpt HΦ”.
                 iMod(inv_alloc N _ (incr_inv ℓ n) with “[Hpt]”) as “#HInv”.
                    这段代码第     1  行介绍了证明中使用的假设和后续要证明的结论. Φ               是后续要证明的结论, Hpt 是前置条件. 第
                 2  行建立了一个名为     N  的不变量, 保护位置ℓ 的内容. 这是为了确保在并发环境中, 不同线程看到的ℓ 的状态是一
                 致的. 后续证明都是使用类似的         Iris 证明策略.

                 2.3   λ Rust
                     λ Rust  是一种基于  Iris 逻辑框架开发的  Rust 形式化语义模型    [22] , 专门用于验证  Rust 程序的内存安全性和并发

                 正确性. 通过利用     Iris 的分离逻辑和幽灵状态机制,       λ Rust  能够精确表达和推理   Rust 的所有权和借用规则, 确保在多
                 线程环境下的内存安全和数据竞争防护, 从而在理论上严格验证                     Rust 程序的正确性和可靠性.
                      λ Rust  中, 资源模型用于描述程序的状态和资源, 如内存单元、锁、信号量等. 资源模型允许对这些资源进行
                    在
                 形式化描述和验证, 确保在并发环境下的正确性和安全性. 幽灵状态是一种在逻辑中引入额外状态的机制, 帮助进
                 行形式化验证. 幽灵状态不影响程序的实际运行, 但在验证过程中用于推理和证明.

                 3   unsafe 代码语法和语义模型

                    Rust 中  unsafe 代码绕过了内存安全保证的检查, 对于         unsafe 代码的验证, 我们在验证时, 实现层接近于          MIR,
                 在语义模型的建立时, 本文参考了          λ Rust  的语法和语义模型定义, 在语法的定义上, 采用         EBNF, 包含基本语法元素如
                 变量声明, 函数定义, 控制结构, 数据结构等, 特别强调所有权和借用规则. 其类型系统包括基本类型                          (如  bool、int)、
                 复合类型   (如数组、切片)、泛型、生命周期标注. 我们在其基础上, 拓展了与操作系统内核相关的一系列语法和语义.

                 3.1   语 法
                    在语法的定义中, 对      Rust 一些语法糖进行了去糖, 所以在基础语法方面更接近于                 MIR, 但又对内核中一些常
                 见且容易证明正确的行为包装成语法糖, 这样可以较大程度上简化我们验证的过程, 例如上下文切换等操作, 被我

                 们作为了语法的一部分. 针对此          λ Rust  语法定义做了拓展和修改, 我们定义了        7  种表达式类型: 上下文, 调用链, 变
                 量, 路径, 操作符, 函数体以及中断.
                    定义  1. 内核验证语法定义.

                     C ::= k|u|runtext() ∈ Context

                     c ::= from|to|Path|call() ∈ Chain

                     v ::= false|true|z|funrec f(x) ret k := F|PID|Device ∈ Val

                     p ::= x|p.n|context.k ∈ Path

                     I ::= v|p|p 1 + p 2 |p 1 − p 2 |p 1 == p 2 |syscall()|new()|delete|∗ p|p 1 := p 2 |p 1 := n∗ p 2 |newP(PID)|killP(PID)| ∈ Instr

                     F ::= let x = I in F|if k then F 1 else F 2 |newlft F|endlft F|case∗ p of ¯ F| jump()|call f(x) ret p ∈ Func
                     H ::= handleInterrupt(type) do F ∈ Handle_irq,
   69   70   71   72   73   74   75   76   77   78   79