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.

Upcoming Meetings

We hold our meetings on the last monday of every month. Currently, we base ourselve off of European time, with meetings at 7PM. If this causes an issue for you, please leave a message on zulip.

December -- Cancelled

Though we love talking rust verification, its important to take breaks too. Enjoy the end of your year and we'll see you back in 2022!

January Meeting (January 31st, 2022)

Herman Venter will present to us his work on MIRAI, an abstract interpreter for MIR.

Details coming soon!

February Meeting (February 28th, 2022)

We will hear an update on Ferrocene, a project to develop a specification for MIR itself, given by Sabree Blackmon and Florian Gilcher.

Details forthcoming!

March Meeting (March 28th, 2022)

Celina Val and Daniel Schwartz-Narbonne will present their work on RMC (Rust Model Checker), a tool they have been developing at Amazon.

Details forthcoming!

2nd Rust Verification Workshop RustVerify

Co-located with ETAPS 2022, Munich, Sunday, April 03, 2022

Deadline for talk/demo proposals: January 14, 2022 (Friday)

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.

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

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.

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.