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

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

5.2 Rust 安全关键应用的自动化验证

Rust 形式化验证在安全关键型应用的实例, 重点探讨其在可信计算、机密计算、云存储服务等方面的贡献.
这种结合形式化验证的方法, 不仅提升了 Rust 在高安全性能领域的应用前景, 也为确保现代计算系统的可靠性和
安全性打下了坚实基础.
加密库是现代应用程序可信计算基础的核心, 形式化验证能系统地防止加密软件中的缺陷, HACL-rs 项目 [69]
的目标是提供一个经过验证的、纯粹的 Rust 实现的加密原语库来确保安全性和可靠性, 致力于将底层使用 F*语
言编写经过严格形式化验证的密码库 HACL*转化为纯 safe Rust 代码. HACL-rs 计划取代当前 libcrux 库中使用
的 HACLC 代码部分从而消除 C 语言外部函数接口 (FFI) 的依赖, 使 libcrux 成为一个完全使用安全 Rust 编写的
库, 提升代码的整体安全性并简化开发和维护过程. 在 HACL-rs 项目的推动下, Zulip 团队 [70] 设计了一种用于为密
码构造编写简洁、可执行、形式化规范的语言 HACSPEC, 从语法上看, HACSPEC 是安全 Rust 的一个纯函数子
集, 它不允许可变引用, 因此避免了有状态 Rust 程序的大部分复杂性. Rust 应用可以直接使用 HACSPEC 代码作
为所需加密组件的原型实现, Rust 强大的类型安全保证意味着未经验证的应用程序中的错误不会影响经过验证的
加密代码的正确性或安全性, 此外 HACSPEC 还能自动转换为 F*, Coq 和 EasyCrypt 语言. Hax [71] 项目进一步扩展
了 HACSPEC 的范围, 成为一种用于验证 Rust 程序的工具, Hax 能够将 Rust 的大部分子集翻译为 F*或 Coq 等形
式化语言, 但不支持包含 unsafe 代码块和可变引用返回类型的代码, 通过 Hax 开发者可以更为可靠地验证和确保
Rust 程序的安全性.
机密计算即服务 (CCaaS) 是一种新兴的服务模式, CCaaS 需要向数据提供商保证, 服务不会将其隐私泄露给
任何未经授权的一方, 并在服务完成后清除其数据. Chen 等人 [72] 在 Coq 中形式化地定义了安全目标 PoBF, 包含
无泄漏 (no leakage) 和无残留 (no residue), 并证明了在哪些安全约束下可以满足 PoBF, 这些约束指导 PoBF 兼容
框架 (PoCF) 的设计实现. PoCF 包括 Rust 语言实现的用于不同硬件 TEE 的通用库、CCaaS 原型 enclaves 和用于
证明 PoBF 满足性的验证器, 它利用 Rust 的强大类型系统和安全特性构建了一个具有隐私保护契约的验证状态
机, 由 Rust 编译器检查内存和类型安全性, 由 Rust 自动验证工具 Prusti 保证类型状态实现与其规范的一致性, 最
后 MIRAI [73] 进行污点分析, 确保 CC 任务的函数调用参数不包含敏感数据结构, 防止机密信息泄露. 实验表明
PoCF 所引入的保护机制在运行时的性能开销很小.
Bornholt 等人 [14] 在 Amazon S3 云对象存储服务中对一种新的键值存储节点实现的正确性进行了验证, 采用
了轻量级形式化方法, 这种方法结合了基于属性的测试和无状态模型检查, 将系统的预期正确性分解为独立的属
性, 并分别利用最适合的工具检测不同属性. 在并发代码的验证过程中, 他们特别采用了两种无状态模型检查器:
Loom 和该文章提出的 Shuttle. Loom 被用于可靠地检查小型但关键的并发代码的所有可能交错情况, 例如自定义
的并发原语. 而 Shuttle 则用于随机检查那些 Loom 无法扩展到的大型测试场景中的交错情况. 作为规范, 他们使
用了一个可执行的参考模型, 该模型用 Rust 语言编写, 定义了系统中组件允许的顺序和无崩溃的行为. 这种选择
使得工程团队能够更容易地编写和维护参考模型, 因为它与实现系统的语言相同. 他们的轻量级形式化方法通过
测试实现, 其中形式化验证测试与常规单元测试类似, 都是使用 Rust 的内置测试基础设施来运行. 这种方法不仅
提高了验证过程的效率, 而且使得形式化验证与日常开发流程无缝集成. 通过这项工作, 他们成功地阻止了 16 个
潜在问题进入生产环境, 这些问题包括崩溃一致性和并发性问题. 这一成果表明, 轻量级形式化方法不仅能够有效
地发现和预防生产环境中的问题, 而且随着系统的演化, 这种方法还可以不断地扩展和改进.

5.3 Rust 自动化验证工具使用建议
(1) 形式化与非形式化方法的结合: 当前许多 Rust 程序验证案例中不仅采用形式化方法, 还融入了如污点分
析、模糊测试、基于属性的测试、编译器静态检查等其他非形式化技术. 例如, 亚马逊在验证 S3 云对象存储服务
时 [14] , 结合了基于属性的测试和无状态模型检查, 将系统预期的正确性分解为独立的属性, 并利用最适合的工具
分别检测这些属性. 在对 CCaaS 的验证过程中, 除了利用 Prusti 进行类型状态实现与规范的一致性检查外, 还进行
污点分析以防止机密信息泄露. 在验证 Rust 操作系统 Theseus 内存子系统时 [63] , 为验证物理内存和虚拟内存之间