RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
Jinhua Wu, Yuting Wang, Liukun Yu, Linglong Meng
TL;DR
RustCompCert tackles the challenge of building a trustworthy Rust-to-assembly compiler by layering a verified frontend on top of the proven CompCert backend to achieve end-to-end semantics preservation and memory safety. The approach focuses on a core Rust subset, Rustlight, with a verified frontend that introduces Drop Elaboration and a Polonius-based borrow-checking pass, whose algorithm is formalized and verified within the Kildall framework as Polonius. A key contribution is the refinement relation between RustIRspec and the RustIR semantics, enabling high-level safety proofs to transfer through compilation to assembly. The work has practical implications for enabling source-level verification of Rust programs by reducing the verification burden to the functional correctness of Rust code under a memory-safe, formally verified pipeline.
Abstract
We present our ongoing work on developing an end-to-end verified Rust compiler based on CompCert. It provides two guarantees: one is semantics preservation from Rust to assembly, i.e., the behaviors of source code includes the behaviors of target code, with which the properties verified at the source can be preserved down to the target; the other is memory safety ensured by the verifying compilation -- the borrow checking pass, which can simplify the verification of Rust programs, e.g., by allowing the verification tools focus on the functional correctness.