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

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

的 sharing predicate 不依赖于线程标识符, 那么类型 T 就是 Sync 的. 这确实符合直觉, 因为如果类型 T 的值 v 的所
有权与线程无关, 则在线程之间转移 v 的所有权是完全安全的. 基于这种方法, RustBelt 提供了对并发语义的支持.
然而, 该工作还存在很多局限. λRust 是 Rust 的子集, 没有包括 traits 等高级语言特性. 并且, λRust 建模的是顺序一
致性内存模型, 避免处理松散内存 (relaxed memory) 所带来的复杂问题, 而实际上某些库 (如 Arc) 采用 related-
memory 操作. 针对此问题, Dang 等人 [31] 对 RustBelt 进行了扩展, 加入了对 Rust 库广泛使用的弱内存模型的支持.
该研究针对弱内存模型下的内存回收问题, 提出了同步影子状态 (synchronized ghost state) 的结构, 并在实验中发
现了 Rust 的 Arc 库中的一个未知的数据竞争安全漏洞. 其次, λRust 是一个具有简化内存模型的小型 Lambda 演
算. 例如, 它有意避免了处理真实的 Rust 堆的挑战, 且操作语义与部分编译器优化不兼容. 此外, 虽然 RustBelt 具
有可扩展性, 用户可以验证自己的 unsafe API, 但是该框架不能直接自动化用于验证 Rust 源程序. 用户需要手工
将 Rust 源代码描述成 RustBelt 模型中的 λRust 形式的代码再使用该工作基于的 Iris 框架进行机械式证明, 学习门
槛高且过程耗时又容易出错. 后文将展开介绍缓解这两个问题的 RefinedRust 工作.
Matsushita 等人 [19] 基于 RustBelt 提出的语义类型 (semantic typing) 方式, 加入 RustHorn 风格的一阶逻辑
(FOL) 形式的规范, 定义了 RustHornBelt 类型系统, 并提供了经过机器检查的可靠性证明. 该研究通过一种叫做参
数化预言 (parametric prophecies) 的新分离逻辑机制开发了 RustHorn 风格的语义模型. 参数化预言的思路由
RustHorn 工具提出, 然而, RustHorn 的可靠性仅针对 Rust 的安全子集建立, RustHornBelt 将其扩展以支持封装
unsafe 代码的安全 API, 为其提供一阶逻辑 (FOL) 形式的规范. 此外, RustHornBelt 中不仅像 RustBelt 一样验证了
类型安全, 还考虑了功能正确性.
Gäher 等人 [15] 扩展了 RustBelt 语义模型并加入了精化所有权类型, 定义了 RefinedRust 类型系统, 并提供了经
过机器检查的可靠性证明. 该研究针对 RustBelt 在内存模型精确度和自动化验证方法方面的不足进行了改进. 一
方面, 该工作扩展了 λRust 的内存模型以描述更多 Rust 特性, 以支持验证包含 unsafe 代码的真实 Rust 程序.
λRust 使用简化内存模型以便于形式化验证以及专注于 Rust 所有权和借用规则的核心特性. 然而这种简化可能会
忽略一些 Rust 语言的底层细节和优化. 例如, 在 λRust 中, 抽象地将所有整数看作无界整数, 整数只有一种类型,
并只占用一个内存位置 (memory cell). 而实际上 Rust 提供 12 种不同的原始机器整数类型, 这些类型在内存中占
用 1–16 个字节. 此外, Rust 编译器会做一些优化, 如利基优化 (Niche optimization) 在不影响表达力的情况下改变
某结构体中不同字段的布局顺序, 以减小结构体的总体大小. 而在 λRust 的内存模型中, 结构体具有固定的布局,
并且忽略了对齐, 因此结构体的字段之间不需要做填充. 针对此类问题, RefinedRust 参考 RefinedC [32] 中对 C 操作
语义的描述, 并真实而细粒度地建模了 RustMIR 的操作语义 Radium. Radium 中定义了数据类型在内存中的排列
方式, 包括其大小和对齐要求, 并详细定义了加载 (loads) 和存储 (stores) 操作受到内存访问布局的影响, 以支持底
层原始指针操作等. 如此, 相比 λRust, Radium 中定义的整数是有界的, i32 类型的整数占用 4 个字节. 然而, Radium
中也有很多 Rust 语义没有包含, 如递归类型, trait, closure 等. 另一方面, 该研究基于 RefinedRust 类型系统中定义
的规则实现了一套工具链, 能够半自动化地对包含安全和 unsafe 代码的 Rust 程序进行功能正确性验证. 具体来
说, 在验证过程中, 带有注释的 Rust 程序被转换成 Coq 中浅嵌入 (shadow embedding) 的 Radium 语言描述的程序,
并基于分离逻辑证明该程序符合 RefinedRust 类型系统定义的规则. 该工作是首个在有正确性保证下验证包含
safe 和 unsafe Rust 程序的工作. 实验中通过验证 Rust 标准库 Vec 实现的一个变体, 表明 RefinedRust 可以完成复
杂的推理, 验证包含不安全指针操作的 Rust 程序.

3.3 基于纯操作语义的 Rust 语义研究

除了依赖于类型系统的方法, 还有一些研究专注于基于 Rust 的操作语义来构建形式规范, 这些基于操作语义
的方法不涉及类型推导的规则定义, 而是将所有权和借用检查作为内存访问控制的核心部分, 以前提条件的形式
嵌入在了内存访问操作语义的语义规则中. 操作语义方法的特点是直接对程序的执行行为和内存等状态的变化进
行建模. 其中, 状态为程序执行期间任一时刻观察到的变量取值, 迁移关系规定如何从一个状态迁移到下一个状
态, 一般定义为一组迁移规则, 每条迁移规则对应一条程序语句. 研究者通过证明模型满足一系列不变式 (invariants)