diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 0000000..f1a2ec7 --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,102 @@ +# A workflow file for running Certora verification through GitHub actions. +# Find results for each push in the "Actions" tab on the GitHub website. +name: Certora verification + +on: + push: {} + pull_request: {} + workflow_dispatch: {} + +jobs: + verify: + runs-on: ubuntu-latest + steps: + # check out the current version + - uses: actions/checkout@v2 + + # install Certora dependencies and CLI + - name: Install python + uses: actions/setup-python@v2 + with: + python-version: '3.10' + # cache: 'pip' + - name: Install certora + run: pip3 install certora-cli + + # the following is only necessary if your project depends on contracts + # installed using yarn + # - name: Install yarn + # uses: actions/setup-node@v3 + # with: + # node-version: 16 + # cache: 'yarn' + # - name: Install dependencies + # run: yarn + + # Install the appropriate versions of solc + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.21/solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.21 + chmod +x /usr/local/bin/solc8.21 + + wget https://github.com/ethereum/solidity/releases/download/v0.8.17/solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.17 + chmod +x /usr/local/bin/solc8.17 + + # Do the actual verification. The `run` field could be simply + # + # certoraRun certora/conf/${{ matrix.params }} + # + # but we do a little extra work to get the commit messages into the + # `--msg` argument to `certoraRun` + # + # Here ${{ matrix.params }} gets replaced with each of the parameters + # listed in the `params` section below. + - name: Verify ${{ matrix.params.name }} + run: > + message="$(git log -n 1 --pretty=format:'CI ${{matrix.params.name}} %h .... %s')"; + certoraRun \ + certora/confs/${{ matrix.params.command }} \ + --msg "$(echo $message | sed 's/[^a-zA-Z0-9., _-]/ /g')" + env: + # For this to work, you must set your CERTORAKEY secret on the GitHub + # website (settings > secrets > actions > new repository secret) + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + # The following two steps save the output json as a GitHub artifact. + # This can be useful for automation that collects the output. + - name: Download output json + if: always() + run: > + outputLink=$(sed 's/zipOutput/output/g' .zip-output-url.txt | sed 's/?/\/output.json?/g'); + curl -L -b "certoraKey=$CERTORAKEY;" ${outputLink} --output output.json || true; + touch output.json; + + - name: Archive output json + if: always() + uses: actions/upload-artifact@v3 + with: + name: output for ${{ matrix.params.name }} + path: output.json + + strategy: + fail-fast: false + matrix: + params: + # each of these commands is passed to the "Verify rule" step above, + # which runs certoraRun on certora/conf/ + # + # Note that each of these lines will appear as a separate run on + # prover.certora.com + # + # It is often helpful to split up by rule or even by method for a + # parametric rule, although it is certainly possible to run everything + # at once by not passing the `--rule` or `--method` options + #- {name: transferSpec, command: 'ERC20.conf --rule transferSpec'} + #- {name: generalRulesOnERC20, command: 'generalRules_ERC20.conf --debug'} + #- {name: generalRulesOnVAULT, command: 'generalRules_VAULT.conf --debug'} + - {name: ghostTemplate, command: 'ghost.conf' } + - {name: ghostWithERC20, command: 'ghostWithERC20s.conf' } + + diff --git a/.gitignore b/.gitignore index d95519b..d54885a 100644 --- a/.gitignore +++ b/.gitignore @@ -15,3 +15,6 @@ node_modules # ignore foundry deploy artifacts broadcast/ + +#certora temp files +.certora_internal \ No newline at end of file diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 0000000..21be40b --- /dev/null +++ b/certora/README.md @@ -0,0 +1,57 @@ +# Certora + +This folder provides a fully functional skeleton for integrating with Certora. +There are two configurations: + + + +## Run From the Command Line + +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) + +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 + +The folder `specs` contains the specification files: +1. `ghost.spec` contains basic rules that are not dependent on any interface. +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. +This configuration is suitable for a standalone project, containing: + * external calls are assumed to be non-state changing and return random values on each call. + * loops are unrolled three times. + * calls to fallbacks are assumed to be side-effect-free and only update the native balance. +2. File `ghostWithERC20s.conf` running `moreExmaplesERC20.spec` on `ghost.sol` with additional ERC20-related contracts. +This demonstrates how to set up a project with multi-contract + + +## CI Integration + +This repository contains a Certora setup in GitHub actions. +You will need to provide your secret `CERTORAKEY` to GitHub. + + + +## Mutation Testing +The Certora Prover is integrated with Gambit, an open-source Solidity mutation testing tool. Mutation testing can give you an estimate of the coverage of your verification. + +To run the mutation test from this directory, run: + `certoraMutate --prover_conf certora/confs/ghost.conf --mutation_conf certora/confs/mutation.mconf`. + However, this does not generate any mutates as 'ghost.sol' is too small. + `certoraMutate --prover_conf certora/confs/ghostWithERC20s.conf --mutation_conf certora/confs/mutationWithERC20.mconf ` mutates `SimpleERC20.sol`. + + +## CVL Examples and Docs +See more CVL specification general examples +and Documenation. +More mutation configurations can be found in the [certoraInit repo](https://github.com/Certora/CertoraInit"). diff --git a/certora/confs/ghost.conf b/certora/confs/ghost.conf new file mode 100644 index 0000000..db74752 --- /dev/null +++ b/certora/confs/ghost.conf @@ -0,0 +1,23 @@ +{ +// list of files that are part of the system + "files": [ + "src/contracts/Ghost.sol" + ], + "solc": "solc8.21", +// matching the main contract to verify and its spec file - Ghost.sol:ghost.spec + "verify": "Ghost:certora/specs/ghost.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 + "rule_sanity" :"basic", +// constraint loops to three unrolls, i.e. every loop will run for at most 3 iterations. 3 is usually enough to cover all interesting 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) + " -optimisticFallback true" + ], + "msg": "Ghost template file" +} \ No newline at end of file diff --git a/certora/confs/ghostWithERC20s.conf b/certora/confs/ghostWithERC20s.conf new file mode 100644 index 0000000..1906ef8 --- /dev/null +++ b/certora/confs/ghostWithERC20s.conf @@ -0,0 +1,26 @@ + // A default configuration for a contract using ERC20s +{ +// list of files that are a part of the system + "files": [ + "src/contracts/Ghost.sol", + "certora/helpers/ERC20Helper.sol", + "certora/helpers/SimpleERC20.sol" + ], + "solc": "solc8.17", +// matching the main contract to verify and its spec file - Ghost.sol:ghost.spec + "verify": "Ghost:certora/specs/moreExamplesERC20.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 + "rule_sanity" :"basic", +// constraint loops to three unrolls, i.e. every loop will run for at most 3 iterations. 3 is usually enough to cover all interesting 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) + " -optimisticFallback true" + ], + "msg": "Ghost with ERC20 template file" +} diff --git a/certora/confs/mutation.mconf b/certora/confs/mutation.mconf new file mode 100644 index 0000000..a09b973 --- /dev/null +++ b/certora/confs/mutation.mconf @@ -0,0 +1,9 @@ +{ + "gambit": [ + { + "filename" : "../../src/contracts/Ghost.sol", + "num_mutants": 1 + } + ], + "msg": "basic mutation configuration" +} \ No newline at end of file diff --git a/certora/confs/mutationWithERC20.mconf b/certora/confs/mutationWithERC20.mconf new file mode 100644 index 0000000..2dd30f5 --- /dev/null +++ b/certora/confs/mutationWithERC20.mconf @@ -0,0 +1,9 @@ +{ + "gambit": [ + { + "filename" : "../helpers/SimpleERC20.sol", + "num_mutants": 5 + } + ], + "msg": "basic mutation configuration" +} \ No newline at end of file diff --git a/certora/helpers/ERC20Helper.sol b/certora/helpers/ERC20Helper.sol new file mode 100644 index 0000000..719ee75 --- /dev/null +++ b/certora/helpers/ERC20Helper.sol @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + + +//probably repalce with an import to the selected library +interface IERC20 { + + function balanceOf(address account) external view returns (uint256); +} + +contract ERC20Helper { + function tokenBalanceOf(address token, address user) public view returns (uint256) { + return IERC20(token).balanceOf(user); + } +} \ No newline at end of file diff --git a/certora/helpers/SimpleERC20.sol b/certora/helpers/SimpleERC20.sol new file mode 100644 index 0000000..136973a --- /dev/null +++ b/certora/helpers/SimpleERC20.sol @@ -0,0 +1,45 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + +//a symbolic erc20 for verification + + +contract SimpleERC20 { + + uint256 private _totalSupply; + mapping(address => uint256) private _balance; + mapping(address => mapping(address => uint256)) private _allowance; + + function totalSupply() public view returns (uint256) { + return _totalSupply; + } + + function balanceOf(address account) public view returns (uint256) { + return _balance[account]; + } + + function allowance(address owner, address spender) public view returns (uint256) { + return _allowance[owner][spender]; + } + + function approve(address spender, uint256 amount) external returns (bool) { + _allowance[msg.sender][spender] = amount; + return true; + } + + function transfer(address recipient, uint256 amount) external returns (bool) { + _balance[msg.sender] -= amount; + _balance[recipient] += amount; + + return true; + } + + function transferFrom(address from,address recipient,uint256 amount) external returns (bool) { + if (_allowance[from][msg.sender] != type(uint256).max) { + _allowance[from][msg.sender] -= amount;} + _balance[from] -= amount; + _balance[recipient] += amount; + + return true; + } +} diff --git a/certora/specs/ghost.spec b/certora/specs/ghost.spec new file mode 100644 index 0000000..fd76e84 --- /dev/null +++ b/certora/specs/ghost.spec @@ -0,0 +1,123 @@ +/*** + +Spec for the Certora Verification Language. +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`, `block.timestamp`). + Methods that are not declared here are assumed to be dependent on the + environment. +*/ +methods { + // function in the main contract under verification + function boo() external returns (string memory) envfree; +} + +/** + @title Find and show a path for each method. + @dev This is a parametric rule - it checks all public/external methods of the contracts listed under `files` in the configuration file. +**/ +rule reachability(method f) +{ + env e; + calldataarg args; + f(e,args); //takes into account only non reveting cases + satisfy true, "function has a non-reverting path"; +} + +/** + @title Define and check functions that should never revert + @dev use f.selector to state which functions should not revert,e.g.f.selector == sig:balanceOf(address).selector +**/ +definition nonReveritngFunction(method f) returns bool = true; + +rule noRevert(method f) filtered {f -> nonReveritngFunction(f) } +{ + env e; + calldataarg arg; + // consider auto filtering for non-payable functions by using !f.selector.isPayable + require e.msg.value == 0; + f@withrevert(e, arg); + assert !lastReverted, "method should never revert"; +} + + +/** + @title Checks if a function can be frontrun + @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 which functions this property should check + /* filtered { f-> !f.isView, g-> !g.isView } */ +{ + env e1; + calldataarg args1; + + storage initialStorage = lastStorage; // creating a storage snapshot for later use + f(e1, args1); + + env e2; + calldataarg args2; + require e2.msg.sender != e1.msg.sender; + g(e2, args2) at initialStorage; // first rolling back the state to the storage snapshot, then calls a function g + + f@withrevert(e1, args1); // f is called on the state snapshot + g + bool succeeded = !lastReverted; + + assert succeeded, "should be called also if frontrunned"; +} + + +/** + @title This rule finds which functions are privileged. + @notice A function is privileged if there is only one address that can call it. + @dev by checking which functions can be called by two different users. +*/ + +rule privilegedOperation(method f, address privileged) +{ + env e1; + calldataarg args1; + require e1.msg.sender == privileged; + + storage initialStorage = lastStorage; + f@withrevert(e1, args1); // privileged succeeds executing candidate privileged operation. + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg args2; + require e2.msg.sender != privileged; + f@withrevert(e2, args2) at initialStorage; // unprivileged + bool secondSucceeded = !lastReverted; + + satisfy (firstSucceeded && secondSucceeded), "function is not privileged"; +} + + +/** + @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 +*/ +rule decreaseInSystemEth(method f) { + + uint256 before = nativeBalances[currentContract]; + + env e; + calldataarg arg; + f(e, arg); + + uint256 after = nativeBalances[currentContract]; + + assert after >= before || false, "function sent eth out of the contract's balance"; /* replace false with cases where eth can decrease */ +} + + +// just an example of the structure of an invariant +// learn more about invariants in our docs: https://docs.certora.com/en/latest/docs/cvl/invariants.html +invariant dummy() + nativeBalances[currentContract] >= 0; diff --git a/certora/specs/moreExamplesERC20.spec b/certora/specs/moreExamplesERC20.spec new file mode 100644 index 0000000..f980944 --- /dev/null +++ b/certora/specs/moreExamplesERC20.spec @@ -0,0 +1,75 @@ +/*** + +Spec for the Certora Verification Language. +See https://docs.certora.com for a complete guide. + +run this file with ghostWithERc20s.conf: + +certoraRun certora\confs\ghostWithERc20s.conf + +***/ + +using ERC20Helper as _erc20Helper; // a variable that is the address of ERC20Helper + +using SimpleERC20 as simpleERC20; + +// Declaration of erc20 functions +methods { + // When there is an unresolved call it will check all implementations found in the list of contracts + // See docs for more information on dispatcher summaries: + // https://docs.certora.com/en/latest/docs/cvl/methods.html + function _.name() external => DISPATCHER(true); + function _.symbol() external => DISPATCHER(true); + function _.decimals() external => DISPATCHER(true); + function _.totalSupply() external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.allowance(address,address) external => DISPATCHER(true); + function _.approve(address,uint256) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + function _.transferFrom(address,address,uint256) external => DISPATCHER(true); + + // functions in other contracts + function ERC20Helper.tokenBalanceOf(address token, address user) external returns (uint256) envfree; + + function simpleERC20.totalSupply() external returns (uint256) envfree; +} + + +/** + @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 } { + + uint256 before = _erc20Helper.tokenBalanceOf(token, currentContract); + + env e; + calldataarg arg; + f(e, arg); + + uint256 after = _erc20Helper.tokenBalanceOf(token, currentContract); + + assert after >= before || false, "function decreased the contract's ERC balance"; // replace false with cases where the token can decrease + +} + +/** + @title sum of erc20 balances is totalSupply + @dev using a ghost variable and hooks to track changes to _balances + @notice to learn more about ghosts you can read the docs: + @notice https://docs.certora.com/en/latest/docs/confluence/anatomy/ghostfunctions.html#initial-axioms-for-uninterpreted-functions +**/ +ghost mathint simpleERC20_sumOfBalances { + init_state axiom simpleERC20_sumOfBalances == 0; +} + + +// to learn more about using hook in CVL you can read the docs: https://docs.certora.com/en/latest/docs/cvl/hooks.html +hook Sstore simpleERC20._balance[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { + simpleERC20_sumOfBalances = simpleERC20_sumOfBalances + newValue - oldValue; +} + +invariant totalSupplyIsSumOfBalances() + to_mathint(simpleERC20.totalSupply()) == simpleERC20_sumOfBalances; diff --git a/src/contracts/Ghost.sol b/src/contracts/Ghost.sol index c5c3da5..5217a5c 100644 --- a/src/contracts/Ghost.sol +++ b/src/contracts/Ghost.sol @@ -1,5 +1,5 @@ // SPDX-License-Identifier: MIT -pragma solidity ^0.8.0; +pragma solidity ^0.8.8; import '../interfaces/IGhost.sol';