Merge pull request #136 from morpho-org/certora/dev

[Certora] Dev

.github/workflows/certora.yml

@@ -0,0 +1,51 @@
+name: Certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    strategy:
+      fail-fast: false
+
+      matrix:
+        conf:
+          - AccrueInterest
+          - ConsistentState
+          - ExactMath
+          - ExitLiquidity
+          - Health
+          - LibSummary
+          - Liveness
+          - RatioMath
+          - Reentrancy
+          - Reverts
+          - Transfer
+
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v4
+
+      - name: Install certora
+        run: pip install certora-cli
+
+      - name: Install solc
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc
+
+      - name: Verify ${{ matrix.conf }}
+        run: certoraRun certora/confs/${{ matrix.conf }}.conf
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.gitignore

@@ -16,6 +16,10 @@ docs/
 # Node modules
 /node_modules
 
+# Certora
+.certora**
+emv-*-certora*
+
 # Hardhat
 /types
 /cache_hardhat

README.md

@@ -40,4 +40,4 @@ All audits are stored in the [audits](./audits/)' folder.
 ## Licences
 
 The primary license for Morpho Blue is the Business Source License 1.1 (`BUSL-1.1`), see [`LICENSE`](./LICENSE).
-However, all files in the following folders can also be licensed under `GPL-2.0-or-later` (as indicated in their SPDX headers): [`src/interfaces`](./src/interfaces), [`src/libraries`](./src/libraries), [`src/mocks`](./src/mocks), [`test`](./test).
+However, all files in the following folders can also be licensed under `GPL-2.0-or-later` (as indicated in their SPDX headers): [`src/interfaces`](./src/interfaces), [`src/libraries`](./src/libraries), [`src/mocks`](./src/mocks), [`test`](./test), [`certora`](./certora).

certora/confs/AccrueInterest.conf

@@ -0,0 +1,12 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/AccrueInterest.spec",
+    "prover_args": [
+        "-smt_hashingScheme plaininjectivity",
+        "-mediumTimeout 30"
+    ],
+    "rule_sanity": "basic",
+    "msg": "Morpho Blue Accrue Interest"
+}

certora/confs/ConsistentState.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/ConsistentState.spec",
+    "rule_sanity": "basic",
+    "msg": "Morpho Blue Consistent State"
+}

certora/confs/ExactMath.conf

@@ -0,0 +1,12 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/ExactMath.spec",
+    "rule_sanity": "basic",
+    "prover_args": [
+        "-smt_hashingScheme plaininjectivity",
+        "-mediumTimeout 30"
+    ],
+    "msg": "Morpho Blue Exact Math"
+}

certora/confs/ExitLiquidity.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec",
+    "rule_sanity": "basic",
+    "msg": "Morpho Blue Exit Liquidity"
+}

certora/confs/Health.conf

@@ -0,0 +1,12 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol",
+        "src/mocks/OracleMock.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/Health.spec",
+    "rule_sanity": "basic",
+    "prover_args": [
+        "-smt_hashingScheme plaininjectivity"
+    ],
+    "msg": "Morpho Blue Health"
+}

certora/confs/LibSummary.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/LibSummary.spec",
+    "rule_sanity": "basic",
+    "msg": "Morpho Blue Lib Summary"
+}

certora/confs/Liveness.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harness/MorphoInternalAccess.sol"
+    ],
+    "verify": "MorphoInternalAccess:certora/specs/Liveness.spec",
+    "rule_sanity": "basic",
+    "msg": "Morpho Blue Liveness"
+}

certora/confs/RatioMath.conf

@@ -0,0 +1,13 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/RatioMath.spec",
+    "rule_sanity": "basic",
+    "prover_args": [
+        "-smt_hashingScheme plaininjectivity",
+        "-mediumTimeout 30",
+        "-timeout 3600"
+    ],
+    "msg": "Morpho Blue Ratio Math"
+}

certora/confs/Reentrancy.conf

@@ -0,0 +1,11 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/Reentrancy.spec",
+    "rule_sanity": "basic",
+    "prover_args": [
+        "-enableStorageSplitting false"
+    ],
+    "msg": "Morpho Blue Reentrancy"
+}

certora/confs/Reverts.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "certora/harness/MorphoHarness.sol"
+    ],
+    "verify": "MorphoHarness:certora/specs/Reverts.spec",
+    "rule_sanity": "basic",
+    "msg": "Morpho Blue Reverts"
+}

