In this blog post, we present our project to formally verify the implementation of the type checker for smart contracts of the 💧 Sui blockchain. The Sui blockchain uses the Move language to express smart contracts. This language is implemented in 🦀 Rust and compiles down to the Move bytecode that is loaded in memory when executing the smart contracts.
We will formally verify the part that checks that the bytecode is well-typed, so that when a smart contract is executed it cannot encounter critical errors. The type checker itself is also written in Rust, and we will verify it using the proof assistant Coq 🐓 and our tool coq-of-rust that translates Rust programs to Coq.
To formally verify your Rust code and ensure it contains no bugs or vulnerabilities, contact us at 📧contact@formal.land.
The cost is €10 per line of Rust code (excluding comments) and €20 per line for concurrent code.
Plan
The plan for this project is as follows:
- Write simulations 🧮 of the Rust code we want to verify in Coq, namely the type checker and the interpreter of bytecode. The simulations are functions that are equivalent to the ones in the original Rust program, but written in a style that is more amenable to formal verification. The changes can be:
- very simple, for example renaming variables to avoid name collisions in Coq,
- more involved like solving the trait instances or replacing Rust references with purely functional code, or
- specific to the project, like reversing the order of the bytecode's stack to simplify the proofs.
- Test these simulations 🔍 to show they behave like the original Rust code on examples covering all the opcodes of the Move bytecode.
- Prove the equivalence 🟰 between the Coq simulations and the Rust code as translated to Coq by
coq-of-rust. This part will give more precise results than the tests, as it will cover all possible inputs and states of the program. The complexity of this part is to go through all the details that exist in the Rust code, like the use of references to manipulate the memory, the macros after expansion, and the parts of the Rust standard library that the code depends on. - Prove that the type checker is correct 🛡️ in Coq. The main properties we want to check are:
- the interpreter preserves the well-typedness of the code as it steps through the opcodes,
- when a program is accepted by the type checker, the interpreter will not fail at runtime with a type error.
What is done
For now, we have written a simulation for the type checker in CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v. We are now:
- adding tests to compare this simulation with the original Rust code,
- writing the simulation for the interpreter of the Move bytecode.
In the following blog posts, we will describe how we structured the simulations and how we are testing or verifying them.
This project is kindly founded by the Sui Foundation which we thank for their trust and support.