Formal Verification of Rust with Stainless

Writing correct software is hard, yet in systems that have a high failure cost or are not easily upgraded like blockchains, bugs and security problems cannot be tolerated. Therefore, these systems are perfect use cases for formal verification, the task of mathematically proving that a system conforms to its specification. Many recent blockchains are implemented in the Rust programming language because it guarantees memory safety at compile-time while providing full control over efficiency to the programmer. To explore the powerful combination of the safety guarantees of Rust’s compiler with the ability to formally verify high-level properties on programs, we present Rust-Stainless. Stainless is a formal verification tool for Scala backed by Satisfiability modulo theories (SMT) solvers. Rust-Stainless is a frontend for Stainless that extracts a subset of Rust, translates it to Scala and verifies it with Stainless. In this thesis project, I significantly advance the feature set of Rust-Stainless, increasing its expressiveness to programs that cannot be processed in Scala Stainless. In particular, this thesis adds support for mutability and in-place updates, by introducing a translation for mutability from Rust to Scala. I argue that the translation yields equivalent runtime semantics in both languages and refine it to work with Stainless. This allows to verify data structures implemented in Rust without sacrificing performance. Other new features are traits with verified contracts, references, and heap allocation. The tool is evaluated on real-world Rust examples from a blockchain context. Remaining limitations concern missing support for some Rust language features, the limitation of only processing one crate at a time, and certain aliasing restrictions of the current Stainless backend for mutability. Finally, I explore possible promising ways for the future advancement of Rust-Stainless.