From 02d514d5a699ecec35037e28fbc840114cea3ec5 Mon Sep 17 00:00:00 2001 From: Adrien Husson Date: Wed, 30 Oct 2024 14:25:22 +0100 Subject: [PATCH] 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; }