From fddfd1478471b92c90f9f2ad38be3a531c908135 Mon Sep 17 00:00:00 2001 From: Shebin John Date: Mon, 16 Sep 2024 12:53:49 +0200 Subject: [PATCH] Migration Contract FV (#832) Based on #829 Some extra changes: - Adding FV to Certora Workflow - Remove the unused `data` from the `SafeMock`. - EOF and some capitalization changes - Parametric argument to some rules --------- Co-authored-by: Hristo Grigorov Co-authored-by: Nicholas Rodrigues Lordello --- .github/workflows/certora.yml | 2 +- certora/conf/safeMigration.conf | 15 ++++ certora/conf/safeToL2Migration.conf | 16 ++++ certora/conf/safeToL2Setup.conf | 15 ++++ certora/mocks/SafeMock.sol | 106 +++++++++++++++++++++++++++ certora/specs/ModuleReach.spec | 2 +- certora/specs/SafeMigration.spec | 74 +++++++++++++++++++ certora/specs/SafeToL2Migration.spec | 64 ++++++++++++++++ certora/specs/SafeToL2Setup.spec | 43 +++++++++++ 9 files changed, 335 insertions(+), 2 deletions(-) create mode 100644 certora/conf/safeMigration.conf create mode 100644 certora/conf/safeToL2Migration.conf create mode 100644 certora/conf/safeToL2Setup.conf create mode 100644 certora/mocks/SafeMock.sol create mode 100644 certora/specs/SafeMigration.spec create mode 100644 certora/specs/SafeToL2Migration.spec create mode 100644 certora/specs/SafeToL2Setup.spec diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 03908144a..acabfb8aa 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -15,7 +15,7 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - rule: ["owner", "safe", "module", "nativeTokenRefund", "signatures"] + rule: ["owner", "safe", "module", "nativeTokenRefund", "signatures", "safeMigration", "safeToL2Migration", "safeToL2Setup"] steps: - uses: actions/checkout@v4 diff --git a/certora/conf/safeMigration.conf b/certora/conf/safeMigration.conf new file mode 100644 index 000000000..957197bf9 --- /dev/null +++ b/certora/conf/safeMigration.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "contracts/libraries/SafeMigration.sol", + "certora/mocks/SafeMock.sol", + ], + "link": [ + "SafeMock:impl=SafeMigration" + ], + "loop_iter": "3", + "msg": "SafeMigration", + "optimistic_hashing": true, + "process": "emv", + "solc": "solc7.6", + "verify": "SafeMigration:certora/specs/SafeMigration.spec" +} \ No newline at end of file diff --git a/certora/conf/safeToL2Migration.conf b/certora/conf/safeToL2Migration.conf new file mode 100644 index 000000000..478529310 --- /dev/null +++ b/certora/conf/safeToL2Migration.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "contracts/libraries/SafeToL2Migration.sol", + "certora/mocks/SafeMock.sol", + ], + "link": [ + "SafeMock:impl=SafeToL2Migration" + ], + "loop_iter": "3", + "msg": "SafeToL2Migration", + "optimistic_hashing": true, + "optimistic_loop": true, + "process": "emv", + "solc": "solc7.6", + "verify": "SafeToL2Migration:certora/specs/SafeToL2Migration.spec" +} \ No newline at end of file diff --git a/certora/conf/safeToL2Setup.conf b/certora/conf/safeToL2Setup.conf new file mode 100644 index 000000000..5f302c41b --- /dev/null +++ b/certora/conf/safeToL2Setup.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "contracts/libraries/SafeToL2Setup.sol", + "certora/mocks/SafeMock.sol" + ], + "link": [ + "SafeMock:impl=SafeToL2Setup" + ], + "loop_iter": "3", + "msg": "SafeToL2Setup", + "optimistic_hashing": true, + "process": "emv", + "solc": "solc7.6", + "verify": "SafeToL2Setup:certora/specs/SafeToL2Setup.spec" +} \ No newline at end of file diff --git a/certora/mocks/SafeMock.sol b/certora/mocks/SafeMock.sol new file mode 100644 index 000000000..c8e568266 --- /dev/null +++ b/certora/mocks/SafeMock.sol @@ -0,0 +1,106 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity >=0.7.0 <0.9.0; + +import {SafeStorage} from "../../contracts/libraries/SafeStorage.sol"; + +contract SafeMock is SafeStorage { + + address public impl; + address public fallbackHandler; + + function setFallbackHandler(address a) public { + fallbackHandler = a; + } + + function getFallbackHandler() public view returns (address) { + return fallbackHandler; + } + + function getNonce() public view returns (uint256) { + return nonce; + } + + function getSingleton() public view returns (address) { + return singleton; + } + + function getChainId() public view returns (uint256 result) { + /* solhint-disable no-inline-assembly */ + /// @solidity memory-safe-assembly + assembly { + result := chainid() + } + /* solhint-enable no-inline-assembly */ + } + + function delegateCallSetupToL2(address l2Singleton) public { + (bool success, ) = impl.delegatecall( + abi.encodeWithSignature("setupToL2(address)", l2Singleton) + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateSingleton() public { + (bool success, ) = impl.delegatecall( + abi.encodeWithSignature("migrateSingleton()") + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateWithFallbackHandler() public { + (bool success, ) = impl.delegatecall( + abi.encodeWithSignature("migrateWithFallbackHandler()") + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateL2Singleton() public { + (bool success, ) = impl.delegatecall( + abi.encodeWithSignature("migrateL2Singleton()") + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateL2WithFallbackHandler() public { + (bool success, ) = impl.delegatecall( + abi.encodeWithSignature("migrateL2WithFallbackHandler()") + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateToL2(address l2Singleton) public { + (bool success, ) = impl.delegatecall( + abi.encodeWithSignature("migrateToL2(address)", l2Singleton) + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateFromV111(address l2Singleton, address fallbackHandlerAddr) public { + (bool success, ) = impl.delegatecall( + abi.encodeWithSignature("migrateFromV111(address,address)", l2Singleton, fallbackHandlerAddr) + ); + + if (!success) { + revert("Something went wrong"); + } + } + +} diff --git a/certora/specs/ModuleReach.spec b/certora/specs/ModuleReach.spec index b5cb9eac4..0266e7ef0 100644 --- a/certora/specs/ModuleReach.spec +++ b/certora/specs/ModuleReach.spec @@ -235,4 +235,4 @@ rule disableModuleDisablesModule { assert !isModuleEnabled(toRemove), "disableModule should disable module"; assert isModuleEnabled(other) == isModuleEnabledBefore, "disableModule should not change other modules"; -} \ No newline at end of file +} diff --git a/certora/specs/SafeMigration.spec b/certora/specs/SafeMigration.spec new file mode 100644 index 000000000..1bb203ac5 --- /dev/null +++ b/certora/specs/SafeMigration.spec @@ -0,0 +1,74 @@ +using SafeMigration as SafeMigration; +using SafeMock as SafeMock; + +methods { + function _.setFallbackHandler(address) external => DISPATCHER(true); +} + +// MIGRATION_SINGLETON is always the current contract +invariant MIGRATION_SINGLETONisAlwaysCurrentContract() + SafeMigration.MIGRATION_SINGLETON == SafeMigration; + + +// All the function that are not view function will revert (if it is not delegateCall) +rule allNonViewFunctionRevert(env e, method f, calldataarg args) filtered { f -> !f.isView } { + requireInvariant MIGRATION_SINGLETONisAlwaysCurrentContract; + SafeMigration.f@withrevert(e,args); + assert lastReverted; +} + + +// Safe's singleton address update integrity (parametric version) +rule singletonMigrationIntegrityParametric(env e, method f, calldataarg args) filtered { + f -> f.selector == sig:SafeMock.delegateMigrateSingleton().selector + || f.selector == sig:SafeMock.delegateMigrateWithFallbackHandler().selector + || f.selector == sig:SafeMock.delegateMigrateL2Singleton().selector + || f.selector == sig:SafeMock.delegateMigrateL2WithFallbackHandler().selector + } { + address singletonBefore = SafeMock.getSingleton(e); + + SafeMock.f@withrevert(e, args); + bool callReverted = lastReverted; + + address singletonAfter = SafeMock.getSingleton(e); + + assert !callReverted && + (f.selector == sig:SafeMock.delegateMigrateSingleton().selector || + f.selector == sig:SafeMock.delegateMigrateWithFallbackHandler().selector) => + singletonAfter == SafeMigration.SAFE_SINGLETON(e); + + assert !callReverted && + (f.selector == sig:SafeMock.delegateMigrateL2Singleton().selector || + f.selector == sig:SafeMock.delegateMigrateL2WithFallbackHandler().selector) => + singletonAfter == SafeMigration.SAFE_L2_SINGLETON(e); + + assert callReverted => singletonAfter == singletonBefore; +} + + +// Safe's fallbackHandler address update integrity (parametric version) +rule fallbackHandlerMigrationIntegrityParametric(env e, method f, calldataarg args) filtered { + f -> f.selector == sig:SafeMock.delegateMigrateSingleton().selector + || f.selector == sig:SafeMock.delegateMigrateWithFallbackHandler().selector + || f.selector == sig:SafeMock.delegateMigrateL2Singleton().selector + || f.selector == sig:SafeMock.delegateMigrateL2WithFallbackHandler().selector + } { + address fallbackHandlerBefore = SafeMock.getFallbackHandler(e); + + SafeMock.f@withrevert(e, args); + bool callReverted = lastReverted; + + address fallbackHandlerAfter = SafeMock.getFallbackHandler(e); + + assert !callReverted && + (f.selector == sig:SafeMock.delegateMigrateWithFallbackHandler().selector || + f.selector == sig:SafeMock.delegateMigrateL2WithFallbackHandler().selector) => + fallbackHandlerAfter == SafeMigration.SAFE_FALLBACK_HANDLER(e); + + assert !callReverted && + (f.selector == sig:SafeMock.delegateMigrateSingleton().selector || + f.selector == sig:SafeMock.delegateMigrateL2Singleton().selector) => + fallbackHandlerAfter == fallbackHandlerBefore; + + assert callReverted => fallbackHandlerAfter == fallbackHandlerBefore; +} diff --git a/certora/specs/SafeToL2Migration.spec b/certora/specs/SafeToL2Migration.spec new file mode 100644 index 000000000..1f322356a --- /dev/null +++ b/certora/specs/SafeToL2Migration.spec @@ -0,0 +1,64 @@ +using SafeToL2Migration as SafeToL2Migration; +using SafeMock as SafeMock; + +methods { + function _.setFallbackHandler(address) external => DISPATCHER(true); +} + +// MIGRATION_SINGLETON is always the current contract +invariant MIGRATION_SINGLETONisAlwaysCurrentContract() + SafeToL2Migration.MIGRATION_SINGLETON == SafeToL2Migration; + + +// All the function that are not view function will revert (if it is not delegateCall) +rule allNonViewFunctionRevert(env e, method f, calldataarg args) filtered { f -> !f.isView } { + requireInvariant MIGRATION_SINGLETONisAlwaysCurrentContract; + SafeToL2Migration.f@withrevert(e,args); + assert lastReverted; +} + +// Calls to migrateToL2() and migrateFromV111() can succeed only if Safe's nonce is correct +rule nonceMustBeCorrect(env e, method f, calldataarg args) filtered { + f -> f.selector == sig:SafeMock.delegateMigrateToL2(address).selector + || f.selector == sig:SafeMock.delegateMigrateFromV111(address,address).selector + } { + // get current nonce of the Safe contract + uint256 currentNonce = SafeMock.getNonce(e); + + SafeMock.f@withrevert(e, args); + bool callReverted = lastReverted; + + assert !callReverted => currentNonce == 1; +} + +// Correct update of Safe's singleton address by migrateToL2() +rule singletonMigrateToL2Integrity(env e, address l2Singleton) { + address singletonBefore = SafeMock.getSingleton(e); + + SafeMock.delegateMigrateToL2@withrevert(e, l2Singleton); + bool callReverted = lastReverted; + + address singletonAfter = SafeMock.getSingleton(e); + + assert !callReverted => singletonAfter == l2Singleton; + assert callReverted => singletonAfter == singletonBefore; +} + + +// Correct update of Safe's singleton address and fallbackHandler address by migrateFromV111() +rule singletonMigrateFromV111Integrity(env e, address l2Singleton, address fallbackHandlerAddr) { + address singletonBefore = SafeMock.getSingleton(e); + address fallbackHandlerBefore = SafeMock.getFallbackHandler(e); + + SafeMock.delegateMigrateFromV111@withrevert(e, l2Singleton, fallbackHandlerAddr); + bool callReverted = lastReverted; + + address singletonAfter = SafeMock.getSingleton(e); + address fallbackHandlerAfter = SafeMock.getFallbackHandler(e); + + assert !callReverted => singletonAfter == l2Singleton; + assert !callReverted => fallbackHandlerAfter == fallbackHandlerAddr; + + assert callReverted => singletonAfter == singletonBefore; + assert callReverted => fallbackHandlerAfter == fallbackHandlerBefore; +} diff --git a/certora/specs/SafeToL2Setup.spec b/certora/specs/SafeToL2Setup.spec new file mode 100644 index 000000000..6408df5c8 --- /dev/null +++ b/certora/specs/SafeToL2Setup.spec @@ -0,0 +1,43 @@ +using SafeToL2Setup as SafeToL2Setup; +using SafeMock as SafeMock; + +// _SELF is always the current contract +// if the "rule_sanity": "basic" flag is enabled this rule would fail sanity check +invariant _SELFisAlwaysCurrentContract() + SafeToL2Setup.SELF == SafeToL2Setup; + + +// All the non-view functions will revert when called directly (only delegateCall is allowed) +rule allNonViewFunctionRevert(env e, method f, calldataarg args) filtered { f -> !f.isView } { + requireInvariant _SELFisAlwaysCurrentContract; + SafeToL2Setup.f@withrevert(e,args); + assert lastReverted; +} + +// The delegateCall to setupToL2() can succeed only if Safe's nonce is zero +rule nonceMustBeZero(env e, address singletonContract) { + // get current nonce of the Safe contract + uint256 currentNonce = SafeMock.getNonce(e); + + SafeMock.delegateCallSetupToL2@withrevert(e, singletonContract); + bool callReverted = lastReverted; + + assert !callReverted => currentNonce == 0; +} + + +// The singleton contract can be updated only if the chainId is not 1 +rule theSingletonContractIsUpdatedCorrectly(env e, address newSingletonContract) { + // `newSingletonContract` is the singleton we try to assign to the Safe contract + + address singletonBefore = SafeMock.getSingleton(e); + uint256 chainId = SafeMock.getChainId(e); + + SafeMock.delegateCallSetupToL2@withrevert(e, newSingletonContract); + bool callReverted = lastReverted; + + address singletonAfter = SafeMock.getSingleton(e); + + assert !callReverted && chainId != 1 => singletonAfter == newSingletonContract; + assert !callReverted && chainId == 1 => singletonAfter == singletonBefore; +}