Certora formally verified rewards checker

.github/workflows/ci-certora.yml

@@ -0,0 +1,58 @@
+name: Certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    paths:
+      - "certora/**"
+      - "lib/**"
+      - "src/common/**"
+      - "*.lock"
+      - "foundry.toml"
+      - "remappings.txt"
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    strategy:
+      fail-fast: false
+
+      matrix:
+        conf:
+          - MerkleTrees
+          - RewardsDistributor
+
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - uses: actions/setup-node@v3
+        with:
+          node-version: 16
+          cache: yarn
+
+      - name: Install dependencies
+        run: yarn install --frozen-lockfile
+        shell: bash
+
+      - 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.13/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc8.13
+
+      - name: Verify ${{ matrix.conf }}
+        run: certoraRun certora/confs/${{ matrix.conf }}.conf
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.gitignore

@@ -39,3 +39,7 @@ lcov.*
 
 # docs
 /docs
+
+# certora
+.certora**
+emv-*-certora*

certora/README.md

@@ -0,0 +1,60 @@
+This folder contains the verification of the rewards distribution mechanism of Morpho Optimizers using CVL, Certora's Verification Language.
+
+# Folder and file structure
+
+The [`certora/specs`](specs) folder contains the specification files.
+
+The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file.
+
+The [`certora/helpers`](helpers) folder contains files that enable the verification of Morpho Blue.
+
+# Overview of the verification
+
+This work aims at providing a formally verified rewards checker.
+The rewards checker is composed of the [Checker.sol](checker/Checker.sol) file, which takes a certificate as an input.
+The certificate is assumed to contain the submitted root to verify, a total amount of rewards distributed, and a Merkle tree, and it is checked that:
+
+1. the Merkle tree is a well-formed Merkle tree
+2. the total amount of rewards distributed matches the total rewards contained in the Merkle tree
+
+Those checks are done by only using "trusted" functions, namely `newLeaf` and `newInternalNode`, that have been formally verified to preserve those invariants:
+
+- it is checked in [MerkleTrees.spec](specs/MerkleTrees.spec) that those functions lead to creating well-formed trees.
+  Well-formed trees also verify that the value of their internal node is the sum of the rewards it contains.
+- it is checked in [RewardsDistributor.spec](specs/RewardsDistributor.spec) that the rewards distributor is correct, meaning that claimed rewards correspond exactly to the rewards contained in the corresponding Merkle tree.
+
+# Getting started
+
+## Verifying the rewards checker
+
+Install `certora-cli` package with `pip install certora-cli`.
+To verify specification files, pass to `certoraRun` the corresponding configuration file in the [`certora/confs`](confs) folder.
+It requires having set the `CERTORAKEY` environment variable to a valid Certora key.
+You can also pass additional arguments, notably to verify a specific rule.
+For example, at the root of the repository:
+
+```
+certoraRun certora/confs/MerkleTrees.conf --rule wellFormed
+```
+
+## Running the rewards checker
+
+To verify that a given list of proofs corresponds to a valid Merkle tree, you must generate a certificate from it.
+This assumes that the list of proofs is in the expected JSON format.
+For example, at the root of the repository, given a `proofs.json` file:
+
+```
+python certora/checker/create_certificate.py proofs.json
+```
+
+This requires installing the corresponding libraries first:
+
+```
+pip install web3 eth-tester py-evm
+```
+
+Then, verify this certificate:
+
+```
+FOUNDRY_PROFILE=checker forge test
+```

certora/checker/Checker.sol

@@ -0,0 +1,59 @@
+// SPDX-License-Identifier: GNU AGPLv3
+pragma solidity ^0.8.0;
+
+import "../../lib/morpho-utils/lib/openzeppelin-contracts/contracts/utils/Strings.sol";
+import "../helpers/MerkleTreeLib.sol";
+import "../../lib/forge-std/src/Test.sol";
+import "../../lib/forge-std/src/StdJson.sol";
+
+contract Checker is Test {
+    using MerkleTreeLib for MerkleTreeLib.Tree;
+    using stdJson for string;
+
+    MerkleTreeLib.Tree public tree;
+
+    struct Leaf {
+        address addr;
+        uint256 value;
+    }
+
+    struct InternalNode {
+        address addr;
+        address left;
+        address right;
+    }
+
+    function testVerifyCertificate() public {
+        string memory projectRoot = vm.projectRoot();
+        string memory path = string.concat(projectRoot, "/certificate.json");
+        string memory json = vm.readFile(path);
+
+        uint256 leafLength = abi.decode(json.parseRaw(".leafLength"), (uint256));
+        Leaf memory leaf;
+        for (uint256 i; i < leafLength; i++) {
+            leaf = abi.decode(
+                json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")),
+                (Leaf)
+            );
+            tree.newLeaf(leaf.addr, leaf.value);
+        }
+
+        uint256 nodeLength = abi.decode(json.parseRaw(".nodeLength"), (uint256));
+        InternalNode memory node;
+        for (uint256 i; i < nodeLength; i++) {
+            node = abi.decode(
+                json.parseRaw(string.concat(".node[", Strings.toString(i), "]")),
+                (InternalNode)
+            );
+            tree.newInternalNode(node.addr, node.left, node.right);
+        }
+
+        assertTrue(!tree.isEmpty(node.addr), "empty root");
+
+        uint256 total = abi.decode(json.parseRaw(".total"), (uint256));
+        assertEq(tree.getValue(node.addr), total, "incorrect total rewards");
+
+        bytes32 root = abi.decode(json.parseRaw(".root"), (bytes32));
+        assertEq(tree.getHash(node.addr), root, "mismatched roots");
+    }
+}

