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

张卓若 等: 面向 Rust 语言的形式化验证方法研究综述 3615

1 struct Obj(u32);
2 letrgn<'y, 'z> { // 'y -> {}, 'z -> {}
3 let mut x = Obj(5); // x : Obj
4 let y = &'y uniq x /* 'y -> { uniq x } */;
5 let z = &'z uniq *y /* 'z -> { uniq x , uniq * y } */;
图 9 Oxide 代码例子

Lehmann 等人 [21] 基于“液态类型 (liquid type)”方法提出 Flux, 通过引入用于函数式验证的精化类型扩展 Rust
的类型系统. 液态类型的方法将类型构造器与简单的无量词逻辑谓词组合来表达复杂不变式, 以简化程序验证. 精
化类型中可以加入额外的逻辑约束, 表达关于值的更多信息. 例如, 一个整型变量除了 int 类型, 还可能被进一步细
化为 int≥0 来表示它总是非负的. 然而, 命令式语言 (imperative language) 中别名的问题使得很难追踪变量类型的
改变, 因此已有的精化类型研究主要针对函数式语言 (functional language). Flux 将逻辑精化与 Rust 的所有权机制
相结合, 实现命令式 (安全) Rust 的验证. 为了处理对可变引用的写操作, Flux 引入了“强引用”的概念, 允许引用的
类型发生变化 (即允许类型强更新), 并跟踪确切的引用位置. Flux 基于 Stacked Borrows 提出的别名规则 (aliasing
discipline) 描述其操作语义, 并证明了其类型系统的可靠性, 确保“良好借用的良类型程序 (合法程序) 的评估不会
陷入僵局”. 基于 Flux 的类型系统规则构建了一个轻量级且高度自动化的验证工具, 实现为 Rust 编译器插件, 在编
译器做检查后分析程序, 自动合成精化类型, 循环不变式和霍尔逻辑约束, 最终基于不动点的方式求解约束, 定位
出错位置. 为展示精化类型相对于程序逻辑的优势, 实验对比了该工具和基于程序逻辑的验证器 Prusti 的验证效
率, 表明在轻量且普遍存在的验证用例上, 如在使用向量的程序中检测索引溢出错误时, Flux 的液态类型将规范行
数减少一半从而将验证时间减少一个数量级, 且能够自动合成循环不变式注释, 减少了人工标注的负担. 然而,
Flux 通过将类型构造器与简单的无量词逻辑谓词组合来表达不变式, 相比之下, Prusti 等基于程序逻辑的方法的
有更丰富的表现力, 可以验证深层功能正确性规范. 此外, Flux 同样针对的是安全代码的验证, 不能推理关于低级
指针操作等问题.

3.2.2 针对包含 unsafe Rust 的语义研究
为了证明包含 unsafe Rust 的安全 Rust 标准库 API 是否提供了安全抽象, Jung 等人 [13] 采用了米尔纳 (Milner)
风格的语义方法描述 Rust 类型系统, 允许在使用不安全特性的情况下也可以做类型推导. 即用丰富的程序逻辑将
某个类型解释为分离逻辑中的一个命题, 所有符合这个命题的值都可以有这个类型, 将类型判断 (typing judgment)
解释为这些谓词之间的逻辑蕴涵. 这种方法不同于语法上基于类型规则的类型定义. 基于这种方法证明语义类型
的可靠性, 即语义类型良好的程序是内存安全和线程安全的, 所有执行的指针访问都是有效的, 并且不存在数据竞
争, 可以安全执行. 语义类型良好限定为需要遵守的验证条件, 即证明只要某个库中的 unsafe 代码符合某些限制条
件, 就是做了安全的封装. 该研究采用高阶并发分离框架 Iris [29,30] 机械化建模了形式语义模型 RustBelt, 并用它以机
器检查的方式验证了大量使用 unsafe 代码的 Rust 标准库抽象的外在安全性. 即, 证明某内部包含 unsafe 代码的库
满足模型中定义的该接口的验证条件. 该研究验证了几个使用 unsafe 代码的常用 Rust 标准库, 包括: Arc、Rc、
Cell、RefCell、Mutex、RwLock 等. RustBelt 语义模型中描述了 Rust 的核心子集 λRust, 包含所有权和生命周期
等基本语法特性. 其中一大亮点是基于 Iris 提出了生命周期逻辑 (lifetime logic), 模仿了 Rust 借用检查机制.
RustBelt 借助给出或收回生命周期令牌 (lifetime token) 的方式表示赋予或收回对某数据结构的暂时性访问权限.
在每次借用语句时该模型通过生命周期逻辑的推理规则检查借用的有效性, 即确保在使用某引用时, 它拥有表示
其生命周期是活跃的 lifetime token. 此外, 在 RustBelt 中详细描述了线程安全的概念. 在 RustBelt 模型中, 所有权
谓词 (ownership predicate) 表示拥有一个 T 类型的值, 共享谓词 (sharing predicate) 表示拥有一个&T 类型的值. 为
了捕捉线程安全的语义, 这两个谓词都引入了一个额外的参数, 该参数与线程标识符 (thread identifier) 相关联. 通
过该线程标识符对应的参数, 类型系统能够建立类型与声明所有权线程之间的依赖关系. 在 Rust 中, Send 表示类
型 T 是线程安全的, Sync 表示类型&T 是线程安全的. 而上述方法提供了一种直观的方式来描述 Send 和 Sync 的
特性: 在语义层面, 如果类型 T 的 ownership predicate 不依赖于线程标识符, 那么类型 T 就是 Send 的; 如果类型 T