Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Hybrid Approach to Semi-automated Rust Verification

Sacha-Élie Ayoun, Xavier Denis, Petar Maksimović, Philippa Gardner

TL;DR

This work presents a hybrid verification pipeline for Rust that splits the verification of safe and unsafe code between Creusot and a novel Gillian-Rust tool, respectively. By embedding a shared specification language and RustBelt/RustHornBelt-inspired abstractions, the approach achieves end-to-end verification of real-world Rust, including unsafe components, with substantial automation and speedups over prior work. The paper details a layout-aware symbolic heap, automated reasoning for lifetimes and borrows, and prophetic reasoning to enable functional correctness, demonstrated on standard library types via a Merge Sort case study and multiple benchmarks. The results suggest that hybrid verification can scale to real unsafe Rust code while reusing safe-code proofs, with practical impact for Rust systems software and library verification. Limitations remain (e.g., closures, multiple lifetimes, concurrency), but the framework provides a concrete path toward broader, automated end-to-end Rust verification.

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.

A Hybrid Approach to Semi-automated Rust Verification

TL;DR

This work presents a hybrid verification pipeline for Rust that splits the verification of safe and unsafe code between Creusot and a novel Gillian-Rust tool, respectively. By embedding a shared specification language and RustBelt/RustHornBelt-inspired abstractions, the approach achieves end-to-end verification of real-world Rust, including unsafe components, with substantial automation and speedups over prior work. The paper details a layout-aware symbolic heap, automated reasoning for lifetimes and borrows, and prophetic reasoning to enable functional correctness, demonstrated on standard library types via a Merge Sort case study and multiple benchmarks. The results suggest that hybrid verification can scale to real unsafe Rust code while reusing safe-code proofs, with practical impact for Rust systems software and library verification. Limitations remain (e.g., closures, multiple lifetimes, concurrency), but the framework provides a concrete path toward broader, automated end-to-end Rust verification.

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.
Paper Structure (25 sections, 8 equations, 10 figures)

This paper contains 25 sections, 8 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Overview
  3. A hybrid approach: Creusot + Gillian-Rust
  4. Example usage of Gillian-Rust
  5. Building Gillian-Rust on top of Gillian
  6. Reasoning about the real Rust heap
  7. Layout-independent memory addresses
  8. Objects in the Rust symbolic heap
  9. Specifying the Rust heap: the typed points-to core predicate
  10. Automating reasoning about mutable borrows
  11. Modelling lifetimes: core predicates
  12. Modelling full borrows: guarded predicates
  13. Proving safety of borrow extraction
  14. Functional correctness and prophetic reasoning
  15. Representations, parametric prophecies, and observations
  16. ...and 10 more sections

Figures (10)

  • Figure 1: A high-level illustration of the differences and connections between the world of pure representations, observed by Creusot, and the world of real representations, observed by RustHornBelt and Gillian-Rust.
  • Figure 2: Update of a laid-out node corresponding to $n\ *\ $bytes.
  • Figure 3: Consumer and producer rules for lifetime tokens (simplified, excerpt)
  • Figure 4: An invalid and a valid mutable reference.
  • Figure 5: Excerpts: observation rules from RustHornBelt (top) and observation consumer/producer rules (bottom)
  • ...and 5 more figures