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

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2025,36(8):3604−3636 [doi: 10.13328/j.cnki.jos.007353] [CSTR: 32375.14.jos.007353] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
面向 Rust 语言的形式化验证方法研究综述

张卓若, 常 瑞, 杨申毅, 陈 芳

(浙江大学 计算机科学与技术学院, 浙江 杭州 310027)
通信作者: 常瑞, E-mail: crix1021@zju.edu.cn

摘 要: Rust 作为一种新兴的安全系统级编程语言, 以其创新的所有权模型和借用检查机制提供了内存安全和并
发安全保证. 尽管 Rust 的设计宗旨在于安全性, 但现有研究揭示了其仍面临诸多安全挑战. 形式化验证作为一种基
于严格数学基础的方法, 为 Rust 安全性提升提供了强有力保障. 通过构建精准清晰的语义模型, 可以证明遵循
Rust 检查规则的程序满足安全性要求; 借助 Rust 自动化验证工具能够帮助用户确保其 Rust 程序的安全性和正确
性. 对 Rust 形式化验证工作进行全面系统性分析. 首先介绍 Rust 核心语义和复杂特性, 并探讨 Rust 形式化语义的
研究与验证工作, 强调 Rust 类型系统在形式化验证中的潜力. 其次, 阐述面向 Rust 程序的自动化验证方法, 并对比
分析不同验证工具的功能、支持的语言特性、采用的验证技术和适用场景, 这对于在 Rust 项目实际开发流程中指
导工具的选择和集成有重要意义. 此外, 还总结 Rust 程序验证的典型实例, 展示形式化验证在确保程序正确性方面
的显著成效, 并结合验证实例总结工具使用建议供用户参考. 最后讨论当前领域的技术挑战, 并指出未来可能的研
究方向, 涵盖了 unsafe Rust 代码的验证、并发代码的验证、可信编译, 以及大模型驱动的形式化验证等. 旨在为
Rust 社区提供坚实的安全基础, 并推动形式化验证在 Rust 开发中的应用.
关键词: 形式化方法; Rust 语言; 程序验证; 形式语义; 内存安全
中图法分类号: TP311

中文引用格式: 张卓若, 常瑞, 杨申毅, 陈芳. 面向Rust语言的形式化验证方法研究综述. 软件学报, 2025, 36(8): 3604–3636. http://
www.jos.org.cn/1000-9825/7353.htm
英文引用格式: Zhang ZR, Chang R, Yang SY, Chen F. Survey on Formal Verification Research for Rust Language. Ruan Jian Xue
Bao/Journal of Software, 2025, 36(8): 3604–3636 (in Chinese). http://www.jos.org.cn/1000-9825/7353.htm

Survey on Formal Verification Research for Rust Language
ZHANG Zhuo-Ruo, CHANG Rui, YANG Shen-Yi, CHEN Fang
(College of Computer Science and Technology, Zhejiang University, Hangzhou 310027, China)
Abstract: As an emerging system programming language with a focus on safety, Rust ensures memory and concurrency safety through its
innovative ownership model and borrowing mechanism. Despite its design for safety, existing research has identified several safety
challenges that Rust still faces. Formal verification, grounded in rigorous mathematical principles, provides robust assurances for enhancing
Rust’s security. By constructing precise and well-defined semantic models, it becomes possible to formally prove that programs adhering to
Rust’s type system meet safety requirements. Automated verification tools for Rust further enable users to validate the safety and
correctness of their programs. This study presents a comprehensive and systematic analysis of formal verification approaches for Rust. It
begins by introducing Rust’s core semantics and complex features, followed by an exploration of research and verification efforts in Rust’s
formal semantics, emphasizing the role and potential of Rust’s type system in formal verification. Next, the study systematically compares
the capabilities, supported language features, underlying techniques, and application scenarios of various automated Rust verification tools.
These comparisons are instrumental in guiding tool selection and integration within real-world Rust development workflows. In addition,

* 基金项目: 国家重点研发计划 (2022YFB4501903)
本文由“形式化方法与应用”专题特约编辑陈明帅研究员、田聪教授、熊英飞副教授推荐.
收稿时间: 2024-08-26; 修改时间: 2024-10-14; 采用时间: 2024-11-26; jos 在线出版时间: 2024-12-10
CNKI 网络首发时间: 2025-04-03