软件学报

作者：张卓若，常瑞，杨申毅，陈芳

单位：张卓若，浙江大学 计算机科学与技术学院, 浙江 杭州 31002711,常瑞，浙江大学 计算机科学与技术学院, 浙江 杭州 31002702,杨申毅，浙江大学 计算机科学与技术学院, 浙江 杭州 31002703,陈芳，浙江大学 计算机科学与技术学院, 浙江 杭州 31002704

关键词：形式化方法;Rust语言;程序验证;形式语义;内存安全

基金：国家重点研发计划(2022YFB4501903)

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

来源：2025年第8期

《软件学报》期刊编辑部

查看软件学报杂志2025年第8期