Rust Formal Methods Interest Group

WG repo | Zulip Channel

The RFMIG provides a forum for academics, industry users and any other interested party discuss and collaborate on the challenges of Rust program verification.

Our objectives are to:

Improve communication between formal tool developers and the Rust core teams

  • Hold 'office hours' with Rust team members to answer questions about the rustc API or the direction of the language.
  • Identify weak points in Rust's current tool interfaces, help shepherd the improvements the formal methods community needs.

Foster a community of formal methods tools and users

  • Provide a platform for tool developers to share their work and encourage collaboration.
  • Gather feedback and input from industrial and hobbyist users of formal method tooling.
  • Work towards improving tool inter-compatibility, in particular of specifications.

Interesting projects

These initiatives may interest the developers of formal methods tools for Rust, don't hesitate to join the discussion on Zulip.

  • Project Stable MIR: An effort to define a semi-stable API boundary for the Rust compiler specifically targeting verification usecases.
  • Project Ghost Code: An experiment to define a generic notion of 'ghost code' for use in the compiler which would enable verification tools to more easily encode their invariants.

Upcoming Meetings

January (TBA)

s

Rust verification tools (2021)

This is a list of Rust verification tools with a bias towards ‘formal methods’ tools. An update of Alastair Reid's 2020 list. Tool types are listed in approximate (and subjective!) increasing order of the level of expertise required and approximate increasing order of the level of assurance that they provide. General advise on high quality rust can be found in this book.

Dynamic checking tools

  • Miri for general UB checking (including data race detection, but only on a single execution)

Concurrency checkers

  • Loom, which focuses on exhaustive checking
  • Shuttle, which focuses on randomized checking

Automatic verification tools

Typically relies on a verification harness to generate symbolic input values for the code under test (although those can sometimes be generated from the function argument types). Typically checks assertions, panics, overflows, etc.

Bounded model checking / Static Symbolic Execution

Abstract interpreter ++

Dynamic Symbolic Execution

  • RVT Rust → LLVM → {KLEE,SeaHorn} Plus a DSL for writing verification harnesses based on the property-based testing library proptest
  • Haybale symbolic execution engine for LLVM written in Rust
  • Seer symbolic execution engine based on Miri (not sure it is active)
  • KLEE-Rust KLEE bindings for Rust (inactive for 6 years) Unbounded (?)

Fully Automated Verification

  • RustHorn Automated loop-invariant finding by reduction to CHCs; First proposed the 'prophetic' verification method of Rust

Auto-Active Verification

Midway between automatic and interactive verification. Relies on hints/annotations/etc inserted in source code such as function contracts, loop invariants, data structure invariants, etc.

Interactive verification

Converts Rust to code in an interactive theorem prover which is then verified with human input. This allows one to treat more complex programs.

Very safe subset of rust

  • HacSpec A specification language for cryptographic primitives in Rust. Has backends in F-star, Coq and EasyCrypt. Also has non-cryptographic applications: riot bootloader, the part of the bootloader that selects which image to boot : involves a small hash algorithm and a list traversal. RIOT link

Coq

  • ConCert extracts functional programs in Coq to Rust by using arenas. It originated from smart contract verification.
  • fiat cryptography is a verified compiler for cryptographic primitives in Coq that generates Rust implementations (and other languages). WIP on extending bedrock2 with a rust printer.

Interactive verification of the foundations of Rust

  • RustBelt Semantics close to MIR, focuses on verification of unsafe code,

Interactive verification of core subsets of Rust

  • Oxicide, arxiv link type systems account of Rust's borrow checker, close to surface rust.
  • WASMCert Formalization of the wasm standard
  • VeLLVM Formalization of the LLVM compilation infrastructure

LEAN prover

  • Electrolysis Rust → LEAN translator (no longer active, MSc thesis)

Standardization/Specification

  • HacSpec A specification language for cryptographic primitives in Rust.
  • Ferrocene (previously called Sealed Rust)

Previous Meetings

October Meeting (October 24th, 2022)

Abstract

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.

Video

September Meeting (September 26th, 2022)

Abstract

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.

Video

June Meeting (June 27th, 2022)

Abstract

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.

About the Speaker

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.

Video

May Meeting (May 30th, 2022)

Abstract

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.

Video

April Meeting (April 25th, 2022)

Abstract

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.

Speaker

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.

Video

March Meeting (March 28th, 2022)

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."

https://model-checking.github.io/kani/getting-started.html

February Meeting (February 28th, 2022)

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.

https://www.eventbrite.com/e/creusot-tickets-260072873967

January Meeting (January 31st, 2022)

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.

November Meeting (November 29th, 2021)

Bas Spitters EventBrite.

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.

October Meeting (October 25th, 2021)

Unfortunately this meeting was not record (my bad).

We discussed the specifications for a few simple functions in Prusti and Creusot. There were quite a few things to say on how we handle borrows and the differences between the two tools.

A summary will be posted soon.

The slides are here

Inaugural Meeting (September 20th, 2021)

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.

Youtube recording

Previous events

💖 Code of conduct

Rust code of conduct

All participants in the Rust Formal Methods IG meeting are expected to observe the Rust code of conduct.

  • We are committed to providing a friendly, safe and welcoming environment for all, regardless of level of experience, gender identity and expression, sexual orientation, disability, personal appearance, body size, race, ethnicity, age, religion, nationality, or other similar characteristic.
  • Please avoid using overtly sexual aliases or other nicknames that might detract from a friendly, safe and welcoming environment for all.
  • Please be kind and courteous. There’s no need to be mean or rude.
  • Respect that people have differences of opinion and that every design or implementation choice carries a trade-off and numerous costs. There is seldom a right answer.
  • Please keep unstructured critique to a minimum. If you have solid ideas you want to experiment with, make a fork and see how it works.
  • We will exclude you from interaction if you insult, demean or harass anyone. That is not welcome behavior. We interpret the term “harassment” as including the definition in the Citizen Code of Conduct; if you have any lack of clarity about what might be included in that concept, please read their definition. In particular, we don’t tolerate behavior that excludes people in socially marginalized groups.
  • Private harassment is also unacceptable. No matter who you are, if you feel you have been or are being harassed or made uncomfortable by a community member, please contact xldenis@lri.fr immediately. Whether you’re a regular contributor or a newcomer, we care about making this community a safe place for you and we’ve got your back.
  • Likewise any spamming, trolling, flaming, baiting or other attention-stealing behavior is not welcome.

Rust Formal Methods IG Rules for participation

Please observe the meeting rules for participation.

Moderation contact

Please contact xldenis@lri.fr.