Noir is a Domain Specific Language for SNARK proving systems. With coq-of-noir, we provide an affordable way to formally verify smart contracts written in Noir. We rely on the well-known proof assistant Coq for the verification work as well proof techniques developed for coq-of-rust and coq-of-solidity.
Follow what we do in our CI file coq.yml. Sorry for not having the time to provide more explanations!
The following steps work:
- A generated translation of the
base64library of Noir to Coq in a code that compiles; we should thus support a large part of the Noir language. - Semantics rules to reason on code like the above together with a proof strategy. This should already cover most of the Noir language.
- A formally verified functional specification of one of the functions with a loop from the
base64library, exercising mutations and array access. We consider this to be our main test to see thatcoq-of-noircan work on non-trivial examples.
Note that the proof process is still very verbose, and this tool is still a work in progress. Contact us at [email protected] or by direct message on our X account if you are interested.
The goal is to enable each team developing critical applications (meaning handling user money) to verify the correctness of their code with the higest degree of certainty thanks to formal verification.
For those who do not know, formal verification is a technique to verify software for 100% of possible execution parameters. This means that the code cannot have bugs or vulnerabilities! Initially applied to software from the spacial/defense industry, the key idea is to mathematically reason about the code to talk about possibly infinitely many possible cases, and to verify all the reasoning by a dedicated tool called a proof checker, in our case 🐓 Coq.
In this repository, we provide a command to automatically translate a Noir program to a representation in Coq. We translate the code after the monomorphisation phase of the Noir compiler so that we do not have to deal with polymorphism or type classes. Instead, one can reconstruct this organization of the code on the Coq side in a refinement step, if needed.
This translation is a shallow embedding optimized to write specifications and proofs about the code. As we erase all the types during the translation to keep only the values, we recommend doing a first proof step that reconstructs these types. This first proof step is also an opportunity to explicit the structure of the global state.
Our initial target is to verify a part of the base64, which uses field arithmetic for optimizations. It also includes many loops, which are generally non-trivial to fully verify with formal verification.
If you have a Noir project that you want to formally verify, either start using coq-of-noir or contact us!
Here are some blog posts featuring this tool:
coq-of-noir is free and open source. It is distributed under a dual license. (MIT/APACHE) The translation phase is based on the code of the Noir compiler to maximize code reuse.