RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust

TL;DR

This paper introduces RustCompCert, a verified Rust compiler based on CompCert, ensuring semantics preservation and memory safety, simplifying verification of Rust programs.

Contribution

It presents the development of an end-to-end verified Rust compiler that guarantees semantics preservation and memory safety through verifying compilation.

Findings

Semantics preservation from Rust to assembly confirmed

Memory safety ensured by borrow checking pass

Simplifies verification of Rust programs

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.