From 2704ea35882e7eaecd469d45ba7c5e7f1f734435 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Tue, 29 Oct 2024 17:15:29 +0100 Subject: [PATCH 1/5] test: check non-view non-multicall functions are protected for all bundlers --- .github/workflows/certora.yml | 49 +++++++++++++++++++ .gitignore | 3 ++ certora/confs/AaveV2MigrationBundlerV2.conf | 10 ++++ certora/confs/AaveV3MigrationBundlerV2.conf | 10 ++++ .../AaveV3OptimizerMigrationBundlerV2.conf | 10 ++++ certora/confs/ChainAgnosticBundlerV2.conf | 10 ++++ .../confs/CompoundV2MigrationBundlerV2.conf | 10 ++++ .../confs/CompoundV3MigrationBundlerV2.conf | 10 ++++ certora/confs/EthereumBundlerV2.conf | 10 ++++ certora/harness/Constants.sol | 8 +++ certora/specs/Protected.spec | 20 ++++++++ 11 files changed, 150 insertions(+) create mode 100644 .github/workflows/certora.yml create mode 100644 certora/confs/AaveV2MigrationBundlerV2.conf create mode 100644 certora/confs/AaveV3MigrationBundlerV2.conf create mode 100644 certora/confs/AaveV3OptimizerMigrationBundlerV2.conf create mode 100644 certora/confs/ChainAgnosticBundlerV2.conf create mode 100644 certora/confs/CompoundV2MigrationBundlerV2.conf create mode 100644 certora/confs/CompoundV3MigrationBundlerV2.conf create mode 100644 certora/confs/EthereumBundlerV2.conf create mode 100644 certora/harness/Constants.sol create mode 100644 certora/specs/Protected.spec diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 00000000..ff43b7da --- /dev/null +++ b/.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 }} diff --git a/.gitignore b/.gitignore index b9f2db94..4a6d1c36 100644 --- a/.gitignore +++ b/.gitignore @@ -30,3 +30,6 @@ node_modules/ /artifacts *.log + +# Certora +.certora_internal diff --git a/certora/confs/AaveV2MigrationBundlerV2.conf b/certora/confs/AaveV2MigrationBundlerV2.conf new file mode 100644 index 00000000..bf9c9c0a --- /dev/null +++ b/certora/confs/AaveV2MigrationBundlerV2.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "src/migration/AaveV2MigrationBundlerV2.sol", + "certora/harness/Constants.sol" + ], + "verify": "AaveV2MigrationBundlerV2:certora/specs/Protected.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Aave V2 Migration Bundler V2 protected functions" +} diff --git a/certora/confs/AaveV3MigrationBundlerV2.conf b/certora/confs/AaveV3MigrationBundlerV2.conf new file mode 100644 index 00000000..7dc2f5b5 --- /dev/null +++ b/certora/confs/AaveV3MigrationBundlerV2.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "src/migration/AaveV3MigrationBundlerV2.sol", + "certora/harness/Constants.sol" + ], + "verify": "AaveV3MigrationBundlerV2:certora/specs/Protected.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Aave V3 Migration Bundler V2 protected functions" +} diff --git a/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf b/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf new file mode 100644 index 00000000..f2a0ccb2 --- /dev/null +++ b/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "src/migration/AaveV3OptimizerMigrationBundlerV2.sol", + "certora/harness/Constants.sol" + ], + "verify": "AaveV3OptimizerMigrationBundlerV2:certora/specs/Protected.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Aave V3 Optimizer Migration Bundler V2 protected functions" +} diff --git a/certora/confs/ChainAgnosticBundlerV2.conf b/certora/confs/ChainAgnosticBundlerV2.conf new file mode 100644 index 00000000..082951a7 --- /dev/null +++ b/certora/confs/ChainAgnosticBundlerV2.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "src/chain-agnostic/ChainAgnosticBundlerV2.sol", + "certora/harness/Constants.sol" + ], + "verify": "ChainAgnosticBundlerV2:certora/specs/Protected.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Chain Agnostic Bundler V2 protected functions" +} diff --git a/certora/confs/CompoundV2MigrationBundlerV2.conf b/certora/confs/CompoundV2MigrationBundlerV2.conf new file mode 100644 index 00000000..51b0a45f --- /dev/null +++ b/certora/confs/CompoundV2MigrationBundlerV2.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "src/migration/CompoundV2MigrationBundlerV2.sol", + "certora/harness/Constants.sol" + ], + "verify": "CompoundV2MigrationBundlerV2:certora/specs/Protected.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Compound V2 Migration Bundler V2 protected functions" +} diff --git a/certora/confs/CompoundV3MigrationBundlerV2.conf b/certora/confs/CompoundV3MigrationBundlerV2.conf new file mode 100644 index 00000000..06a390fb --- /dev/null +++ b/certora/confs/CompoundV3MigrationBundlerV2.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "src/migration/CompoundV3MigrationBundlerV2.sol", + "certora/harness/Constants.sol" + ], + "verify": "CompoundV3MigrationBundlerV2:certora/specs/Protected.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Compound V3 Migration Bundler V2 protected functions" +} diff --git a/certora/confs/EthereumBundlerV2.conf b/certora/confs/EthereumBundlerV2.conf new file mode 100644 index 00000000..4e3e2369 --- /dev/null +++ b/certora/confs/EthereumBundlerV2.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "src/ethereum/EthereumBundlerV2.sol", + "certora/harness/Constants.sol" + ], + "verify": "EthereumBundlerV2:certora/specs/Protected.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Ethereum Bundler V2 protected functions" +} diff --git a/certora/harness/Constants.sol b/certora/harness/Constants.sol new file mode 100644 index 00000000..a524aefe --- /dev/null +++ b/certora/harness/Constants.sol @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity 0.8.24; + +import "../../src/libraries/ConstantsLib.sol" as ConstantsLib; + +contract Constants { + address public constant UNSET_INITIATOR = ConstantsLib.UNSET_INITIATOR; +} diff --git a/certora/specs/Protected.spec b/certora/specs/Protected.spec new file mode 100644 index 00000000..6528bd2c --- /dev/null +++ b/certora/specs/Protected.spec @@ -0,0 +1,20 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +using Constants as constants; + +methods { + function initiator() external returns(address) envfree; + function MORPHO() external returns(address) envfree; + function constants.UNSET_INITIATOR() external returns(address) envfree; +} + + +rule protectedMethodsComplete(method f, env e, calldataarg data) filtered { + f -> !f.isView && !f.isFallback && f.selector != sig:multicall(bytes[]).selector +} +{ + require e.msg.sender != constants.UNSET_INITIATOR(); + require e.msg.sender != initiator(); + require e.msg.sender != MORPHO(); + f@withrevert(e,data); + assert lastReverted; +} From 8603571928c8d48b1e737116e8f2fa5a00ed2790 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Tue, 29 Oct 2024 18:21:10 +0100 Subject: [PATCH 2/5] docs: add README.md & docs, fix workflow file --- .github/workflows/certora.yml | 2 +- certora/README.md | 35 +++++++++++++++++++++++++++++++++++ certora/specs/Protected.spec | 6 +++++- 3 files changed, 41 insertions(+), 2 deletions(-) create mode 100644 certora/README.md diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index ff43b7da..236954b8 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -41,7 +41,7 @@ jobs: 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 + sudo mv solc-static-linux /usr/local/bin/solc - name: Verify ${{ matrix.conf }} specification run: certoraRun certora/confs/${{ matrix.conf }}.conf diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 00000000..0a8da460 --- /dev/null +++ b/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, and +- 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. diff --git a/certora/specs/Protected.spec b/certora/specs/Protected.spec index 6528bd2c..9d266df7 100644 --- a/certora/specs/Protected.spec +++ b/certora/specs/Protected.spec @@ -8,7 +8,11 @@ methods { } -rule protectedMethodsComplete(method f, env e, calldataarg data) filtered { +// 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. + // Do not check the fallback function. + // Do not check multicall, which is used to start a new bundle. f -> !f.isView && !f.isFallback && f.selector != sig:multicall(bytes[]).selector } { From e997f43d0787f6ce0e1a35a302666284375419fe Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Tue, 29 Oct 2024 23:02:45 +0100 Subject: [PATCH 3/5] fix: remove unset_initiator require --- certora/confs/AaveV2MigrationBundlerV2.conf | 3 +-- certora/confs/AaveV3MigrationBundlerV2.conf | 3 +-- certora/confs/AaveV3OptimizerMigrationBundlerV2.conf | 3 +-- certora/confs/ChainAgnosticBundlerV2.conf | 3 +-- certora/confs/CompoundV2MigrationBundlerV2.conf | 3 +-- certora/confs/CompoundV3MigrationBundlerV2.conf | 3 +-- certora/confs/EthereumBundlerV2.conf | 3 +-- certora/harness/Constants.sol | 8 -------- certora/specs/Protected.spec | 4 ---- 9 files changed, 7 insertions(+), 26 deletions(-) delete mode 100644 certora/harness/Constants.sol diff --git a/certora/confs/AaveV2MigrationBundlerV2.conf b/certora/confs/AaveV2MigrationBundlerV2.conf index bf9c9c0a..3661f225 100644 --- a/certora/confs/AaveV2MigrationBundlerV2.conf +++ b/certora/confs/AaveV2MigrationBundlerV2.conf @@ -1,7 +1,6 @@ { "files": [ - "src/migration/AaveV2MigrationBundlerV2.sol", - "certora/harness/Constants.sol" + "src/migration/AaveV2MigrationBundlerV2.sol" ], "verify": "AaveV2MigrationBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", diff --git a/certora/confs/AaveV3MigrationBundlerV2.conf b/certora/confs/AaveV3MigrationBundlerV2.conf index 7dc2f5b5..02346908 100644 --- a/certora/confs/AaveV3MigrationBundlerV2.conf +++ b/certora/confs/AaveV3MigrationBundlerV2.conf @@ -1,7 +1,6 @@ { "files": [ - "src/migration/AaveV3MigrationBundlerV2.sol", - "certora/harness/Constants.sol" + "src/migration/AaveV3MigrationBundlerV2.sol" ], "verify": "AaveV3MigrationBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", diff --git a/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf b/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf index f2a0ccb2..783266a1 100644 --- a/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf +++ b/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf @@ -1,7 +1,6 @@ { "files": [ - "src/migration/AaveV3OptimizerMigrationBundlerV2.sol", - "certora/harness/Constants.sol" + "src/migration/AaveV3OptimizerMigrationBundlerV2.sol" ], "verify": "AaveV3OptimizerMigrationBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", diff --git a/certora/confs/ChainAgnosticBundlerV2.conf b/certora/confs/ChainAgnosticBundlerV2.conf index 082951a7..5a6ba6b3 100644 --- a/certora/confs/ChainAgnosticBundlerV2.conf +++ b/certora/confs/ChainAgnosticBundlerV2.conf @@ -1,7 +1,6 @@ { "files": [ - "src/chain-agnostic/ChainAgnosticBundlerV2.sol", - "certora/harness/Constants.sol" + "src/chain-agnostic/ChainAgnosticBundlerV2.sol" ], "verify": "ChainAgnosticBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", diff --git a/certora/confs/CompoundV2MigrationBundlerV2.conf b/certora/confs/CompoundV2MigrationBundlerV2.conf index 51b0a45f..58b938a5 100644 --- a/certora/confs/CompoundV2MigrationBundlerV2.conf +++ b/certora/confs/CompoundV2MigrationBundlerV2.conf @@ -1,7 +1,6 @@ { "files": [ - "src/migration/CompoundV2MigrationBundlerV2.sol", - "certora/harness/Constants.sol" + "src/migration/CompoundV2MigrationBundlerV2.sol" ], "verify": "CompoundV2MigrationBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", diff --git a/certora/confs/CompoundV3MigrationBundlerV2.conf b/certora/confs/CompoundV3MigrationBundlerV2.conf index 06a390fb..5a379797 100644 --- a/certora/confs/CompoundV3MigrationBundlerV2.conf +++ b/certora/confs/CompoundV3MigrationBundlerV2.conf @@ -1,7 +1,6 @@ { "files": [ - "src/migration/CompoundV3MigrationBundlerV2.sol", - "certora/harness/Constants.sol" + "src/migration/CompoundV3MigrationBundlerV2.sol" ], "verify": "CompoundV3MigrationBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", diff --git a/certora/confs/EthereumBundlerV2.conf b/certora/confs/EthereumBundlerV2.conf index 4e3e2369..2d144f99 100644 --- a/certora/confs/EthereumBundlerV2.conf +++ b/certora/confs/EthereumBundlerV2.conf @@ -1,7 +1,6 @@ { "files": [ - "src/ethereum/EthereumBundlerV2.sol", - "certora/harness/Constants.sol" + "src/ethereum/EthereumBundlerV2.sol" ], "verify": "EthereumBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", diff --git a/certora/harness/Constants.sol b/certora/harness/Constants.sol deleted file mode 100644 index a524aefe..00000000 --- a/certora/harness/Constants.sol +++ /dev/null @@ -1,8 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0-or-later -pragma solidity 0.8.24; - -import "../../src/libraries/ConstantsLib.sol" as ConstantsLib; - -contract Constants { - address public constant UNSET_INITIATOR = ConstantsLib.UNSET_INITIATOR; -} diff --git a/certora/specs/Protected.spec b/certora/specs/Protected.spec index 9d266df7..3a6237a5 100644 --- a/certora/specs/Protected.spec +++ b/certora/specs/Protected.spec @@ -1,10 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later -using Constants as constants; - methods { function initiator() external returns(address) envfree; function MORPHO() external returns(address) envfree; - function constants.UNSET_INITIATOR() external returns(address) envfree; } @@ -16,7 +13,6 @@ rule protectedWithSetInitiator(method f, env e, calldataarg data) filtered { f -> !f.isView && !f.isFallback && f.selector != sig:multicall(bytes[]).selector } { - require e.msg.sender != constants.UNSET_INITIATOR(); require e.msg.sender != initiator(); require e.msg.sender != MORPHO(); f@withrevert(e,data); From 02d514d5a699ecec35037e28fbc840114cea3ec5 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 30 Oct 2024 14:25:22 +0100 Subject: [PATCH 4/5] fix: address PR review --- .github/workflows/certora.yml | 2 +- certora/README.md | 4 ++-- certora/confs/AaveV2MigrationBundlerV2.conf | 1 + certora/confs/AaveV3MigrationBundlerV2.conf | 1 + certora/confs/AaveV3OptimizerMigrationBundlerV2.conf | 1 + certora/confs/ChainAgnosticBundlerV2.conf | 1 + certora/confs/CompoundV2MigrationBundlerV2.conf | 1 + certora/confs/CompoundV3MigrationBundlerV2.conf | 1 + certora/confs/EthereumBundlerV2.conf | 1 + certora/specs/Protected.spec | 5 ++--- 10 files changed, 12 insertions(+), 6 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 236954b8..ff43b7da 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -41,7 +41,7 @@ jobs: 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 + sudo mv solc-static-linux /usr/local/bin/solc-0.8.24 - name: Verify ${{ matrix.conf }} specification run: certoraRun certora/confs/${{ matrix.conf }}.conf diff --git a/certora/README.md b/certora/README.md index 0a8da460..d7302afa 100644 --- a/certora/README.md +++ b/certora/README.md @@ -10,7 +10,7 @@ This folder contains the [CVL](https://docs.certora.com/en/latest/docs/cvl/index - [CompoundV3MigrationBundlerV2](../src/migration/CompoundV3MigrationBundlerV2.sol) - [EthereumBundlerV2](../src/ethereum/EthereumBundlerV2.sol) -## Getting Started +## 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). @@ -19,7 +19,7 @@ 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, and +- 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. diff --git a/certora/confs/AaveV2MigrationBundlerV2.conf b/certora/confs/AaveV2MigrationBundlerV2.conf index 3661f225..a80ab53d 100644 --- a/certora/confs/AaveV2MigrationBundlerV2.conf +++ b/certora/confs/AaveV2MigrationBundlerV2.conf @@ -2,6 +2,7 @@ "files": [ "src/migration/AaveV2MigrationBundlerV2.sol" ], + "solc": "solc-0.8.24", "verify": "AaveV2MigrationBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", "server": "production", diff --git a/certora/confs/AaveV3MigrationBundlerV2.conf b/certora/confs/AaveV3MigrationBundlerV2.conf index 02346908..40a072c1 100644 --- a/certora/confs/AaveV3MigrationBundlerV2.conf +++ b/certora/confs/AaveV3MigrationBundlerV2.conf @@ -2,6 +2,7 @@ "files": [ "src/migration/AaveV3MigrationBundlerV2.sol" ], + "solc": "solc-0.8.24", "verify": "AaveV3MigrationBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", "server": "production", diff --git a/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf b/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf index 783266a1..650467c6 100644 --- a/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf +++ b/certora/confs/AaveV3OptimizerMigrationBundlerV2.conf @@ -2,6 +2,7 @@ "files": [ "src/migration/AaveV3OptimizerMigrationBundlerV2.sol" ], + "solc": "solc-0.8.24", "verify": "AaveV3OptimizerMigrationBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", "server": "production", diff --git a/certora/confs/ChainAgnosticBundlerV2.conf b/certora/confs/ChainAgnosticBundlerV2.conf index 5a6ba6b3..deb09cae 100644 --- a/certora/confs/ChainAgnosticBundlerV2.conf +++ b/certora/confs/ChainAgnosticBundlerV2.conf @@ -2,6 +2,7 @@ "files": [ "src/chain-agnostic/ChainAgnosticBundlerV2.sol" ], + "solc": "solc-0.8.24", "verify": "ChainAgnosticBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", "server": "production", diff --git a/certora/confs/CompoundV2MigrationBundlerV2.conf b/certora/confs/CompoundV2MigrationBundlerV2.conf index 58b938a5..291c7e8e 100644 --- a/certora/confs/CompoundV2MigrationBundlerV2.conf +++ b/certora/confs/CompoundV2MigrationBundlerV2.conf @@ -2,6 +2,7 @@ "files": [ "src/migration/CompoundV2MigrationBundlerV2.sol" ], + "solc": "solc-0.8.24", "verify": "CompoundV2MigrationBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", "server": "production", diff --git a/certora/confs/CompoundV3MigrationBundlerV2.conf b/certora/confs/CompoundV3MigrationBundlerV2.conf index 5a379797..61c11ed4 100644 --- a/certora/confs/CompoundV3MigrationBundlerV2.conf +++ b/certora/confs/CompoundV3MigrationBundlerV2.conf @@ -2,6 +2,7 @@ "files": [ "src/migration/CompoundV3MigrationBundlerV2.sol" ], + "solc": "solc-0.8.24", "verify": "CompoundV3MigrationBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", "server": "production", diff --git a/certora/confs/EthereumBundlerV2.conf b/certora/confs/EthereumBundlerV2.conf index 2d144f99..d847e5aa 100644 --- a/certora/confs/EthereumBundlerV2.conf +++ b/certora/confs/EthereumBundlerV2.conf @@ -2,6 +2,7 @@ "files": [ "src/ethereum/EthereumBundlerV2.sol" ], + "solc": "solc-0.8.24", "verify": "EthereumBundlerV2:certora/specs/Protected.spec", "rule_sanity": "basic", "server": "production", diff --git a/certora/specs/Protected.spec b/certora/specs/Protected.spec index 3a6237a5..138a1aa5 100644 --- a/certora/specs/Protected.spec +++ b/certora/specs/Protected.spec @@ -13,8 +13,7 @@ rule protectedWithSetInitiator(method f, env e, calldataarg data) filtered { f -> !f.isView && !f.isFallback && f.selector != sig:multicall(bytes[]).selector } { - require e.msg.sender != initiator(); - require e.msg.sender != MORPHO(); f@withrevert(e,data); - assert lastReverted; + bool reverted = lastReverted; + assert e.msg.sender != initiator() && e.msg.sender != MORPHO() => reverted; } From 79873ea9a3e4af43e7fcadf4475747f73b638799 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 30 Oct 2024 19:43:46 +0100 Subject: [PATCH 5/5] fix: address more PR reviews --- certora/README.md | 2 +- certora/specs/Protected.spec | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/certora/README.md b/certora/README.md index d7302afa..7f042841 100644 --- a/certora/README.md +++ b/certora/README.md @@ -1,4 +1,4 @@ -# Bundlers Formal Verification +# 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: diff --git a/certora/specs/Protected.spec b/certora/specs/Protected.spec index 138a1aa5..bcc8dc12 100644 --- a/certora/specs/Protected.spec +++ b/certora/specs/Protected.spec @@ -1,19 +1,19 @@ // SPDX-License-Identifier: GPL-2.0-or-later -methods { - function initiator() external returns(address) envfree; - function MORPHO() external returns(address) envfree; -} - // 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 -> !f.isView && !f.isFallback && f.selector != sig:multicall(bytes[]).selector + 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); - bool reverted = lastReverted; - assert e.msg.sender != initiator() && e.msg.sender != MORPHO() => reverted; + assert lastReverted; }