We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust's rich region-based type system to eliminate memory reasoning for a large class of Rust programs by translating them to a pure lambda-calculus, as long as they do not rely on interior mutability or unsafe code. Doing so, we relieve the proof engineer of the burden of memory-based reasoning, allowing them to instead focus on functional properties of their code.
This talk describes CreuSAT, a formally verified SAT solver written in Rust. In addition to implementing the core conflict-driven clause learning (CDCL) algorithm, CreuSAT also implements a series of crucial optimizations. The most important of these is the two watched literals scheme with blocking literals and circular search, the variable move-to-front (VMTF) decision heuristic, clause deletion, phase saving, and moving average based restarts.
The resulting solver is the first deductively verified solver which is able to consistently solve problems from the SAT competition. This is done while maintaining a relatively small code base, amounting to around 4 thousand lines of proof code and program code combined, with a low proof overhead of around three lines of proof code per line of program code.
Statically analyzing information flow, or how data influences other data within a program, is a challenging task in languages with mutation and pointers. Prior work addressed these challenges with bespoke type systems to encode information flow, such as in JFlow (for Java) and FlowCaml (for OCaml). We demonstrate that Rust's existing system of ownership types can repurposed for modular information flow analysis. We describe our analysis using Oxide, a formal model of safe Rust, and prove its soundness as noninterference. We implement the analysis as Flowistry, a tool that analyzes information flow within Rust's MIR CFG. And we show that Flowistry is reasonably precise versus a whole-program analysis via an evaluation on a dataset of large Rust codebases.
Will Crichton is a 6th year CS Ph.D. student at Stanford University advised by Profs. Pat Hanrahan and Maneesh Agrawala. His research combines programming language theory and cognitive psychology to build better tools for programmers. Will just defended his thesis, "Revisiting Program Slicing with Ownership-based Information Flow", and will soon be starting a postdoc with Shriram Krishnamurthi at Brown to study the learnability of Rust.
crux-mir is a symbolic testing tool for Rust. The user writes test cases using symbolic variables as inputs; crux-mir uses symbolic execution to check that the tests pass for all possible values of the symbolic variables. crux-mir checks for absence of panics, overflows, and some forms of undefined behavior, and it supports user-defined assertions. Recently, crux-mir gained support for calling Cryptol specifications directly from Rust code and for compositional reasoning, which allows efficiently verifying more complex functions, such as Rust implementations of cryptographic primitives. In this talk, I'll describe the design of crux-mir and show some examples of its use, with particular focus on the newer Cryptol and compositional reasoning features.
Ferrocene is an effort to bring Rust into the realm of safety-critical software while also bringing tangible benefits to so called mission-critical efforts. The project has been ongoing for about a year now. This talk will give an overview of current findings and particularly an observation of the current state of the safety-critical ecosystem.
Particularly, it will share observations on the application of formal methods in the realm right now.
Florian Gilcher is a co-founder of Ferrous Systems and a Rust teacher since 2015. Previously a member of the Rust Community and Core team and a co-founder of the Rust Foundation, Florian is currently focusing to bringing Rust to safety critical systems, such as cars.
Celina Val and Daniel Schwartz-Narbonne will present their work on Kani, a Rust model-checker they are developing at Amazon.
Kani is a Rust verification tool based on model checking. With Kani, you can ensure that broad classes of problems are absent from your Rust code by writing proof harnesses, which are broadly similar to tests (especially property tests). Kani is especially useful for verifying unsafe code in Rust, where many of the language's usual guarantees can no longer be checked by the compiler. But Kani is also useful for finding panics in safe Rust, and it can check user-defined assertions.
Kani is currently in the initial development phase, and has not yet made an official release. It is under active development, but it does not yet support all Rust language features."
Xavier Denis will discuss Creusot, his deductive verifier for Rust. Creusot aims to provide efficient verification of complex safe Rust code, and is backed by the Why3 verification platform. In this talk we'll briefly cover the high-level architecture of Creusot and some of the unique features in the tool.
Herman Venter gave a retrospective view of his work on MIRAI, an abstract interpreter for MIR code. We went over key design choices for abstract interpreters and the tradeoffs they imply.
Find the YouTube video here.
Formal Verification of Subsets of Rust
Rust is a big and complex language. Fortunately, it contains a number of interesting sublanguages for which formal verification is more manageable. I will give an overview of three projects that we are working on in my group.
ConCert is a Coq framework for reasoning about functional programs, in particular focussing on smart contracts. As part of this we have developed a general backend to the Coq proof assistant which allows one to generate provably correct functional rust programs. One main use case is to generate rust smart contracts which can be used on the concordium blockchain.
HACSPEC is a subset of rust for the specification of high assurance cryptography. We have used it to specify the BLS elliptic curve. This sepcification can be translated to Coq from where we use fiat-cryptography and BedRock to generate a correct by construction, efficient, platform independent implementation.
Find the YouTube video here.
Unfortunately this meeting was not record (my bad).
A summary will be posted soon.
The slides are here
During this meeting, we will introduced the RFMIG, and had a presentation from Vytautas Astraukas of Prusti, showing a little glimpse of verification for Rust software.