diff --git a/.github/workflows/ci-certora.yml b/.github/workflows/ci-certora.yml new file mode 100644 index 000000000..bf9333253 --- /dev/null +++ b/.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 }} diff --git a/.gitignore b/.gitignore index 87882328d..6a651f72f 100644 --- a/.gitignore +++ b/.gitignore @@ -39,3 +39,7 @@ lcov.* # docs /docs + +# certora +.certora** +emv-*-certora* diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 000000000..aa16618b7 --- /dev/null +++ b/certora/README.md @@ -0,0 +1,61 @@ +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. +Examples of lists of proofs can be found as `proofs.json` files in the subfolders of the [distribution folder of morpho-optimizers-rewards](https://github.com/morpho-org/morpho-optimizers-rewards/tree/main/distribution). +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 +``` diff --git a/certora/checker/Checker.sol b/certora/checker/Checker.sol new file mode 100644 index 000000000..364773b09 --- /dev/null +++ b/certora/checker/Checker.sol @@ -0,0 +1,50 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; + +import "../../lib/morpho-utils/lib/openzeppelin-contracts/contracts/utils/Strings.sol"; +import "../helpers/MerkleTrees.sol"; +import "../../lib/forge-std/src/Test.sol"; +import "../../lib/forge-std/src/StdJson.sol"; + +contract Checker is Test { + using stdJson for string; + + MerkleTrees trees = new MerkleTrees(); + address constant tree = address(0); + + 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)); + MerkleTreeLib.Leaf memory leaf; + for (uint256 i; i < leafLength; i++) { + leaf = abi.decode( + json.parseRaw(string.concat(".leaf[", Strings.toString(i), "]")), + (MerkleTreeLib.Leaf) + ); + trees.newLeaf(tree, leaf); + } + + uint256 nodeLength = abi.decode(json.parseRaw(".nodeLength"), (uint256)); + MerkleTreeLib.InternalNode memory node; + for (uint256 i; i < nodeLength; i++) { + node = abi.decode( + json.parseRaw(string.concat(".node[", Strings.toString(i), "]")), + (MerkleTreeLib.InternalNode) + ); + trees.newInternalNode(tree, node); + } + + // At this point `node` is the candidate for the root. + + assertTrue(!trees.isEmpty(tree, node.addr), "empty root"); + + uint256 total = abi.decode(json.parseRaw(".total"), (uint256)); + assertEq(trees.getValue(tree, node.addr), total, "incorrect total rewards"); + + bytes32 root = abi.decode(json.parseRaw(".root"), (bytes32)); + assertEq(trees.getHash(tree, node.addr), root, "mismatched roots"); + } +} diff --git a/certora/checker/create_certificate.py b/certora/checker/create_certificate.py new file mode 100644 index 000000000..5d3c3fc28 --- /dev/null +++ b/certora/checker/create_certificate.py @@ -0,0 +1,82 @@ +import sys +import json +from web3 import Web3, EthereumTesterProvider + +w3 = Web3(EthereumTesterProvider()) + + +# Returns the hash of a node given the hashes of its children. +def keccak_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 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 = {} + + +# Populates the fields of the tree along the path given by the proof. +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] + + +# 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( + { + "addr": hash_to_address[node], + "left": hash_to_address[left[node]], + "right": hash_to_address[right[node]], + } + ) + else: + certificate["leaf"].append( + {"addr": hash_to_address[node], "value": hash_to_value[node]} + ) + + +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) diff --git a/certora/confs/MerkleTrees.conf b/certora/confs/MerkleTrees.conf new file mode 100644 index 000000000..f90dfd073 --- /dev/null +++ b/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", +} diff --git a/certora/confs/RewardsDistributor.conf b/certora/confs/RewardsDistributor.conf new file mode 100644 index 000000000..d0f4b263e --- /dev/null +++ b/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", +} diff --git a/certora/helpers/MerkleTreeLib.sol b/certora/helpers/MerkleTreeLib.sol new file mode 100644 index 000000000..6b1bdca10 --- /dev/null +++ b/certora/helpers/MerkleTreeLib.sol @@ -0,0 +1,96 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; + +library MerkleTreeLib { + using MerkleTreeLib for Node; + + struct Leaf { + address addr; + uint256 value; + } + + struct InternalNode { + address addr; + address left; + address right; + } + + struct Node { + address left; + address right; + uint256 value; + // hash of [addr, value] for leaves, and [left.hash, right.hash] for internal nodes. + bytes32 hashNode; + } + + function isEmpty(Node memory node) internal pure returns (bool) { + return + node.left == address(0) && + node.right == address(0) && + node.value == 0 && + node.hashNode == bytes32(0); + } + + // The tree has no root because every node (and the nodes underneath) form a Merkle tree. + struct Tree { + mapping(address => Node) nodes; + } + + function newLeaf(Tree storage tree, Leaf memory leaf) internal { + // The address of the receiving account is used as the key to create a new leaf. + // This ensures that a single account cannot appear twice in the tree. + Node storage node = tree.nodes[leaf.addr]; + require(leaf.addr != address(0), "addr is zero address"); + require(leaf.value != 0, "value is zero"); + require(node.isEmpty(), "leaf is not empty"); + + node.value = leaf.value; + node.hashNode = keccak256(abi.encodePacked(leaf.addr, leaf.value)); + } + + function newInternalNode(Tree storage tree, InternalNode memory internalNode) internal { + // The key of the new internal node is left arbitrary. + Node storage node = tree.nodes[internalNode.addr]; + Node storage leftNode = tree.nodes[internalNode.left]; + Node storage rightNode = tree.nodes[internalNode.right]; + require(internalNode.addr != address(0), "node is zero address"); + require(node.isEmpty(), "node is not empty"); + require(!leftNode.isEmpty(), "left is empty"); + require(!rightNode.isEmpty(), "right is empty"); + require(leftNode.hashNode <= rightNode.hashNode, "children are not pair sorted"); + + node.left = internalNode.left; + node.right = internalNode.right; + // The value of an internal node represents the sum of the values of the leaves underneath. + node.value = leftNode.value + rightNode.value; + node.hashNode = keccak256(abi.encode(leftNode.hashNode, rightNode.hashNode)); + } + + // The specification of a well-formed tree is the following: + // - empty nodes are well-formed + // - other nodes should have non-zero value, where the leaf node contains the value of the account and internal nodes contain the sum of the values of its leaf children. + // - correct hashing of leaves and of internal nodes + // - internal nodes have their children pair sorted and not empty + function isWellFormed(Tree storage tree, address addr) internal view returns (bool) { + Node storage node = tree.nodes[addr]; + + if (node.isEmpty()) return true; + + if (node.value == 0) return false; + + if (node.left == address(0) && node.right == address(0)) { + return node.hashNode == keccak256(abi.encodePacked(addr, node.value)); + } else { + // Well-formed nodes have exactly 0 or 2 children. + if (node.left == address(0) || node.right == address(0)) return false; + Node storage left = tree.nodes[node.left]; + Node storage right = tree.nodes[node.right]; + return + !left.isEmpty() && + !right.isEmpty() && + node.value == left.value + right.value && + left.hashNode <= right.hashNode && + node.hashNode == keccak256(abi.encode(left.hashNode, right.hashNode)); + } + } +} diff --git a/certora/helpers/MerkleTrees.sol b/certora/helpers/MerkleTrees.sol new file mode 100644 index 000000000..8a254c6d4 --- /dev/null +++ b/certora/helpers/MerkleTrees.sol @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity ^0.8.0; + +import "./MerkleTreeLib.sol"; + +contract MerkleTrees { + using MerkleTreeLib for MerkleTreeLib.Node; + using MerkleTreeLib for MerkleTreeLib.Tree; + + mapping(address => MerkleTreeLib.Tree) internal trees; + + function newLeaf(address tree, MerkleTreeLib.Leaf memory leaf) public { + trees[tree].newLeaf(leaf); + } + + function newInternalNode(address tree, MerkleTreeLib.InternalNode memory internalNode) public { + trees[tree].newInternalNode(internalNode); + } + + function getLeft(address tree, address node) public view returns (address) { + return trees[tree].nodes[node].left; + } + + function getRight(address tree, address node) public view returns (address) { + return trees[tree].nodes[node].right; + } + + function getValue(address tree, address node) public view returns (uint256) { + return trees[tree].nodes[node].value; + } + + function getHash(address tree, address node) public view returns (bytes32) { + return trees[tree].nodes[node].hashNode; + } + + function isEmpty(address tree, address node) public view returns (bool) { + return trees[tree].nodes[node].isEmpty(); + } + + function isWellFormed(address tree, address node) public view returns (bool) { + return trees[tree].isWellFormed(node); + } + + // Check that the nodes are well formed starting from `node` and going down the `tree. + // The `proof` is used to choose the path downward. + function wellFormedPath( + address tree, + address node, + bytes32[] memory proof + ) public view { + for (uint256 i = proof.length; ; ) { + require(isWellFormed(tree, node)); + + if (i == 0) break; + + bytes32 otherHash = proof[--i]; + + address left = getLeft(tree, node); + address right = getRight(tree, node); + + node = getHash(tree, left) == otherHash ? right : left; + } + } +} diff --git a/certora/helpers/MorphoToken.sol b/certora/helpers/MorphoToken.sol new file mode 100644 index 000000000..83a10679c --- /dev/null +++ b/certora/helpers/MorphoToken.sol @@ -0,0 +1,10 @@ +// SPDX-License-Identifier: AGPL-3.0-only +pragma solidity >=0.8.0; + +import "@rari-capital/solmate/src/tokens/ERC20.sol"; + +contract MorphoToken is ERC20 { + constructor(address _receiver) ERC20("Morpho Token", "MORPHO", 18) { + _mint(_receiver, 1_000_000_000 ether); + } +} diff --git a/certora/specs/MerkleTrees.spec b/certora/specs/MerkleTrees.spec new file mode 100644 index 000000000..bd92032eb --- /dev/null +++ b/certora/specs/MerkleTrees.spec @@ -0,0 +1,32 @@ +// SPDX-License-Identifier: AGPL-3.0-only + +methods { + function newInternalNode(address, MerkleTreeLib.InternalNode) external envfree; + + function getValue(address, address) external returns(uint256) envfree; + function isEmpty(address, address) external returns(bool) envfree; + function isWellFormed(address, address) external returns(bool) envfree; +} + +invariant zeroIsEmpty(address tree) + isEmpty(tree, 0); + +invariant nonEmptyHasValue(address tree, address addr) + ! isEmpty(tree, addr) => getValue(tree, addr) != 0 +{ preserved newInternalNode(address _, MerkleTreeLib.InternalNode internalNode) { + requireInvariant nonEmptyHasValue(tree, internalNode.left); + requireInvariant nonEmptyHasValue(tree, internalNode.right); + } +} + +invariant wellFormed(address tree, address addr) + isWellFormed(tree, addr) +{ preserved { + requireInvariant zeroIsEmpty(tree); + } + preserved newInternalNode(address _, MerkleTreeLib.InternalNode internalNode) { + requireInvariant zeroIsEmpty(tree); + requireInvariant nonEmptyHasValue(tree, internalNode.left); + requireInvariant nonEmptyHasValue(tree, internalNode.right); + } +} diff --git a/certora/specs/RewardsDistributor.spec b/certora/specs/RewardsDistributor.spec new file mode 100644 index 000000000..b625e6236 --- /dev/null +++ b/certora/specs/RewardsDistributor.spec @@ -0,0 +1,98 @@ +// SPDX-License-Identifier: AGPL-3.0-only + +using MerkleTrees as MerkleTrees; +using MorphoToken as MorphoToken; + +methods { + function prevRoot() external returns(bytes32) envfree; + function currRoot() external returns(bytes32) envfree; + function claimed(address) external returns(uint256) envfree; + function claim(address, uint256, bytes32[]) external envfree; + + function MerkleTrees.getValue(address, address) external returns(uint256) envfree; + function MerkleTrees.getHash(address, address) external returns(bytes32) envfree; + function MerkleTrees.wellFormedPath(address, address, bytes32[]) external envfree; + + function MorphoToken.balanceOf(address) external returns(uint256) envfree; +} + +// Check how updateRoot changes the storage. +rule updateRootStorageChange(env e, bytes32 _newRoot) { + bytes32 rootBefore = currRoot(); + + updateRoot(e, _newRoot); + + assert prevRoot() == rootBefore; + assert currRoot() == _newRoot; +} + +// Check an account claimed amount is correctly updated. +rule updatedClaimedAmount(address _account, uint256 _claimable, bytes32[] _proof) { + claim(_account, _claimable, _proof); + + assert _claimable == claimed(_account); +} + +// Check an account can only claim greater amounts each time. +rule increasingClaimedAmounts(address _account, uint256 _claimable, bytes32[] _proof) { + uint256 claimed = claimed(_account); + + claim(_account, _claimable, _proof); + + assert _claimable > claimed; +} + +// Check that claiming twice is equivalent to claiming once with the last amount. +rule claimTwice(address _account, uint256 _claim1, uint256 _claim2) { + storage initStorage = lastStorage; + + bytes32[] _proof1; bytes32[] _proof2; + claim(_account, _claim1, _proof1); + claim(_account, _claim2, _proof2); + assert _claim2 >= _claim1; + + storage afterBothStorage = lastStorage; + + bytes32[] _proof3; + claim(_account, _claim2, _proof3) at initStorage; + + assert lastStorage == afterBothStorage; +} + +// Check that the transferred amount is equal to the claimed amount minus the previous claimed amount. +rule transferredTokens(address _account, uint256 _claimable, bytes32[] _proof) { + // Assume that the rewards distributor itself is not receiving the tokens, to simplify this rule. + require _account != currentContract; + + uint256 balanceBefore = MorphoToken.balanceOf(_account); + uint256 claimedBefore = claimed(_account); + + // Safe require because the sum is capped by the total supply. + require balanceBefore + MorphoToken.balanceOf(currentContract) < 2^256; + + claim(_account, _claimable, _proof); + + uint256 balanceAfter = MorphoToken.balanceOf(_account); + + assert balanceAfter - balanceBefore == _claimable - claimedBefore; +} + +rule claimCorrectness(address _account, uint256 _claimable, bytes32[] _proof) { + address prevTree; address prevNode; + address currTree; address currNode; + + // Assume that prevRoot and currRoot correspond to prevTree and currTree. + require MerkleTrees.getHash(prevTree, prevNode) == prevRoot(); + require MerkleTrees.getHash(currTree, currNode) == currRoot(); + + // No need to make sure that currNode (resp prevNode) is equal to currRoot (resp prevRoot): one can pass an internal node instead. + + // Assume that prevTree and currTree are well-formed. + MerkleTrees.wellFormedPath(prevTree, prevNode, _proof); + MerkleTrees.wellFormedPath(currTree, currNode, _proof); + + claim(_account, _claimable, _proof); + + assert _claimable == MerkleTrees.getValue(prevTree, _account) || + _claimable == MerkleTrees.getValue(currTree, _account); +} diff --git a/foundry.toml b/foundry.toml index ea3ee9bd1..ae945ca94 100644 --- a/foundry.toml +++ b/foundry.toml @@ -19,3 +19,8 @@ fork_block_number = 15_581_371 [profile.aave-v2] fork_block_number = 15_581_371 # Block number when the Aave's V2 IRM was updated for the stETH. + +[profile.checker] +test = 'certora/checker' +fs_permissions = [{access = "read", path= "./certificate.json"}] +match_contract = 'Checker'