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

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


                 基石.
                    内核安全是操作系统安全的核心部分, 因为内核负责管理系统的所有关键操作, 包括内存管理、进程调度、
                 硬件交互等. 强化内核安全性可以有效防止恶意软件和攻击者获取核心权限, 从而控制整个系统.
                    当前, Rust 是一种以内存安全和线程安全为核心设计原则的编程语言. 它通过所有权机制、借用检查和生命
                 周期管理来防止常见的内存错误, 如空指针引用和数据竞争. 这使得                     Rust 在系统级编程中尤其受欢迎, 因为它能
                 够在编译时捕获许多潜在的错误, 从而减少运行时崩溃和漏洞的可能性. 然而, Rust 中也存在一个名为                             unsafe 的
                 关键字, 它允许开发者绕过编译器的安全检查, 以进行一些低级操作, 如直接操作内存指针. 虽然                            unsafe 代码块在
                 某些情况下是必要的, 但它也引入了潜在的风险. 如果使用不当, unsafe 代码块可能导致内存泄漏, 数据竞争和其
                 他安全漏洞. 因此, 对     unsafe 代码进行形式化验证是确保其安全性的重要手段. 这种验证可以帮助确认                       unsafe 块
                 在特定条件下是安全的, 从而增强整个系统的安全性和可靠性.
                    目前, 许多院校机构都在尝试将          Rust 语言应用于操作系统内核的开发中, 形式化方法               [1] 作为确保系统安全性
                 和可靠性的有力手段, 广泛应用于操作系统内核的安全性检验中, 但针对                      Rust 构建的操作系统内核的验证工作仍
                 然缺乏, 针对   Rust 特点的内核验证方法也处于探索阶段.
                    某内核是国产自主开发的          Rust 内核, 采用平衡于用户态服务模式和内核态函数模式之间的内核态服务模式,
                 在性能和可靠性上进行折衷, 利用           Rust 的内存安全特性产生的原生的安全隔离, 异步并发等减少性能的损失. 可
                 信的应用可以在用户态独占资源, 较大提高性能的释放.
                    本文以某内核作为验证目标, 提出了            GhostFunc 的  safe 代码块和  unsafe 代码块组合验证思路, 后者的验证基

                 于  λ Rust  进行接口的构建与拓展. 所有工作在      Coq  定理证明器中以     Iris 并发分离逻辑框架呈现. 论文主要工作和创
                 新如下.
                    (1) 提出了  GhostFunc 的  Rust 系统组合验证思路.
                    (2) 针对操作系统内核的验证拓展了          λ Rust  语义模型.
                    (3) 对  Rust 构建的内核的形式化模型提供了实例.
                    本文第   1  节主要介绍操作系统内核验证、Rust 形式化验证等的相关工作. 第                   2  节介绍  Coq  交互式定理证明
                 器, Iris 分离逻辑框架和   λ Rust  语义模型, 并简要介绍某内核的设计结构. 第         3  节介绍  unsafe 代码块语法和语义模型
                 与建模. 第  4  节讨论  GhostFunc 的构建与形式化. 第    5  节介绍  safe 代码块的形式化以及整体的验证方案与流程.

                 1   相关工作

                    当前国内外针对操作系统内核的验证工作有很多, 主要分为模型层面的验证和代码层面的验证. 下面对这些
                 工作进行介绍.
                    Liang  等人  [2] 提出将  Rely-Guarantee 方法应用于验证并发程序变换, 这一方法有效地处理了并发程序中的复
                 杂性. 随后, Xu  等人  [3] 进一步提出了一个具有多级中断的抢占式操作系统内核的实用验证框架, 并成功将其应用
                 于  μC/OS-II 嵌入式操作系统的验证工作. 这一验证框架通过形式化的方法确保了操作系统内核在处理多级中断
                 时的正确性和可靠性. 乔磊等人         [4] 组成的  SpaceOS  验证团队针对  SpaceOS  嵌入式实时操作系统     [5] 进行了一系列验
                 证工作. 他们使用     Event-B  抽象方案对内存管理模块进行了详细的验证工作. Klein             等人  [6,7] 对  seL4  内核的验证工
                 作主要确认了内核的实现与其形式化规格完全一致. 这一验证覆盖了内核的所有功能, 包括线程调度、内存管理
                 和进程通信等. 通过使用定理证明器           Isabelle/HOL, 他们成功地证明了    seL4  内核在各个方面的正确性, 这一工作被
                 认为是操作系统内核验证领域的一项具有代表性的成果. Andronick                 等人  [8] 对实时操作系统   eChronos 进行了验证,
                 特别关注在多程序复杂并发以及多级嵌套中断场景下的内核调度性质. 他们在                          Isabelle/HOL  中对内核的同步和异
                 步中断机制以及上下文切换调度栈进行了详细的建模, 并通过证明调度栈在运行过程中保持一些基本属性, 如线
                 程调度栈的最底层保存的一定是当前线程等, 得出调度属性在内核全局都保持的结论. 这一验证确保了任何时刻
                 运行的程序都是优先级最高的程序. Singularity         项目  [9] 是由  Microsoft Research  发起的, 旨在开发一种高可靠性的
   67   68   69   70   71   72   73   74   75   76   77