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

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

Chen 等人 [62] 使用 Rust 开发了类 L4 的微内核 Atmosphere, 并基于 Verus 进行验证. 该工作首先定义了高层规
约描述 Atmosphere 接口的行为, 再证明系统调用的实现是高层规约的精化. 他们还改造了 Verus: 不再使用未经验
证的通用内存分配器, 而是基于自己实现的验证安全的简单内存分配器; 设计了一个过程宏以支持高效的域可变
借用. 证明代码与原始代码比率为 7.5:1, 低于之前的方法.
Ijaz 等人 [63] 提出了语内设计 (intralingual design) 的概念, 即利用 Rust 的类型系统, 在编译期保证部分不变式,
从而减少需要交给约束求解器的验证条件. 这可以用来保证系统资源管理的正确性, 即用一种类型 (不实现 copy
特征, 字段私有) 表示一种系统资源, Rust 的类型规则就可以适配到该系统资源: 使用 Rust 类型状态 (typestate) 特
性实现访问控制, 通过所有权转移或者借用实现资源委托, 系统资源自动回收; 也可以用来表明一个操作是否完
成: 让执行操作的函数返回一个特定类型的实例 (但是需要确保只有该函数会实例化这种类型), 如果要保证一个
操作序列, 可以让下一个函数的参数包含该特定类型, 消费掉这个实例. 但是语内设计的表达能力有限, 如不能证
明算术属性. 另外, 尽管 Rust 的类型系统保证一种类型的不同实例 (内存对象) 是不相交的, 但不能保证这些实例
对应的系统资源也是不相交的. 他们将该设计应用到开源 Rust 操作系统 Theseus 的内存子系统, 并且对页框分配
[1]
器使用 prusti 验证其返回的页不会重叠. 由于约束求解器只需要对页框分配器返回页框的唯一性进行判定, 所以
最终的证明代码与原始代码比率为 1:76, 非常轻量化.
文件系统最重要的属性之一是在崩溃或断电时保持其完整性和用户数据, 构建崩溃一致性文件系统是一件很
有挑战性的任务. SquirrelFS 文件系统 [64] 引入了一种新的崩溃一致性机制–同步软更新 (synchronous soft updates),
将崩溃安全归结为对文件系统元数据的更新之间的强制排序. 在 SquirrelFS 中, Rust 语言的类型状态 (typestate) 特
性被用来实现这一排序. 每个持久性结构都有其对应的类型状态, 这些类型状态定义了结构可能处于的一系列状
态, 并且通过 Rust 的类型系统来保证文件系统操作按照正确的顺序执行. 这种方法不仅提高了代码的可读性和可
维护性, 而且通过编译时检查减少了运行时错误的可能性. 此外, SquirrelFS 的开发团队还使用了 Alloy 建模语言
来对文件系统设计进行建模, 并保持 Rust 中的类型状态模型与 Alloy 模型在设计上的一致性; 通过在 Alloy 中运
用模型检查的方法, 验证了通过类型状态强制的操作顺序确实能够满足崩溃一致性的要求.
HyperEnclave [65] 是基于高特权软件 (hypervisor) 的可信执行环境, 通过模拟 TEE 指令集兼容已有 TEE 生态
(如 SGX), 并且已经在蚂蚁集团得到部署. Dai 等人 [66] 设计了一个模块化验证框架 MIRVerif, 验证 HyperEnclave
的内存隔离机制实现的正确性. MIRVerif 可根据 Rust MIR 的轻量级语义验证 Rust 系统代码. 他们修改了 Rust 编
译器, 将改造过的 HyperEnclave 内存管理模块代码转译进而嵌入到 Coq, 得到实现层的规约, 沿用 CertiKOS 和
SeKVM 使用的 CCAL 方法, 基于函数调用图将涉及的函数分为 15 层, 并且增加了对不同层之间指针参数传递的
支持, 逐层求精, 最终证明实现层精化抽象层. 在抽象层上定义了系统状态迁移的操作 (内存读写和 hypercall), 证
明了页表映射满足的不变式, 进而证明了系统的无干扰性. 该工作首次用形式化方法对一个工业界实际部署的
Rust 系统进行功能正确性验证. 但他们对于架构相关代码以及第三方库的代码选择相信其正确性并不加以验证,
另外, 他们对 RustMIR 的语义形式化依靠人工阅读文档校验.
AMD SEV-SNP [67] 机密虚拟机架构可以创建虚拟机级别的可信执行环境, 其中, 运行在高虚拟机特权级别
(VMPL) 的安全模块可为客户机提供远程认证、完整性保护、中断注入监控等关键安全功能. VERISMO [68] 是第
一个功能正确性、信息流安全性经形式化验证的安全模块, 基于 Verus 完成了验证过程. 该工作将证明分为两层.
机器模型层定义了抽象机器模型 ψ, 其中包含如寄存器、内存、页表与 RMP 等硬件资源, 定义了 hypervisor、
VMPL0 安全模块、VMPL3 客户机这 3 种实体及对应的操作原语 (内存操作、RMP 操作、页表操作等), 证明了
客户机的私有内存不能被其他实体读取或更改、VMPL3 的客户机内核不能读取或修改 VMPL0 安全模块的私有
内存, 以及客户机地址翻译的正确性, 保证了客户机的机密性与完整性. 实现层扩展了 Verus 的内存权限, 并且将
权限的概念扩展到锁和寄存器, 以证明功能正确性, 为 VERISMO 的变量维护猜测空间, 证明密钥传播时相对其他
实体始终为机密变量. VERISMO 的验证只需 6 min, 验证过程中在 AMD 官方安全模块中发现恶意的 hypervisor
可以将 VMPL0 的信息暴露给 VMPL3, 并将该漏洞上报并得到确认.