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

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

索如何在一个统一的框架内对这些编程范式进行综合的形式化建模, 成为程序语言研究领域的一个重要且具有挑
战性的课题. 这不仅能够推动 Rust 语言本身的理论发展, 也能为理解和应用 Rust 提供更深层次的洞见. 然而, 鉴
于前文提到的 Rust 语言缺乏统一规范的问题, 这一研究过程需要 Rust 验证人员与 Rust 社区的开发者进行紧密的
交流与合作, 共同推进.
Rust 自动化验证工具的优化及提升: 在自动化验证工具的研发领域, 扩展对 Rust 语言更多特性的支持是提升
验证准确性和实用性的关键. 鉴于 Rust 的许多语义特性尚缺乏官方规范, 实现工具与现有及开发中的 Rust 规范
的整合显得尤为重要. 此外, 不同的验证技术各有优势, 适用于不同的场景. 探索如何将这些技术融合到统一的框
架之中, 实现优势互补, 对于拓宽 Rust 验证领域的研究视野和应用范围具有重大意义. 如表 2 所示, 不同的验证工
具针对不同的语言特性和验证性质提供了不同程度的支持. 尽管目前 Rust 的验证研究在处理某些技术时存在一
定程度的相互借鉴, 但各研究团队或项目大多独立开展工作, 且在测试过程中因针对不同的测试集而缺少直接的
比较. 因此, 对现有技术进行全面的比较分析, 深入探讨不同工具在性能、功能支持和准确性等方面的表现, 并在
此基础上进行优势整合, 对于推动 Rust 在学术界和工业界的应用至关重要. 例如, 在统一验证框架中, 验证不同性
质, 如内存安全性, 功能正确性时可以分别使用不同的工具; 验证包含 safe 和 unsafe 代码的程序, 使用不同工具分
别验证 safe 和 unsafe 的部分并保证语义一致性和结果整合后整体的正确性.
对非安全 Rust 代码的验证: 形式化验证能够帮助开发者更安全、更有效地使用 unsafe 代码. 然而现有研究仅
触及了冰山一角, 大多停留在学术概念验证阶段. 要实现其在工业级别的广泛应用, 仍需跨越重大的技术障碍. 此
外, 已有针对 unsafe 代码的验证主要涉及两方面. 一方面是针对原始指针, 即确保任何时候该指针的访问都是合法
和安全的. 另一方面是针对 Rust 的核心库调用一些底层不安全函数的场景, 例如直接使用原始指针进行内存分配
和释放的函数或将 Rust 类型强制转换为其他任意类型的函数. 实际上, Rust 中还有其他一些 unsafe 操作, 比如利
用 Rust 中调用不安全函数的能力 (FFI) 实现与 C 代码互操作, 这在 Rust 的 unsafe 代码使用中非常普遍且存在安
全隐患 [79] . 任何提供 C 接口的外部库中的函数都可以作为不安全函数从 Rust 中调用, 这为跨语言集成提供了便
利. 然而, 一个关键的挑战是如何确保这些函数在跨不同编程语言编写的程序中不会违反 Rust 类型系统所提供的
安全保证. 这是因为, 尽管 Rust 的类型系统在语言内部提供了内存安全保证, 但当涉及外部 C 函数时, 这些保证可
能不再适用. Rust 社区探索了很多方法来处理跨语言调用的问题, 包括提供更安全的抽象、改进的文档和工具支
持, 而形式化验证也可以帮助确保所有的外部调用都符合 Rust 的安全性原则. 汪宇霆 [80] 正在进行的验证工作是该
研究领域的一项探索性尝试. 该研究通过设计 Rust 核心语言的开放语义和语言接口并设计带所有权的语义接口,
作为 safe Rust 和 unsafe Rust 的交互协议. 然后再将该语义接口与编译器的语义接口整合, 获得支持分离编译的语
义接口, 借助 CompCert 分离编译框架验证 safe Rust 函数和 unsafe C 函数之间是否正确交互, 并保证完整程序编
译和链接后的正确性. 而形式化可以用于的另一种场景是对静态可变变量的 unsafe 代码的逻辑推理. Rust 语言中
的静态可变变量 (static mut) 允许创建全局可变状态, 这使得多个线程能够访问并可能同时修改这一全局数据. 在
这种情况下, 开发者需要采取额外的预防措施来预防数据竞争的发生.
对并发 Rust 代码的验证: 目前针对并发 Rust 程序的形式化验证工作较少. 现有工作中, RustBelt 基于并发分
离逻辑可以支持 Rust 中并发程序的证明, 证明了 Mutex, RwLock 等同步原语库的线程安全, 但是该工作没有开发
基于并发分离逻辑的 Rust 语言程序的自动化验证工具; 现有基于模型检测的并发程序自动验证方法只针对死锁
等部分问题, 还有大部分空缺亟需填补, 例如 unsafe 代码中操作共享内存造成的数据竞争问题, 消息传递造成的与
预期不符合的时序逻辑错误等. 实际上, 不仅限于形式化验证领域, 从整体上看, 现有对 Rust 安全研究的工作也主
要还是以研究 Rust 内存安全为主, 对 Rust 并发安全的研究有所欠缺. 但在现实 Rust 软件中, 并发漏洞的数量仅次
于内存漏洞 [81] . Rust 在编译时防止了许多潜在的并发错误, 然而, 并发编程在涉及复杂的生命周期、互斥锁的死
锁或异步任务的协作等复杂的并发场景中仍然充满挑战, 需要开发者小心设计和实现以避免逻辑错误. 形式化的
验证方法使用数学对程序和系统进行精确的建模和严格的验证, 这对于构建高可靠性、高性能的并发系统尤为重
要. 然而, 并发技术的特性也决定了其验证是相对困难的. 由于组件间的相互影响, 一般难以对单独一个组件的正
确性进行验证, 这也导致了在规模较大的系统中, 无法使用简单的验证方法进行模块化的验证. 因此, 开发能够支