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

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

其次, 由于缺少规范, 现有的验证工具难以独立于 rustc 开发. 它们往往需要集成 rustc 的部分代码或依赖其特
定的实现细节, 这限制了验证工具的通用性和可移植性. 而且, 由于 rustc 本身处于积极开发状态, 其内部实现经常
发生较大变化, 这导致验证工具需要不断适应这些变化, 进而影响了工具的稳定性和可靠性. 在缺乏规范的背景
下, 某些 rustc 的实现行为甚至难以评估其合理性. 例如, Rust 编译器可能会采用一些特殊的利基优化手段, 在不影
响表达能力的情况下调整结构体的内存布局以减小其整体大小. 例如, 两个结构体 struct A {u32 x; u64 y}; struct B
{u32x; u64 y}; 在 rustc 里可能有不同的二进制表示方式, A 有可能编译成先 x 后 y, 而 B 则是先 y 后 x. 在处理某
些底层指针操作, 如堆操作时, 结构体的内存布局就显得尤为关键. 正确的内存布局对于确保程序的正确性和安全
性至关重要. 然而, 由于缺乏明确的规范, 我们无法断言哪种布局是正确的, 这导致了在进行形式化验证时存在不
确定性. 针对这个问题, Gillian-Rust 通过自己的符号式编码方式来编码地址, 使得其是内存布局不相关的 (layout-
independent). RefinedRust 也提出任意的布局算法 (arbitrary layout algorithm) 对其验证过程进行了参数化, 确保验
证的正确性不受具体数据布局的影响. 而 Kani 实现为 rustc 的插件, 每次验证时从 rustc 获取编译后生成的具体信
息, 包括当前确定的数据结构布局.
然而, 定义 Rust 语言规范并非易事. 现有的资源如 Rust 参考手册、标准库文档、非安全代码指南等, 都不够
完整或不适宜作为权威参考. 一个准确的定义需要深入考虑 Rust 的设计原则、语言特性、生态系统和社区实践.
在过去一两年中, Rust 社区已经开始了一些旨在构建规范的项目. 例如, Ferrocene [76] 语言规范项目主要用于安全攸
关系统, 它提供了一个全面的框架, 覆盖了从语法到名称解析, 再到编译器的全面功能. Ferrocene 规范是用英语以
公理化的风格编写的, 类似于 C/C++规范的描述形式. 此外, a-mir-formality [77] 项目致力于构建 Rust 类型系统的形
式化模型, 特别是对 Rust 语言借用检查器的规则进行形式化定义. 而 MiniRust [78] 项目提供一个轻量级 Rust 语言
子集的操作语义, 描述 Rust 核心语言程序在执行时可能表现出的行为. 每个项目都有其独特的侧重点, 如何将这
些项目与现有的 Rust 官方文档整合, 形成一套连贯、全面的规范, 是一个亟待解决的问题. 我们可以看到, 形式化
语言的严谨性和无歧义性使其成为描述 Rust 规范的一个理想工具. 而一旦 Rust 规范得到明确定义, 它将反过来
促进形式化验证的发展.
(2) 对 Rust 标准库的依赖性在形式化验证中带来了额外的考量. 因为它要求验证过程不仅局限于用户编写的
代码, 还需涵盖标准库的实现, 以确保整个程序的正确性. 目前, 许多现有的验证工具在进行程序验证时, 通常采取
信任标准库的策略, 并不对其进行深入验证. 这不仅降低了验证的精确程度, 而且和依赖于特定的编译器版本一
样, 依赖于特定标准库版本也限制了验证器的通用性, 还增加了后期维护工作的难度. 有些工具, 如 Verus, 通过重
写部分标准库并提供一套抽象化的 API, 使得它们验证的程序基于这些抽象 API. 在验证某程序时, 如何清晰描述
并验证标准库接口的功能规约是需要解决的问题.
(3) Safe Rust 和 unsafe Rust 程序的联合验证是一项挑战性的工作. 安全 Rust 拥有许多高级特性, 例如高阶函
数、迭代器等高级抽象, 这些特性为开发者提供了便利和强大的表达能力, 但为自动化验证增加了难度. 而另一方
面, 不安全 Rust 中则涉及复杂且底层原始指针等操作, 且由于没有编译器的保障, 需要开发者确保所有的内存操
作都是合法的而不会导致段错误, 这就需要对内存地址的有效范围进行推理. 为了开发同时处理两者的工具需要
对 Rust 语言特性深入的理解, 还需要在设计上实现一种精巧的平衡, 既能提供对底层操作低级别的精准控制, 又
能自动高效地处理安全 Rust 中使用的高级特性, 可能还需要确保 unsafe Rust 不会破坏 safe Rust 的安全保障并利
用该安全保障来简化验证流程.

7 未来工作展望

结合面临的挑战与当前的研究进展, 本文认为 Rust 形式化验证方向未来值得关注的研究工作主要包括以下
几方面.
Rust 全语言的形式化语义建模: 有的方法建模了 Rust 语义的一个子集, 而不是实际的 Rust 语言, 无论是在
Rust 的表面语法层面还是在中间表示 (MIR) 层面的描述, 都包含了简化的假设来处理语言的复杂性. Rust 作为一
种多范式编程语言, 它巧妙地融合了命令式、函数式、面向对象和泛型编程等多种编程范式. 在这样的背景下, 探