certora setup

.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/<contents of the command>
+          #
+          # 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' }
+
+

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=<personal_access_key>` 
+
+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 <a href=https://www.certora.com/gambit>Gambit</a>, 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 <a href="https://github.com/Certora/Examples/tree/master/CVLByExample" target="_blank">CVL specification general examples</a>
+and  <a href="https://docs.certora.com" target="_blank">Documenation</a>.
+More mutation configurations can be found in the [certoraInit repo](https://github.com/Certora/CertoraInit"). 

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"
+}

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"
+}

certora/confs/mutation.mconf

@@ -0,0 +1,9 @@
+{
+    "gambit": [
+        {
+            "filename" : "../../src/contracts/Ghost.sol",
+            "num_mutants": 1
+        }
+    ],
+    "msg": "basic mutation configuration"
+} 

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);
+    }
+}

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;
+    }
+}

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;