[Certora] Universal rewards distributor verification

.github/workflows/certora.yml

@@ -0,0 +1,45 @@
+name: Certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    strategy:
+      fail-fast: false
+
+      matrix:
+        conf:
+          - MerkleTree
+          - UniversalRewardsDistributor
+
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - 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-0.8.19
+
+      - name: Verify ${{ matrix.conf }}
+        run: certoraRun certora/confs/${{ matrix.conf }}.conf
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.gitignore

@@ -15,4 +15,8 @@ docs/
 
 # npm
 package-lock.json
-node_modules
+node_modules
+
+# certora
+.certora**
+emv-*-certora*

Dockerfile

@@ -0,0 +1,14 @@
+FROM ubuntu:latest
+WORKDIR /usr/rewards-checker
+
+RUN apt update
+RUN apt install python3-pip git curl -y
+RUN pip install web3 eth-tester py-evm
+
+RUN curl -L https://foundry.paradigm.xyz | bash
+ENV PATH="${PATH}:/root/.foundry/bin/"
+RUN foundryup
+
+COPY . .
+RUN python3 certora/checker/create_certificate.py proofs.json
+RUN FOUNDRY_PROFILE=checker forge test

certora/README.md

@@ -0,0 +1,56 @@
+This folder contains the verification of the universal rewards distribution mechanism 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 and a Merkle tree, and it is checked that the Merkle tree is well-formed.
+
+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 [MerkleTree.spec](specs/MerkleTree.spec) that those functions lead to creating well-formed trees.
+- it is checked in [UniversalRewardsDistributor.spec](specs/UniversalRewardsDistributor.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, check this certificate:
+
+```
+FOUNDRY_PROFILE=checker forge test
+```

certora/checker/Checker.sol

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity ^0.8.0;
+
+import "../../lib/openzeppelin-contracts/contracts/utils/Strings.sol";
+import "../helpers/MerkleTree.sol";
+import "../../lib/forge-std/src/Test.sol";
+import "../../lib/forge-std/src/StdJson.sol";
+
+contract Checker is Test {
+    using stdJson for string;
+
+    MerkleTree tree = new MerkleTree();
+
+    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);
+        }
+
+        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);
+        }
+
+        assertTrue(!tree.isEmpty(node.id), "empty root");
+
+        bytes32 root = abi.decode(json.parseRaw(".root"), (bytes32));
+        assertEq(tree.getHash(node.id), root, "mismatched roots");
+    }
+}

certora/checker/create_certificate.py

@@ -0,0 +1,109 @@
+import sys
+import json
+from eth_abi import encode
+from web3 import Web3, EthereumTesterProvider
+
+w3 = Web3(EthereumTesterProvider())
+
+
+# Returns the hash of a node given the hashes of its children.
+def hash_node(left_hash, right_hash):
+    return w3.to_hex(
+        w3.solidity_keccak(["bytes32", "bytes32"], [left_hash, right_hash])
+    )
+
+
+# Returns the hash of a leaf given the rewards details.
+def hash_leaf(address, reward, amount):
+    encoded_args = encode(["address", "address", "uint256"], [address, reward, amount])
+    first_hash = w3.solidity_keccak(
+        ["bytes"],
+        [encoded_args],
+    )
+    second_hash = w3.solidity_keccak(
+        ["bytes"],
+        [first_hash],
+    )
+    return w3.to_hex(second_hash)
+
+
+# Returns the identifier of a leaf.
+def hash_id(addr, reward):
+    encoded_args = encode(["address", "address"], [addr, reward])
+    return w3.to_hex(w3.solidity_keccak(["bytes"], [encoded_args]))
+
+
+certificate = {}
+hash_to_id = {}
+hash_to_address = {}
+hash_to_reward = {}
+hash_to_value = {}
+left = {}
+right = {}
+
+
+# Populates the fields of the tree along the path given by the proof.
+def populate(addr, reward, amount, proof):
+    computedHash = hash_leaf(addr, reward, amount)
+    hash_to_id[computedHash] = hash_id(addr, reward)
+    hash_to_address[computedHash] = addr
+    hash_to_reward[computedHash] = reward
+    hash_to_value[computedHash] = amount
+    for proofElement in proof:
+        [leftHash, rightHash] = (
+            [computedHash, proofElement]
+            if computedHash <= proofElement
+            else [proofElement, computedHash]
+        )
+        computedHash = hash_node(leftHash, rightHash)
+        hash_to_id[computedHash] = computedHash
+        left[computedHash] = leftHash
+        right[computedHash] = rightHash
+
+
+# Traverse the tree and generate corresponding instruction for each internal node and each leaf.
+def walk(node):
+    if node in left:
+        walk(left[node])
+        walk(right[node])
+        certificate["node"].append(
+            {
+                "id": node,
+                "left": hash_to_id[left[node]],
+                "right": hash_to_id[right[node]],
+            }
+        )
+    else:
+        certificate["leaf"].append(
+            {
+                "addr": hash_to_address[node],
+                "reward": hash_to_reward[node],
+                "value": hash_to_value[node],
+            }
+        )
+
+
+with open(sys.argv[1]) as input_file:
+    proofs = json.load(input_file)
+    rewards = proofs["rewards"]
+
+    certificate["root"] = proofs["root"]
+    certificate["leaf"] = []
+    certificate["node"] = []
+
+    for addr, data in rewards.items():
+        address = w3.to_checksum_address(addr)
+        for reward, data in data.items():
+            reward = w3.to_checksum_address(reward)
+            amount = int(data["amount"])
+            populate(addr, reward, 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/MerkleTree.conf

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

certora/confs/UniversalRewardsDistributor.conf

@@ -0,0 +1,15 @@
+{
+    "files": [
+        "src/UniversalRewardsDistributor.sol",
+        "lib/openzeppelin-contracts/contracts/token/ERC20/ERC20.sol",
+        "certora/helpers/MerkleTree.sol",
+        "certora/helpers/Util.sol",
+    ],
+    "solc": "solc-0.8.19",
+    "verify": "UniversalRewardsDistributor:certora/specs/UniversalRewardsDistributor.spec",
+    "optimistic_loop": true,
+    "loop_iter": "4",
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "Universal Rewards Distributor",
+}