certora/confs/Transfer.conf

@@ -0,0 +1,11 @@
+{
+    "files": [
+        "certora/harness/TransferHarness.sol",
+        "certora/dispatch/ERC20Standard.sol",
+        "certora/dispatch/ERC20USDT.sol",
+        "certora/dispatch/ERC20NoRevert.sol"
+    ],
+    "verify": "TransferHarness:certora/specs/Transfer.spec",
+    "rule_sanity": "basic",
+    "msg": "Morpho Blue Transfer"
+}

certora/dispatch/ERC20NoRevert.sol

@@ -0,0 +1,48 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+contract ERC20NoRevert {
+    address public owner;
+    uint256 public totalSupply;
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    constructor() {
+        owner = msg.sender;
+    }
+
+    modifier onlyOwner() {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function _transfer(address _from, address _to, uint256 _amount) internal returns (bool) {
+        if (balanceOf[_from] < _amount) {
+            return false;
+        }
+        balanceOf[_from] -= _amount;
+        balanceOf[_to] += _amount;
+        return true;
+    }
+
+    function transfer(address _to, uint256 _amount) public returns (bool) {
+        return _transfer(msg.sender, _to, _amount);
+    }
+
+    function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) {
+        if (allowance[_from][msg.sender] < _amount) {
+            return false;
+        }
+        allowance[_from][msg.sender] -= _amount;
+        return _transfer(_from, _to, _amount);
+    }
+
+    function approve(address _spender, uint256 _amount) public {
+        allowance[msg.sender][_spender] = _amount;
+    }
+
+    function mint(address _receiver, uint256 _amount) public onlyOwner {
+        balanceOf[_receiver] += _amount;
+        totalSupply += _amount;
+    }
+}

certora/dispatch/ERC20Standard.sol

@@ -0,0 +1,42 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+contract ERC20Standard {
+    address public owner;
+    uint256 public totalSupply;
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    constructor() {
+        owner = msg.sender;
+    }
+
+    modifier onlyOwner() {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function _transfer(address _from, address _to, uint256 _amount) internal returns (bool) {
+        balanceOf[_from] -= _amount;
+        balanceOf[_to] += _amount;
+        return true;
+    }
+
+    function transfer(address _to, uint256 _amount) public returns (bool) {
+        return _transfer(msg.sender, _to, _amount);
+    }
+
+    function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) {
+        allowance[_from][msg.sender] -= _amount;
+        return _transfer(_from, _to, _amount);
+    }
+
+    function approve(address _spender, uint256 _amount) public {
+        allowance[msg.sender][_spender] = _amount;
+    }
+
+    function mint(address _receiver, uint256 _amount) public onlyOwner {
+        balanceOf[_receiver] += _amount;
+        totalSupply += _amount;
+    }
+}

certora/dispatch/ERC20USDT.sol

@@ -0,0 +1,45 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+contract ERC20USDT {
+    address public owner;
+    uint256 public totalSupply;
+    mapping(address => uint256) public balanceOf;
+    mapping(address => mapping(address => uint256)) public allowance;
+
+    constructor() {
+        owner = msg.sender;
+    }
+
+    modifier onlyOwner() {
+        require(msg.sender == owner);
+        _;
+    }
+
+    function _transfer(address _from, address _to, uint256 _amount) internal {
+        balanceOf[_from] -= _amount;
+        balanceOf[_to] += _amount;
+    }
+
+    function transfer(address _to, uint256 _amount) public {
+        _transfer(msg.sender, _to, _amount);
+    }
+
+    function transferFrom(address _from, address _to, uint256 _amount) public {
+        if (allowance[_from][msg.sender] < type(uint256).max) {
+            allowance[_from][msg.sender] -= _amount;
+        }
+        _transfer(_from, _to, _amount);
+    }
+
+    function approve(address _spender, uint256 _amount) public {
+        require(!((_amount != 0) && (allowance[msg.sender][_spender] != 0)));
+
+        allowance[msg.sender][_spender] = _amount;
+    }
+
+    function mint(address _receiver, uint256 _amount) public onlyOwner {
+        balanceOf[_receiver] += _amount;
+        totalSupply += _amount;
+    }
+}

certora/gambit.conf

@@ -0,0 +1,6 @@
+ {
+      "filename" : "../src/Morpho.sol",
+      "sourceroot": "..",
+      "num_mutants": 15,
+      "solc_remappings": []
+}