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

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

持模块化并具有良好可扩展性的 Rust 程序并发验证方法, 是一个重要课题.
对 Rust 编译器的形式化验证: Rust 语言因其内存安全的保证, 被认为是开发安全关键型应用的理想选择. 但
是, 目前基于 LLVM 的 Rust 编译器工具链并未提供足够的安全验证, 这限制了 Rust 在高安全需求场景下的应用
潜力. 尽管社区内对于开发一个经过验证的 Rust 编译器工具链的呼声日益高涨, 但这一目标的实现尚未取得显著
进展. 一个可能发展方向是将 Rust 编译到 Vellvm [82] 或 CompCert 的 Clight [83] 中间表示, 可以复用一部分现有的经
过验证的编译器工具链. 这种验证工作不仅能够增强 Rust 编译器本身的可靠性, 也将为构建更为安全的软件生态
系统提供坚实的基础.
大模型驱动的 Rust 形式化验证: 近年来, 各大语言模型 (large language model, LLM) 蓬勃发展, 形式化验证领
域的许多学者也开始积极探索大语言模型的应用潜力. 这些模型在代码理解和自然语言到形式化规范语言的转换
方面展现出巨大潜力. 利用大语言模型来解释代码的功能、约束和预期行为, 有助于降低形式化专家学习 Rust 语
言的成本, 并在人工指导下将这些知识转化为形式化规范. 目前, 学者们已经成功地将大语言模型应用于提高定理
证明过程的自动化水平. 例如, Song 等人 [84] 设计大型语言模型辅助的 Lean Copilot 框架用于证明定理过程中的自
动化, 能够实现证明步骤建议、自动完成中间证明目标、选择相关前提条件等, 实验结果表明, 这种方法在定理证
明过程中相较于传统的基于规则的自动化方法, 更有效地辅助了人工操作, 提高了自动化程度. Wu 等人 [85] 和
Jiang 等人 [86] 也分别针对 Isabelle/HOL 利用大语言模型将数学问题翻译为形式化语言实现自动化定理证明. 尽管
这些尝试取得了显著进展, 但目前大语言模型尚未能够解决复杂实际系统应用程序的形式化验证问题. 未来如果
能构建一个专门针对 Rust 程序及其验证的大规模数据库, 用于训练大语言模型, 将有望扩展其在 Rust 形式化验
证中的应用范围, 并提高验证的准确度. 目前, 将大语言模型与 Rust 验证工具相结合的研究还处于初期阶段. 尽管
已有尝试, 如将 ChatGPT 与 Kani [87] 或 Verus [88] 等验证工具结合, 辅助编写断言条件等程序属性, 但这些尝试仍然
有限. 如果能够将大语言模型更深入地集成到 Rust 验证框架中, 实现轻量级的形式化验证或混合代码审查与测试,
将有望形成一个更加完整、便捷且高度自动化的 Rust 形式化验证生态系统, 从而提升形式化验证的实用性和影
响力.

References:
[1] Boos K, Liyanage N, Ijaz R, Zhong L. Theseus: An experiment in operating system structure and state management. In: Proc. of the 14th
USENIX Conf. on Operating Systems Design and Implementation. Berkeley: USENIX Association, 2020. 1.
[2] Redoxfs. 2017. https://gitlab.redox-os.org/redox-os/redoxfs
[3] Lyu S, Rzeznik A. Going serverless with the Amazon AWS Rust SDK. In: Lyu S, Rzeznik A, eds. Practical Rust Projects: Build
Serverless, AI, Machine Learning, Embedded, Game, and Web Applications. 2nd ed., Berkeley: Apress, 2023. 201–246. [doi: 10.1007/
978-1-4842-9331-7_6]
[4] Database drivers and ORMs for Rust that are ready for production. 2020. https://blog.logrocket.com/11-database-drivers-and-orms-for-
rust-that-are-ready-for-production
[5] Servo. 2017. https://github.com/servo/servo
[6] Smoltcp. 2017. https://github.com/smoltcp-rs/smoltcp
[7] Solana. https://solana.com/zh
[8] Xu H, Chen ZB, Sun MS, Zhou YF, Lyu MR. Memory-safety challenge considered solved? An in-depth study with all Rust CVEs. ACM
Trans. on Software Engineering and Methodology (TOSEM), 2022, 31(1): 3. [doi: 10.1145/3466642]
[9] Mergendahl S, Burow N, Okhravi H. Cross-language attacks. In: Proc. of the 29th Network and Distributed System Security Symp. San
Diego: The Internet Society, 2022. 1–17.
[10] system-pclub. 2020. https://github.com/system-pclub/rust-study
[11] Hu S, Hua BJ, Ouyang WR, Fan QL. A survey of Rust language security research. Journal of Cyber Security, 2023, 8(6): 64–83 (in
Chinese with English abstract). [doi: 10.19363/J.cnki.cn10-1380/tn.2023.11.06]
[12] Cui M, Chen C, Xu H, Zhou Y. SafeDrop: Detecting memory deallocation bugs of Rust programs via static data-flow analysis. ACM
Trans. on Software Engineering and Methodology, 2023, 32(4): 1–21.
[13] Jung R, Jourdan JH, Krebbers R, Dreyer D. RustBelt: Securing the foundations of the Rust programming language. Proc. of the ACM on