一句话：提出在 Coq 中证明可靠的精化类型系统，支持 safe 与 unsafe Rust 代码的基础性半自动功能正确性验证。
Rust 基于所有权的类型系统静态保证内存安全，适合安全关键系统，但现有自动演绎验证工具既不产生可在证明助手中检查的基础证明，也仅限 safe 代码，而实际程序常在关键 API 中使用 unsafe。RefinedRust 是一个在 Coq 中证明可靠的精化类型系统，目标是对 safe 与 unsafe Rust 代码进行基础性半自动功能正确性验证。其原型工具将带注解的 Rust 代码翻译为 Coq 内嵌的 Rust 模型，再借助 Coq 中的分离逻辑自动化检查其是否满足类型系统；所有证明均由 Coq 检查，故自动化与类型系统本身无需被信任。作者通过验证一个涉及复杂 unsafe 指针操作推理的 Rust Vec 变体实现来评估其有效性。
Rust is a modern systems programming language whose ownership-based type system statically guarantees memory safety, making it particularly well-suited to the domain of safety-critical systems. In recent years, a wellspring of automated deductive verification tools have emerged for establishing functional correctness of Rust code. However, none of the previous tools produce foundational proofs (machine-checkable in a generalpurpose proof assistant), and all of them are restricted to the safe fragment of Rust. This is a problem because the vast majority of Rust programs make use of unsafe code at critical points, such as in the implementation of widely-used APIs. We propose RefinedRust , a refinement type system—proven sound in the Coq proof assistant—with the goal of establishing foundational semi-automated functional correctness verification of both safe and unsafe Rust code. We have developed a prototype verification tool implementing RefinedRust. Our tool translates Rust code (with user annotations) into a model of Rust embedded in Coq, and then checks its adherence to the RefinedRust type system using separation logic automation in Coq. All proofs generated by RefinedRust are checked by the Coq proof assistant, so the automation and type system do not have to be trusted. We evaluate the effectiveness of RefinedRust by verifying a variant of Rust’s Vec implementation that involves intricate reasoning about unsafe pointer-manipulating code.
@article{GaherSJKD24,
title = {RefinedRust: A Type System for High-Assurance Verification of Rust Programs},
author = {Lennard Gäher and Michael Sammler and Ralf Jung and Robbert Krebbers and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656422}
}