diff --git a/certora/README.md b/certora/README.md index 12f4a44..301359a 100644 --- a/certora/README.md +++ b/certora/README.md @@ -7,20 +7,23 @@ There are two configurations: ## Run From the Command Line -To run the checks from the command line, first install the Python SDK: -`pip install certora-cli` +Follow this guide to install the prover and its dependencies: +[Installation Guide](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html) -Set your Certora Key: -`export CERTORAKEY=` - -Then run from this directory: +Once installations are set, run from this directory: `certoraRun ./certora/confs/ghost.conf` + +## Recommended IDE + +We recommended using VSCode with the following extension: +[Certora Verification Language LSP](https://marketplace.visualstudio.com/items?itemName=Certora.evmspec-lsp) +This extension is found in the VSCode extensions/marketplace. It provides syntactic support for the Certora Verification Language (CVL) - the language in which we will be writing specifications. ## Files Folder `specs` contains the specification files: 1. `ghost.spec` contains basic rules that are not dependent on any interface. -1. `moreExmaplesERC20.spec` contains basic examples including ghost, hooks, and multi-contract features. +2. `moreExmaplesERC20.spec` contains basic examples including ghost, hooks, and multi-contract features. Folder `confs` contains the configuration files for running the Certora Prover: 1. File `ghost.conf` for running `ghost.spec` on `ghost.sol` file. @@ -28,7 +31,7 @@ This configuration is suitable for a standalone project, containing: * external calls are assumed to be non-state changing and returning random value on each call. * loops are unrolled three times. * calls to fallbacks are assumed to be side-effect-free and only update the native balance. - 1. File `ghostWithERC20s.conf` running `moreExmaplesERC20.spec` on `ghost.sol` with additional ERC20-related contracts. +2. File `ghostWithERC20s.conf` running `moreExmaplesERC20.spec` on `ghost.sol` with additional ERC20-related contracts. This demonstrates how to setup a project with multi-contract diff --git a/certora/confs/ghost.conf b/certora/confs/ghost.conf index 0dd9302..ffc5f99 100644 --- a/certora/confs/ghost.conf +++ b/certora/confs/ghost.conf @@ -1,18 +1,22 @@ -// A default configuration for a standalone contract +# A default configuration for a contract using ERC20s { - // list of files that are part of the system +# list of files that are part of the system "files": [ "src/contracts/Ghost.sol" ], - // main contract to verify ghost and spec file +# main contract to verify (Ghost):spec file (ghost) "verify": "Ghost:certora/specs/ghost.spec", - // check the spec +# apply very important sanity checks that should always be run before finishing a verification +# docs: https://docs.certora.com/en/latest/docs/prover/checking/sanity.html?highlight=rule%20sanity "rule_sanity" :"basic", - // assume 3 unroling of loops is enought +# assume 3 unrolling of loops, i.e. every loop will run for at most 3 iterations. 3 is usually enough in most cases. +# this in turn will impose requirements on the length of the array (etc.) that a loop is iterating on (the stop condition of the loop) +# docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html#loop-iter "loop_iter" : "3", +# docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html#optimistic-loop "optimistic_loop" : true, "prover_args": [ - // assume calls to fallback are to EOAs (e.g., no code, only balance updated) + # assume calls to fallback are to EOAs (e.g., no code, only balance updated) " -optimisticFallback true" ], "msg": "Ghost template file" diff --git a/certora/confs/ghostWithERC20s.conf b/certora/confs/ghostWithERC20s.conf index cb7d774..141e777 100644 --- a/certora/confs/ghostWithERC20s.conf +++ b/certora/confs/ghostWithERC20s.conf @@ -1,20 +1,24 @@ -// A default configuration for a contract using ERC20s +# A default configuration for a contract using ERC20s { - // list of files that are part of the system +# list of files that are part of the system "files": [ "src/contracts/Ghost.sol", "certora/helpers/ERC20Helper.sol", "certora/helpers/SimpleERC20.sol" ], - // main contract to verify ghost, spec file +# main contract to verify (Ghost):spec file (moreExamplesERC20) "verify": "Ghost:certora/specs/moreExamplesERC20.spec", - // check the spec +# apply very important sanity checks that should always be run before finishing a verification +# docs: https://docs.certora.com/en/latest/docs/prover/checking/sanity.html?highlight=rule%20sanity "rule_sanity" :"basic", - // assume 3 unroling of loops is enought +# assume 3 unrolling of loops, i.e. every loop will run for at most 3 iterations. 3 is usually enough in most cases. +# this in turn will impose requirements on the length of the array (etc.) that a loop is iterating on (the stop condition of the loop) +# docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html#loop-iter "loop_iter" : "3", +# docs: https://docs.certora.com/en/latest/docs/prover/cli/options.html#optimistic-loop "optimistic_loop" : true, "prover_args": [ - // assume calls to fallback are to EOAs (e.g., no code, only balance updated) + # assume calls to fallback are to EOAs (e.g., no code, only balance updated) " -optimisticFallback true" ], "msg": "Ghost with ERC20 template file" diff --git a/certora/specs/ghost.spec b/certora/specs/ghost.spec index 969351c..dc43c07 100644 --- a/certora/specs/ghost.spec +++ b/certora/specs/ghost.spec @@ -8,7 +8,7 @@ See https://docs.certora.com for a complete guide. /* Declaration of methods that are used in the rules. `envfree` indicates that - the method is not dependent on the environment (`msg.value`, `msg.sender`). + the method is not dependent on the environment (`msg.value`, `msg.sender`, `block.timestamp`). Methods that are not declared here are assumed to be dependent on the environment. */ @@ -51,21 +51,21 @@ rule noRevert(method f) filtered {f -> nonReveritngFunction(f) } @dev This property is implemented as a relational property - it compares two different executions on the same state. **/ rule simpleFrontRunning(method f, method g) - /// usually a heavy rule, use filtering to decide on which this property should hole + /// usually a heavy rule, use filtering to decide which functions this property should check /* filtered { f-> !f.isView, g-> !g.isView } */ { env e1; - calldataarg arg; + calldataarg args1; - storage initialStorage = lastStorage; - f(e1, arg); + storage initialStorage = lastStorage; // creating a storage snapshot for later use + f(e1, args1); env e2; - calldataarg arg2; + calldataarg args2; require e2.msg.sender != e1.msg.sender; - g(e2, arg2) at initialStorage; //roll back to state before calling f + g(e2, args2) at initialStorage; // first rolling back the state to the storage snapshot, then calls a function g - f@withrevert(e1, arg); + f@withrevert(e1, args1); // f is called on the state snapshot + g bool succeeded = !lastReverted; assert succeeded, "should be called also if frontrunned"; @@ -81,17 +81,17 @@ rule simpleFrontRunning(method f, method g) rule privilegedOperation(method f, address privileged) { env e1; - calldataarg arg; + calldataarg args1; require e1.msg.sender == privileged; storage initialStorage = lastStorage; - f@withrevert(e1, arg); // privileged succeeds executing candidate privileged operation. + f@withrevert(e1, args1); // privileged succeeds executing candidate privileged operation. bool firstSucceeded = !lastReverted; env e2; - calldataarg arg2; + calldataarg args2; require e2.msg.sender != privileged; - f@withrevert(e2, arg2) at initialStorage; // unprivileged + f@withrevert(e2, args2) at initialStorage; // unprivileged bool secondSucceeded = !lastReverted; satisfy (firstSucceeded && secondSucceeded), "function is not privileged"; @@ -99,9 +99,9 @@ rule privilegedOperation(method f, address privileged) /** - @title This rule check with ether is sent out. + @title This rule check if ether is sent out. @dev nativeBalances[u] is u.balance in solidity - @dev currentContract is the main contract under verification + @dev currentContract is the main contract under verification */ rule decreaseInSystemEth(method f) { diff --git a/certora/specs/moreExamplesERC20.spec b/certora/specs/moreExamplesERC20.spec index f48a8d2..765e896 100644 --- a/certora/specs/moreExamplesERC20.spec +++ b/certora/specs/moreExamplesERC20.spec @@ -16,6 +16,8 @@ using SimpleERC20 as simpleERC20; // Declaration of erc20 functions methods { // When there is an unresolved call it will check all implementaions found in the list of contracts + // See docs for more information on dispatcher summary: + // https://docs.certora.com/en/latest/docs/cvl/methods.html?highlight=dispatcher#dispatcher-summaries function _.name() external => DISPATCHER(true); function _.symbol() external => DISPATCHER(true); function _.decimals() external => DISPATCHER(true); @@ -34,9 +36,10 @@ methods { /** - @title decrease in system's erc20 balance - @dev calls another contract + @title decrease in system's erc20 balance + @dev calls another contract @dev example for filtering and checking only on methods from the main contract + @notice method f must be defined in the rule signature to be recognized by the filter */ rule decreaseInERC20(method f, address token) filtered { f-> f.contract == currentContract } { @@ -53,7 +56,7 @@ rule decreaseInERC20(method f, address token) filtered { f-> f.contract == curre } /** - @title sum of erc20 balances if totalSupply + @title sum of erc20 balances is totalSupply @dev usign a ghost variable and hooks to track changes to _balances **/ ghost mathint simpleERC20_sumOfBalances {