A Hybrid Approach to Semi-automated Rust Verification

TL;DR

This paper introduces Gillian-Rust, a semi-automated verification tool for unsafe Rust code, combining automated safe Rust verification with targeted semi-automated unsafe code analysis, achieving faster verification times.

Contribution

It presents Gillian-Rust, a novel verification tool that automates reasoning about unsafe Rust code using a rich separation logic, integrated with existing safe Rust verifiers.

Findings

Gillian-Rust verifies real-world Rust code with minimal annotations.

The tool achieves verification speeds orders of magnitude faster than comparable tools.

Hybrid approach effectively combines automated and semi-automated verification methods.

Abstract

We propose a hybrid approach to end-to-end Rust verification where the proof effort is split into powerful automated verification of safe Rust and targeted semi-automated verification of unsafe Rust. To this end, we present Gillian-Rust, a proof-of-concept semi-automated verification tool built on top of the Gillian platform that can reason about type safety and functional correctness of unsafe code. Gillian-Rust automates a rich separation logic for real-world Rust, embedding the lifetime logic of RustBelt and the parametric prophecies of RustHornBelt, and is able to verify real-world Rust standard library code with only minor annotations and with verification times orders of magnitude faster than those of comparable tools. We link Gillian-Rust with Creusot, a state-of-the-art verifier for safe Rust, by providing a systematic encoding of unsafe code specifications that Creusot can use but cannot verify, demonstrating the feasibility of our hybrid approach.