🦀 coq-of-rust

note

This project was funded by the Aleph Zero Foundation.

Our Rust analyzer coq-of-rust provides:

• The highest level of security 🛡️ for your Rust programs by checking all possible user inputs 🔍 (formal verification).
• A verification of any kinds of security properties 👮 (interactive prover).
• Reusable proofs 🔁 you can re-run as the code evolves, eliminating the need of costly manual code audits.

This is better than testing that might miss some edge cases. In fact, we always find all the bugs!¹

Service

We apply coq-of-rust to formally verify your Rust programs, writing the specifications and proofs of correctness. See our project for Sui as a reference.

This is the highest level of security 💫 and this is accessible now. This is the strongest way to protect your code even against state-level attackers 🦸 since this is maths-backed, like encryption protects your data.

🦸 Contact us! 

How it works

It converts Rust programs to the 🐓 Rocq proof system. You access the source on GitHub. coq-of-rust generates a shallow embedding of Rust into Rocq. We run the translation from the THIR level of the Rust compiler. The generated Rocq code is more verbose than the source Rust as we explicit all the low-level details, such as the sequencing of effects or the implicit borrowing/dereferencing.

Example

coq-of-rust translates the Rust code from Revm:

pub const fn limit(&self) -> u64 {
    self.limit
}

to the Rocq code:

(* Generated by coq-of-rust *)
Definition limit (ε : list Value.t) (τ : list Ty.t) (α : list Value.t) : M :=
  match ε, τ, α with
  | [], [], [ self ] =>
    ltac:(M.monadic
      (let self := M.alloc (| self |) in
      M.read (|
        M.SubPointer.get_struct_record_field (|
          M.deref (| M.read (| self |) |),
          "revm_interpreter::gas::Gas",
          "limit"
        |)
      |)))
  | _, _, _ => M.impossible "wrong number of arguments"
  end.

We can see that the generated code if more verbose. The good news is that a large subset of Rust can be translated, including most of the standard library (alloc and core). The difficulty is in reasoning about such translated code. We work hard to develop automations and strategies to make this process easier.

Getting started

To install coq-of-rust, you need to clone the GitHub repository and to have a working installation of Rust. Then, from the root folder of the project, you can run:

cargo install --path lib/

It will install the additional cargo coq-of-rust command. Then to translate in Rocq the project of your choice:

cd my_rust_project/
# You need to copy the rust-toolchain file to force the right version of Rust
cp ../coq-of-rust/rust-toolchain ./
cargo coq-of-rust

This should generate a bunch of .v Rocq files, with one file per corresponding Rust file. To compile them, the simplest is to copy them in the CoqOfRust/ folder of the coq-of-rust project and to run from there:

# Install the Rocq dependencies
opam repo add coq-released https://coq.inria.fr/opam/released
opam install . --deps-only
# Compile the whole project (it takes time)
make -j4 # 4 is your number of cores

For robustness, the files are not dependent for compilation, so that one translation failure does not block you.

Workflow

To formally verify a Rust project using coq-of-rust we work as follows:

1. translate the Rust code to Rocq using coq-of-rust
2. define the memory of the program (how the values will be allocated)
3. write simulation functions for each function of the Rust code, to give a simpler and more functional definition of the code
4. verify that these simulations are equivalent to the source code
5. prove properties over these simulations

As some of the work is very verbose and repetitive, such as the definition of the simulation functions, but thankfully generative AI tools such as Github Copilot are better and better at code generation.

Footnotes

1. What does this mean? We assume given a formal specification of the code that mathematically describes what is supposed to be a bug and what is supposed to be a feature. From the there, the Rocq proof system that we use can check that the code is correct with respect to this specification for all possible user inputs. The result is a mathematical proof checked by the computer. Almost any programs can be verified except the proof checker itself, as it would be a paradox. See this paper to see how Rocq was used to make the only C compiler without bugs (well, except on the non formally verified parts). ↩