Enabling Rich Lightweight Verification of Rust Software

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 this end, we offer program annotations with syntax and semantics identical to those of boolean Rust expressions, with some restrictions regarding side-effects and determinism that we describe with a definition of purity. Some aspects of Rust require special annotations. For example, to describe formally the relation between returned references and the function arguments that they block according to type system rules, we introduce a new program annotation called a pledge. We implement our technique in an open-source verification tool called Prusti, which we use to evaluate our technique on several collections of programs. Overall, by leveraging Rust types to construct the core proof automatically, the annotations required by our technique are drastically simpler, and shorter, than those of verification techniques for other programming languages. When a Rust program is not entirely safe, but also contains unsafe code, the strong properties of Rust types are weakened by some exceptions. For example, libraries that are implemented with unsafe code can expose interior mutability, meaning that they can mutate values behind shared references that, in a fully-safe program, would be immutable. Naively applying the verification techniques for fully-safe code to this setting would be unsound, because a verifier would incorrectly assume that interior mutability cannot cause mutations. To handle these cases, we develop a second new verification technique to reason about safe clients: safe programs that use trusted libraries implemented with unsafe code. These clients pose verification challenges due to the ability to observe interior mutability. To address this, we base our technique on a new notion of implicit library capabilities: properties of a Rust type, such as immutability or non-aliasing, that are not defined by the Rust language as in the case of references, but are determined by the developers of the Rust library. We introduce new library annotations to declare these capabilities explicitly, and we develop a verification technique that uses the capabilities to verify the functional correctness of safe clients based on an encoding into first-order logic. Our technique supports an expressive variety of capabilities: core capabilities correspond to the properties of regular Rust references in safe code, while extended capabilities go one step beyond and enable expressing new properties that do not have an equivalent in safe code. Each of these capabilities has particular properties, including unique access to a memory location, write access, immutability, and absence of concurrent usages. For our core capabilities, we prove correctness of their properties by developing a novel proof technique. This derives the properties of core capabilities from those of Rust references, side-stepping some problems posed by the current absence of formal semantics for unsafe code. We implement our technique in an open-source verifier called Mendel, which we use to verify functional properties of sequences of API calls to popular Rust libraries, including Rc, Arc, Cell, RefCell, AtomicI32, Mutex, and RwLock. Our results show that our technique is expressive enough to specify the functional behavior of real-world API methods, while requiring little annotation on the client side of their libraries. Overall, the verification techniques that we develop are lightweight because they require few user annotations, while still being rich enough to verify expressive user-chosen properties. The verification tools that we build around them are designed to offer a particularly curated user experience, thanks to some usability choices and solutions that we also describe.

Grantor dc:publisher

ETH Zurich

Year dc:date

2024

Author dc:creator

• Poli, Federico; id_orcid0000-0001-7709-1965

Contributors dc:contributor

• Müller, Peter; id_orcid0000-0001-7709-1965
• Summers, Alexander J.
• Jung, Ralf; id_orcid0000-0001-7709-1965
• Kunčak, Viktor

• 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

Statement dc:rights

• info:eu-repo/semantics/openAccess
• Creative Commons Attribution 4.0 International

Licence

• http://creativecommons.org/licenses/by/4.0/

Language dc:language

en

Identifier

https://doi.org/10.3929/ethz-b-000703796

OAI identifier oai:identifier

oai:www.research-collection.ethz.ch:20.500.11850/703796