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

3614 软件学报 2025 年第 36 卷第 8 期

不符合 Rust 基于所有权和借用检查的强大类型系统中所定义的语法良好性. 在现实世界的应用中, 许多广泛使用
的 Rust 标准库 API 内部都包含 unsafe 代码来扩展表达能力, 如何确保该 API 在观察上是安全的 (observationally
safe) 是一个重要问题. 观察上安全意味着即使在存在 unsafe 代码的情况下, API 对外的表现仍然是符合 Rust 安全
原则, 不会对调用者造成不可预测的影响. 针对此问题, 现有研究工作提出了语义类型可靠性 (semantic type soundness)
的概念, 即证明语义类型良好的程序是内存安全和线程安全的, 可以安全执行. 本节将依次探讨这两种证明方法,
并展开相关研究工作.

3.2.1 针对纯 safe Rust 的语义研究
比较早期的形式化语义建模工作包括 Patina [23] , 旨在为 Rust 早期版本 (1.0 之前) 提供内存安全证明. Patina 描
述了 Rust 早期借用检查器的操作语义, 并基于该操作语义, 给出了该语言子集的可靠性证明. 然而, 早期 Rust 语
言设计不够稳定, 因此 Patina 的模型中缺少很多 Rust 关键特性, 如借用检查过程中缺少生命周期推理, 因此该模
型在现阶段的可参考性有限.
Payet 等人 [22] 参考 Featherweight Java [28] 提出 Featherweight Rust 轻量演算 (lightweight calculus) FR, 描述了

Rust 复制、移动、借用和生命周期特性. FR 仅限于小的 Rust 子集, 如涉及语句表达式仅包括 let 绑定、赋值、移
动、部分移动和借用, 没有考虑控制流、类型转换、函数可变性、通用函数调用语法等. 该演算采用了流敏感的
类型系统来编码类型和借用检查的规则, 并证明类型系统的语法可靠性, 即类型和借用安全的程序不会陷入僵局
(get stuck), 并保持借用不变式, 确保类型和借用安全的程序不会尝试解引用悬挂指针. 文中探索了对 FR 演算的几
个扩展, 如对控制流、元组、方法调用等更复杂特性的支持, 但没有证明扩展后类型系统的可靠性. 该研究基于
FR 形式化系统定义的规则实现了一个工具, 对程序进行类型检查和借用检查. 该工具解析 Rust 源代码为抽象语
法树 (AST), 遍历树形结构为每个节点分配类型并确保程序中的所有类型操作都是合法的, 最后进行借用检查, 确
保程序遵循 Rust 的借用规则. 实验中还对 Rust 编译器进行了模糊测试, 基于 FR 定义的规则生成符合或不符合类
型和借用安全的程序, 比对编译器的判断结果, 发现了一个确认的编译器错误.
同样参考 Featherweight Java, Weiss 等人 [20] 提出了 Oxide, 在类型系统层面对 Rust 的借用检查规则进行了精
确的描述. 相比于 Featherweight Rust, Oxide 覆盖大量 Rust 子集. 此外, 不同于 FR 使用的结构化生命周期, Oxide
提出了一种类似于原型借用检查器 Polonius 中的生命周期视角, 即, 将生命周期视为一系列称为区域 (region) 的
位置集合, 这些 region 能够近似地表示引用的起源 (origin), Oxide 借用检查器利用这些关于引用的起源信息来决
定在程序的特定位置创建或使用引用是否安全, 实现对引用的精确跟踪和管理. Oxide 中对每个借用表达式都自
动注释了与其绑定的 region, 并定义相应的类型规则基于该注释信息进行推导, 从而实现一种基于区域的别名管
理系统. 具体来说, region (表示为'a、'b 等) 可以被视为一系列借用 (loan) 的集合, 这些借用集合共同构成了对引
用起源 (origins) 的静态近似. 这样, 我们可以将 region 理解为内存中不同对象的静态分组. 当我们将引用与特定
的 region 关联时, 我们实际上是在指明该引用可能指向的内存对象必须来自于与该 region 相关联的 loan 集合.
Oxide 语言的设计接近于 Rust 的源代码级别, 但增加了类型注释. 如图 9 的简单 Oxide 代码为例. 该例中定义了
一个包含 u32 类型字段的结构体 Obj, x 是该类型的可变实例, y 是对 x 的引用, z 是重借用. 注释内容展现了类型
检查过程中内部元数据的更新. 在类型检查时, 第 2 行通过特定语法 letrgn 引入了两个新的 regions 'y 和 'z, 各自关
联一个空的 loan 集合. 第 4 行创建对 x 的一个唯一引用 (unique reference) y 后, 这次借用操作产生元数据 'y→
uniq x }, 它将 uniq x 的 集合相关联. 这表明, 任何带有 region 'y 标识的引用都必须指向
{ region 'y 与包含 loan x. 其中,
uniq 表示这是唯一引用 (即可变引用), 和共享引用 shrd 区分开. 第 5 行从 y 重新借用得到 z 后, 这次操作将区域'z
uniq uniq ∗y 的 uniq ∗y 表示从 y 的重新借用. 这包含两个关键信息: 首先, 带有 region 'z 标识
与包含 x 和 loan 集合相关联.
的引用指向 x; 其次, 带有 region 'z 标识的引用是通过从 y 重新借用而创建的. 后者意味着, 只要引用 z 存在, y 就应
该被视为不可用, 以确保引用的合法使用. 该研究利用了基于语法的方式证明了 Oxide 的类型安全性. 此外, 该研
究实现了一个从 Rust 到 Oxide 语言的编译器以及一个原型类型检查器, 实验评估了 Oxide 类型检查器结果与
rustc 借用检查器在 Rust 官方非词法生命周期测试套件上的一致性.