certora/checker/create_certificate.py

@@ -0,0 +1,78 @@
+import sys
+import json
+from web3 import Web3, EthereumTesterProvider
+
+w3 = Web3(EthereumTesterProvider())
+
+
+def keccak_node(left_hash, right_hash):
+    return w3.to_hex(
+        w3.solidity_keccak(["bytes32", "bytes32"], [left_hash, right_hash])
+    )
+
+
+def keccak_leaf(address, amount):
+    address = w3.to_checksum_address(address)
+    return w3.to_hex(w3.solidity_keccak(["address", "uint256"], [address, amount]))
+
+
+certificate = {}
+hash_to_address = {}
+hash_to_value = {}
+left = {}
+right = {}
+
+
+def populate(address, amount, proof):
+    amount = int(amount)
+    computedHash = keccak_leaf(address, amount)
+    hash_to_address[computedHash] = address
+    hash_to_value[computedHash] = amount
+    for proofElement in proof:
+        [leftHash, rightHash] = (
+            [computedHash, proofElement]
+            if computedHash <= proofElement
+            else [proofElement, computedHash]
+        )
+        computedHash = keccak_node(leftHash, rightHash)
+        left[computedHash] = leftHash
+        right[computedHash] = rightHash
+        hash_to_address[computedHash] = keccak_node(computedHash, computedHash)[:42]
+
+
+def walk(h):
+    if h in left:
+        walk(left[h])
+        walk(right[h])
+        certificate["node"].append(
+            {
+                "addr": hash_to_address[h],
+                "left": hash_to_address[left[h]],
+                "right": hash_to_address[right[h]],
+            }
+        )
+    else:
+        certificate["leaf"].append(
+            {"addr": hash_to_address[h], "value": hash_to_value[h]}
+        )
+
+
+with open(sys.argv[1]) as input_file:
+    proofs = json.load(input_file)
+    certificate["root"] = proofs["root"]
+    certificate["total"] = int(proofs["total"])
+    certificate["leaf"] = []
+    certificate["node"] = []
+
+    for address, data in proofs["proofs"].items():
+        populate(address, data["amount"], data["proof"])
+
+    walk(proofs["root"])
+
+    certificate["leafLength"] = len(certificate["leaf"])
+    certificate["nodeLength"] = len(certificate["node"])
+
+    json_output = json.dumps(certificate)
+
+with open("certificate.json", "w") as output_file:
+    output_file.write(json_output)

certora/confs/MerkleTrees.conf

@@ -0,0 +1,12 @@
+{
+    "files": [
+        "certora/helpers/MerkleTrees.sol"
+    ],
+    "solc": "solc8.13",
+    "verify": "MerkleTrees:certora/specs/MerkleTrees.spec",
+    "loop_iter": "4",
+    "optimistic_loop": true,
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "Merkle Tree",
+}

certora/confs/RewardsDistributor.conf

@@ -0,0 +1,21 @@
+{
+    "files": [
+        "src/common/rewards-distribution/RewardsDistributor.sol",
+        "certora/helpers/MerkleTrees.sol",
+        "certora/helpers/MorphoToken.sol",
+    ],
+    "solc": "solc8.13",
+    "verify": "RewardsDistributor:certora/specs/RewardsDistributor.spec",
+    "link": [
+        "RewardsDistributor:MORPHO=MorphoToken"
+    ],
+    "packages": [
+        "@openzeppelin=node_modules/@openzeppelin",
+        "@rari-capital/solmate=lib/solmate",
+    ],
+    "optimistic_loop": true,
+    "loop_iter": "4",
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "Rewards Distributor",
+}