Merge pull request #461 from morpho-org/feat/certora

Check non-view non-multicall functions are protected

.github/workflows/certora.yml

@@ -0,0 +1,49 @@
+name: Certora
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    strategy:
+      fail-fast: false
+
+      matrix:
+        conf:
+          - AaveV2MigrationBundlerV2
+          - AaveV3MigrationBundlerV2
+          - AaveV3OptimizerMigrationBundlerV2
+          - ChainAgnosticBundlerV2
+          - CompoundV2MigrationBundlerV2
+          - CompoundV3MigrationBundlerV2
+          - EthereumBundlerV2
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install python
+        uses: actions/setup-python@v5
+        with:
+          python-version: ">=3.11"
+
+      - name: Install certora
+        run: pip install certora-cli
+
+      - name: Install solc (0.8.24)
+        run: |
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.24/solc-static-linux
+          chmod +x solc-static-linux
+          sudo mv solc-static-linux /usr/local/bin/solc-0.8.24
+
+      - name: Verify ${{ matrix.conf }} specification
+        run: certoraRun certora/confs/${{ matrix.conf }}.conf
+        env:
+          CERTORAKEY: ${{ secrets.CERTORAKEY }}

.gitignore

@@ -30,3 +30,6 @@ node_modules/
 /artifacts
 
 *.log
+
+# Certora
+.certora_internal

certora/README.md

@@ -0,0 +1,35 @@
+# Bundlers formal verification
+
+This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index.html) specification and verification setup for the following bundler contracts:
+
+- [AaveV2MigrationBundlerV2](../src/migration/AaveV2MigrationBundlerV2.sol)
+- [AaveV3MigrationBundlerV2](../src/migration/AaveV3MigrationBundlerV2.sol)
+- [AaveV3OptimizerMigrationBundlerV2](../src/migration/AaveV3OptimizerMigrationBundlerV2.sol)
+- [ChainAgnosticBundlerV2](../src/chain-agnostic/ChainAgnosticBundlerV2.sol)
+- [CompoundV2MigrationBundlerV2](../src/migration/CompoundV2MigrationBundlerV2.sol)
+- [CompoundV3MigrationBundlerV2](../src/migration/CompoundV3MigrationBundlerV2.sol)
+- [EthereumBundlerV2](../src/ethereum/EthereumBundlerV2.sol)
+
+## Getting started
+
+To verify a specification, run the command `certoraRun Spec.conf` where `Spec.conf` is one of the configuration files in [`certora/confs`](confs).
+
+You must have set the `CERTORAKEY` environment variable to a valid Certora key.
+
+## Overview
+
+Bundler methods used during a bundle execution have the `protected` modifier. This modifier ensures that:
+- an initiator has been set;
+- the caller is the bundle initiator or the Morpho contract.
+
+The `Protected.spec` file checks that all bundler functions, except noted exceptions, respect the requirements of the `protected` modifier when an initiator has been set.
+
+## Verification architecture
+
+### Folders and file structure
+
+The [`certora/specs`](specs) folder contains the following files:
+
+- [`Protected.spec`](specs/Protected.spec) checks that all methods except noted exceptions respect the `protected` modifier when an initiator has been set.
+
+The [`certora/confs`](confs) folder contains a configuration file for each deployed bundler.

certora/confs/AaveV2MigrationBundlerV2.conf

@@ -0,0 +1,10 @@
+{
+  "files": [
+    "src/migration/AaveV2MigrationBundlerV2.sol"
+  ],
+  "solc": "solc-0.8.24",
+  "verify": "AaveV2MigrationBundlerV2:certora/specs/Protected.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Aave V2 Migration Bundler V2 protected functions"
+}

certora/confs/AaveV3MigrationBundlerV2.conf

@@ -0,0 +1,10 @@
+{
+  "files": [
+    "src/migration/AaveV3MigrationBundlerV2.sol"
+  ],
+  "solc": "solc-0.8.24",
+  "verify": "AaveV3MigrationBundlerV2:certora/specs/Protected.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Aave V3 Migration Bundler V2 protected functions"
+}

certora/confs/AaveV3OptimizerMigrationBundlerV2.conf

@@ -0,0 +1,10 @@
+{
+  "files": [
+    "src/migration/AaveV3OptimizerMigrationBundlerV2.sol"
+  ],
+  "solc": "solc-0.8.24",
+  "verify": "AaveV3OptimizerMigrationBundlerV2:certora/specs/Protected.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Aave V3 Optimizer Migration Bundler V2 protected functions"
+}

certora/confs/ChainAgnosticBundlerV2.conf

@@ -0,0 +1,10 @@
+{
+  "files": [
+    "src/chain-agnostic/ChainAgnosticBundlerV2.sol"
+  ],
+  "solc": "solc-0.8.24",
+  "verify": "ChainAgnosticBundlerV2:certora/specs/Protected.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Chain Agnostic Bundler V2 protected functions"
+}

certora/confs/CompoundV2MigrationBundlerV2.conf

@@ -0,0 +1,10 @@
+{
+  "files": [
+    "src/migration/CompoundV2MigrationBundlerV2.sol"
+  ],
+  "solc": "solc-0.8.24",
+  "verify": "CompoundV2MigrationBundlerV2:certora/specs/Protected.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Compound V2 Migration Bundler V2 protected functions"
+}

certora/confs/CompoundV3MigrationBundlerV2.conf

@@ -0,0 +1,10 @@
+{
+  "files": [
+    "src/migration/CompoundV3MigrationBundlerV2.sol"
+  ],
+  "solc": "solc-0.8.24",
+  "verify": "CompoundV3MigrationBundlerV2:certora/specs/Protected.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Compound V3 Migration Bundler V2 protected functions"
+}

certora/confs/EthereumBundlerV2.conf

@@ -0,0 +1,10 @@
+{
+  "files": [
+    "src/ethereum/EthereumBundlerV2.sol"
+  ],
+  "solc": "solc-0.8.24",
+  "verify": "EthereumBundlerV2:certora/specs/Protected.spec",
+  "rule_sanity": "basic",
+  "server": "production",
+  "msg": "Ethereum Bundler V2 protected functions"
+}

certora/specs/Protected.spec

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+// Check that all methods except those noted below comply with the `protected` modifier when an initiator has been set.
+rule protectedWithSetInitiator(method f, env e, calldataarg data) filtered {
+    // Do not check view functions.
+    f -> !f.isView &&
+    // Do not check the fallback function.
+    !f.isFallback &&
+    // Do not check multicall, which is used to start a new bundle.
+    f.selector != sig:multicall(bytes[]).selector
+}
+{
+    // Safe require because `protected` functions should be callable by the initiator.
+    require e.msg.sender != currentContract._initiator;
+    // Safe require because `protected` functions should be callable by Morpho.
+    require e.msg.sender != currentContract.MORPHO;
+    f@withrevert(e,data);
+    assert lastReverted;
+}