Awesome

<img src="logo.png" alt= "logo" width="120px" height="120px" style="vertical-align: middle;"> <span style="vertical-align: middle;">coq-of-rust</span>

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

Even if Rust's type system prevents many mistakes, including memory errors, the code is still not immune to vulnerabilities, such as unexpected panics or wrongly implemented business rules.

The way to go further is to mathematically prove that it is bug-free: this is named "formal verification" and what coq-of-rust proposes! This is the only way to ensure your code contains no bugs or vulnerabilities, even against state-level actors 🧚.

The development of coq-of-rust was mainly funded by the Aleph Zero Foundation. We thank them for their support!

Table of Contents

• Example
• Rationale
• Prerequisites
• Installation and User Guide
• Features
• Contact
• Alternative Projects
• Contributing

Example

At the heart of coq-of-rust is the translation of Rust programs to the proof system Coq 🐓. Once some Rust code is translated to Coq, it can then be verified using standard proof techniques.

Here is an example of a Rust function:

fn add_one(x: u32) -> u32 {
    x + 1
}

Running coq-of-rust, it translates in Coq to:

Definition add_one (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ x ] =>
    ltac:(M.monadic
      (let x := M.alloc (| x |) in
      BinOp.Panic.add (| M.read (| x |), Value.Integer Integer.U32 1 |)))
  | _, _ => M.impossible
  end.

Functions such as BinOp.Panic.add are part of the standard library for Rust in Coq that we provide. We can then express and verify specifications on the code in Coq.

Workflow

Here is the typical workflow of usage for coq-of-rust:

graph TB
    R[Rust code 🦀] -- coq-of-rust --> T[Translated code 🐓]
    T -- name resolutions --> L[Linked code 🐓]
    L -- refinement --> S[Simulations 🐓]
    S --> P
    SP[Specifications 🐓] --> P[Proofs 🐓]
    P -.-> X[100% reliable code! 🦄]

We start by generating an automatic translation of the Rust we verify to Coq code with coq-of-rust. The translation is originally verbose. We go through two semi-automated refinement steps, links and simulations, that gradually make the code more amenable to formal verification.

Finally, we write the specifications and prove that our Rust program fulfills them with any possible user input 🔥.

Examples of typical specifications are:

• The code cannot panic.
• This clever data structure is equivalent to its naive version, except for the execution time.
• This new release, which introduces new endpoints and does a lot of refactoring, is fully backward-compatible with the previous version.
• Data invariants are properly preserved.
• The storage system is sound, as what goes in goes out (this generally amounts to state that the serialization/deserialization functions are inverse).
• The implementation behaves as a special case of what the whitepaper describes once formally expressed.

With that in hand, you can virtually reduce your bugs and vulnerabilities to zero 🦸!

Rationale

Formal verification allows the prevention of all bugs in critical software.

The type system of Rust already offers strong guarantees to avoid bugs that exist in C or Python. We still need to write tests to verify the business rules or the absence of panic. Testing is incomplete as it cannot cover all execution cases.

With formal verification, we cover all cases (code 100% bug-free!). We replace the tests with mathematical reasoning on code. You can view it as an extension of the type system but without restrictions on the expressivity.

The tool coq-of-rust translates Rust programs to the battle-tested formal verification system Coq to make Rust programs 100% safe 🚀.

Prerequisites

• Rust
• Coq (see coq-of-rust.opam)

Installation and User Guide

The build tutorial provides detailed instructions on building and installing coq-of-rust, while the user tutorial provides an introduction to the coq-of-rust command line interface and the list of supported options.

Language features

The translation works at the level of the THIR intermediate representation of Rust.

We support 99% of the Rust examples from the Rust Book by Examples. This includes:

• basic control structures (like if and match)
• loops (while and for)
• references and mutability (& and &mut)
• closures
• panics
• user types (with struct and enum)
• the definition of traits
• the implementation keyword impl for traits or user types

Contact

For formal verification services on your Rust code base, contact us at contact@formal.land. Formal verification can apply to smart contracts, database engines, or any critical Rust project. This provides the highest confidence level in the absence of bugs compared to other techniques, such as manual reviews or testing.

Alternative Projects

Here are other projects working on formal verification for Rust:

• Aeneas: Translation from MIR to purely functional Coq/F* code. Automatically put the code in a functional form. See their paper Aeneas: Rust verification by functional translation.
• Hacspec v2: Translation from THIR to Coq/F* code
• Creusot: Translation from MIR to Why3 (and then SMT solvers)
• Verus: Automatic verification for Rust with annotations
• Kani: Model-checking with CBMC

Contributing

This is all open-source software.

Open some pull requests or issues to contribute to this project. All contributions are welcome! This project is open-source under license AGPL for the Rust code (the translator) and MIT for the Coq libraries. There is a bit of code taken from the Creusot project to make the Cargo command coq-of-rust and run the translation in the same context as Cargo.