Enabling Rich Lightweight Verification of Rust Software
type: CreativeWork
description: Rust is a novel programming language that is rapidly gaining adoption in the software industry thanks to its performance and safety properties. Among its strengths, Rust's type system is designed to detect at compile time certain kinds of memory-related bugs, such as dangling pointers and null dereferences. However, the language does not aim to detect functional errors; how to do this efficiently is in general an open topic in the field of software verification. This thesis explores the link between Rust and software verification, showing how the static properties of Rust can be leveraged to develop new, simpler, verification techniques. In particular, we identify formalization, specification and automation challenges that block user-friendly, scalable, deductive verification. To address these challenges we develop two novel verification techniques for Rust that work on different subsets of the language. Our first new technique focuses on verification of programs that are entirely written in safe Rust: the portion of the Rust language in which the compiler takes care of guaranteeing absence of memory-related bugs. For this setting, we define a model of the properties of Rust types in the implicit dynamic frames logic — a variant of separation logic — using the Viper language. We then develop a new static analysis that tracks the capabilities of Rust types (e.g., the ability to read or write a certain memory location), and we use its results in an algorithm that constructs automatically a core proof of the program, which encodes the immutability and aliasing guarantees of Rust types. This proof is expressed in the implicit dynamic frames logic, but our technique hides this as an implementation detail, effectively shielding the verification users from the complex details of the logic. To verify the functional correctness of a program, users only have to specify the functional behavior of its functions, writing contracts such as preconditions and postconditions. To thi…
abstract: Rust is a novel programming language that is rapidly gaining adoption in the software industry thanks to its performance and safety properties. Among its strengths, Rust's type system is designed to detect at compile time certain kinds of memory-related bugs, such as dangling pointers and null dereferences. However, the language does not aim to detect functional errors; how to do this efficiently is in general an open topic in the field of software verification. This thesis explores the link between Rust and software verification, showing how the static properties of Rust can be leveraged to develop new, simpler, verification techniques. In particular, we identify formalization, specification and automation challenges that block user-friendly, scalable, deductive verification. To address these challenges we develop two novel verification techniques for Rust that work on different subsets of the language. Our first new technique focuses on verification of programs that are entirely written in safe Rust: the portion of the Rust language in which the compiler takes care of guaranteeing absence of memory-related bugs. For this setting, we define a model of the properties of Rust types in the implicit dynamic frames logic — a variant of separation logic — using the Viper language. We then develop a new static analysis that tracks the capabilities of Rust types (e.g., the ability to read or write a certain memory location), and we use its results in an algorithm that constructs automatically a core proof of the program, which encodes the immutability and aliasing guarantees of Rust types. This proof is expressed in the implicit dynamic frames logic, but our technique hides this as an implementation detail, effectively shielding the verification users from the complex details of the logic. To verify the functional correctness of a program, users only have to specify the functional behavior of its functions, writing contracts such as preconditions and postconditions. To thi…
author: Poli, Federico; id_orcid0000-0001-7709-1965
language: en
keywords: VERIFICATION (SOFTWARE ENGINEERING); Software Verification; Formal Verification; Deductive Verification; Rust (programming language); Separation Logic; First-order logic; SMT solvers; Software Engineering, info:eu-repo/classification/ddc/004, Data processing, computer science
license: http://creativecommons.org/licenses/by/4.0/
date published: 2024
date modified: 2026-07-27T19:27:05Z
provider: ETH Zürich
publisher: Networked Digital Library of Theses and Dissertations
type: WebPage
source organization: ETH Zurich

PropertyValue
property ID: Handle
value: http://hdl.handle.net/20.500.11850/703796

PropertyValue
property ID: DOI
value: 10.3929/ethz-b-000703796