diff --git a/coq/CoqOfSolidity/contracts/tutorial/model.v b/coq/CoqOfSolidity/contracts/tutorial/model.v index e75a1e1ae238..c3d7b77f554b 100644 --- a/coq/CoqOfSolidity/contracts/tutorial/model.v +++ b/coq/CoqOfSolidity/contracts/tutorial/model.v @@ -27,7 +27,7 @@ Lemma run_checked_add_t_uint256 codes environment state Proof. unfold safe_add in H_sum. destruct (_ In the rest of the documentation, we assume you have some knowledge in formal verification and in particular in the ๐Ÿ“ [Coq](https://coq.inria.fr/) proof assistant which we use. On a general note, expect it to be _harder_ to fully formally verify a program than to write it. Still, it must be the _simplest way_ to truly ensure your program is correct. @@ -12,14 +12,17 @@ Thanks to `coq-of-solidity`, you can: - Prove that your business rules are always respected. - Run these checks in your CI/CD pipeline to ensure that no bug is introduced in your codebase. -This adds a final layer of security to traditional code audits which are based on human reasoning and testing which only checks a finite amount of cases. +This adds a final layer of security to traditional code audits which are based on human reasoning and testing which only checks a finite amount of cases. This verification even goes beyond other formal verification methods. + +![Verification process](./verification-techniques.png) +_Picture from a [presentation](https://mikedodds.github.io/files/talks/2024-10-09-n-things-I-learned.pdf) of [Galois](https://galois.com/)_ ## Typical workflow Formal verification is expensive โฒ๏ธ, so you should apply it after every other verification (testing, code review, etc.) is done. Here is a typical workflow: 1. You model your smart contract in the Coq proof system. For this step, you manually rewrite your smart contract in idiomatic Coq code. -2. You start expressing and proving a few properties in Coq about your model. For example, that for any possible call the total number of tokens in your contract is constant, if that is a business rule. +2. You start expressing and proving a few properties in Coq about your model. For example, for any possible call the total number of tokens in your contract is constant, if that is a business rule. 3. Once you are confident in the approach, you show that your model is equivalent to the Solidity source code using `coq-of-solidity` and integrate this check into your CI/CD pipeline. At this step, you will probably discover some differences between your model and the source code, like unaccounted integer overflows, and you will have to refine your model to take them into account. 4. When your code evolves, you can update your model and your proofs to ensure that your new code is still correct. `coq-of-solidity` will make sure that your model is still equivalent to your source code ๐Ÿš€. @@ -96,7 +99,7 @@ Lemma run_checked_add_t_uint256 codes environment state It says that for any initial chain `state` and `x` and `y` such that they are in the range of `uint256`, if the addition does not overflow, then the result of the translation is the sum of `x` and `y`, and the chain `state` is unchanged. We could make a similar statement for the overflow case. -Now we need to prove that this statement is true using the tactic language of Coq and some of the custom tactics provided by `coq-of-solidity`. We write the proof using the interactive mode of Coq. To give an idea, here is our proof: +Now, we need to prove that this statement is true using the tactic language of Coq and some of the custom tactics provided by `coq-of-solidity`. We write the proof using the interactive mode of Coq. To give an idea, here is our proof: ```coq Proof. @@ -129,3 +132,5 @@ We recommend only translating the unoptimized version of Yul. That way you are s - Keep the same variable names in the Coq translation as in the source Solidity, helping for the proof process. - Have a diff in the translation that is proportional to the diff in the source code. + +The implementation of `coq-of-solidity` is actually fairly simple and relies on the existing Coq system for the heavy work! ๐Ÿ‹๏ธ diff --git a/coq/docs/src/presentation.md b/coq/docs/src/presentation.md new file mode 100644 index 000000000000..6b3ce8ea74b7 --- /dev/null +++ b/coq/docs/src/presentation.md @@ -0,0 +1,29 @@ +# Presentation + +Here is a ๐ŸŽ๏ธ quick presentation, in simple words, of what `coq-of-solidity` does. + +> With `coq-of-solidity` you make sure that the money stored on your Solidity smart contract cannot be stolen. ๐Ÿ›ก๏ธ + +Every month, millions of dollars ๐Ÿ’ฐ are stolen from smart contracts. This is because a single mistake in the code, even if this is just one line, lets an attacker withdraw all the money and disappear with it! + +Audits are mandatory, but this is a human ๐Ÿง  verifying the code, and mistakes are made. + +> ๐Ÿšจ Even if major smart contracts have all been audited, they are still regularly hacked. + +With `coq-of-solidity`, the computer checks that the reasoning of the auditor is correct: this is like a spell checker for auditors. + +As a result, you can truly be sure that no attack scenario has been forgotten and that your smart contract is truly secure โœ…. + +In addition, when you update the code of your smart contract, you can replay the reasoning for free to make sure your smart contract is still secure on the old part ๐Ÿ˜Ž . This _saves on auditing costs_. + +## Why us? + +Verifying reasoning about code is called ๐Ÿ”Ž _formal verification_. This is a complex technique ๐Ÿงช and very few companies have developed a tool to do this for Solidity. In addition, `coq-of-solidity` is the only one with [Clear](https://github.com/NethermindEth/Clear) that can express any possible reasoning/property on your code. This is thanks to the use of an ๐Ÿ“ interactive theorem prover on the backend. + +At [๐ŸŒฒ Formal Land](https://formal.land/), where we developed `coq-of-solidity`, we are one of the leading teams applying formal verification to large-scale programs. We have developed two other formal verification tools, with [coq-of-rust](https://github.com/formal-land/coq-of-rust) for ๐Ÿฆ€ Rust and [coq-of-ocaml](https://github.com/formal-land/coq-of-ocaml) for ๐Ÿซ OCaml. Read more about what we do on our [๐Ÿ“– blog](https://formal.land/blog). + +## How much? ๐Ÿ’ธ + +For a large smart contract (5,000 lines of Solidity), consider a price of **$50,000** for a formal verification of a _model_ of the code, and **$100,000** for a verification at the level of the _source code_ (more precise). So, this is competitive with traditional audits. + +[๐Ÿ’Œ Contact us](mailto:contact@formal.land) for an evaluation! diff --git a/coq/docs/src/verification-techniques.png b/coq/docs/src/verification-techniques.png new file mode 100644 index 000000000000..ed3a768edcb6 Binary files /dev/null and b/coq/docs/src/verification-techniques.png differ