From 2017d17c413e8e40c9739185a97e4cdc17fdcc50 Mon Sep 17 00:00:00 2001 From: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Date: Sat, 3 Feb 2024 19:50:37 +0200 Subject: [PATCH] certora setup --- .github/workflows/certora.yml | 104 ++++++++++++++++++++++ certora/README.md | 51 +++++++++++ certora/confs/ghost.conf | 19 +++++ certora/confs/ghostWithERC20s.conf | 21 +++++ certora/confs/mutation.mconf | 9 ++ certora/helpers/ERC20Helper.sol | 15 ++++ certora/helpers/SimpleERC20.sol | 44 ++++++++++ certora/specs/ghost.spec | 123 +++++++++++++++++++++++++++ certora/specs/moreExamplesERC20.spec | 68 +++++++++++++++ 9 files changed, 454 insertions(+) create mode 100644 .github/workflows/certora.yml create mode 100644 certora/README.md create mode 100644 certora/confs/ghost.conf create mode 100644 certora/confs/ghostWithERC20s.conf create mode 100644 certora/confs/mutation.mconf create mode 100644 certora/helpers/ERC20Helper.sol create mode 100644 certora/helpers/SimpleERC20.sol create mode 100644 certora/specs/ghost.spec create mode 100644 certora/specs/moreExamplesERC20.spec diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 0000000..2cb08f7 --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,104 @@ +# 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 version of solc + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.0/solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.0 + chmod +x /usr/local/bin/solc8.0 + ln -s /usr/local/bin/solc8.0 /usr/local/bin/solc + + 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 + max-parallel: 4 + 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: 'ghosWithERC20s.conf' } + + \ No newline at end of file diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 0000000..12f4a44 --- /dev/null +++ b/certora/README.md @@ -0,0 +1,51 @@ +# Certora + +This folder provides a fully functional skeleton for integrating with Certora. +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` + +Set your Certora Key: +`export CERTORAKEY=` + +Then run from this directory: +`certoraRun ./certora/confs/ghost.conf` + +## 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. + +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 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. +This demonstrates how to setup 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` + + +## 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..0dd9302 --- /dev/null +++ b/certora/confs/ghost.conf @@ -0,0 +1,19 @@ +// A default configuration for a standalone contract +{ + // list of files that are part of the system + "files": [ + "src/contracts/Ghost.sol" + ], + // main contract to verify ghost and spec file + "verify": "Ghost:certora/specs/ghost.spec", + // check the spec + "rule_sanity" :"basic", + // assume 3 unroling of loops is enought + "loop_iter" : "3", + "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..0e06d55 --- /dev/null +++ b/certora/confs/ghostWithERC20s.conf @@ -0,0 +1,21 @@ +// A default configuration for a standalone contract +{ + // 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 + "verify": "Ghost:certora/specs/moreExamplesERC20.spec", + // check the spec + "rule_sanity" :"basic", + // assume 3 unroling of loops is enought + "loop_iter" : "3", + "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" +} \ No newline at end of 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/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..4962e3a --- /dev/null +++ b/certora/helpers/SimpleERC20.sol @@ -0,0 +1,44 @@ +// 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..1ca65f7 --- /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`). + 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. +**/ +rule reachability(method f) +{ + env e; + calldataarg args; + f(e,args); //takes into account only non reveting cases + satisfy true; +} + +/** + @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 + require e.msg.value == 0; + f@withrevert(e, arg); + assert !lastReverted, "method should not 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 on which this property should hole + /* filtered { f-> !f.isView, g-> !g.isView } */ +{ + env e1; + calldataarg arg; + + storage initialStorage = lastStorage; + f(e1, arg); + + + env e2; + calldataarg arg2; + require e2.msg.sender != e1.msg.sender; + g(e2, arg2) at initialStorage; //roll back to state before calling f + + f@withrevert(e1, arg); + 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 arg; + require e1.msg.sender == privileged; + + storage initialStorage = lastStorage; + f@withrevert(e1, arg); // privileged succeeds executing candidate privileged operation. + bool firstSucceeded = !lastReverted; + + env e2; + calldataarg arg2; + require e2.msg.sender != privileged; + f@withrevert(e2, arg2) at initialStorage; // unprivileged + bool secondSucceeded = !lastReverted; + + satisfy (firstSucceeded && secondSucceeded), "function is not privileged"; +} + + +/** + @title This rule check with 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 ; /* fill in cases where eth can decrease */ +} + + +// just an example of the structure of an invariant +invariant dummy() + nativeBalances[currentContract] >= 0; \ No newline at end of file diff --git a/certora/specs/moreExamplesERC20.spec b/certora/specs/moreExamplesERC20.spec new file mode 100644 index 0000000..89b05a5 --- /dev/null +++ b/certora/specs/moreExamplesERC20.spec @@ -0,0 +1,68 @@ +/*** + +Spec for the Certora Verification Language. +See https://docs.certora.com for a complete guide. + +run this file with ghostWithERc20s.conf: + +certoraRun certora\confs\hostWithERc20s.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 implementaions found in the list of contracts + 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 +*/ +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 ; //fill in cases token can decrease + +} + +/** + @title sum of erc20 balances if totalSupply + @dev usign a ghost variable and hooks to track changes to _balances +**/ +ghost mathint simpleERC20_sumOfBalances { + init_state axiom simpleERC20_sumOfBalances == 0; +} + +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; \ No newline at end of file