diff --git a/certora/conf/SafeMigration.conf b/certora/conf/SafeMigration.conf new file mode 100644 index 000000000..e9a85aeef --- /dev/null +++ b/certora/conf/SafeMigration.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "contracts/libraries/SafeMigration.sol", + "certora/mocks/SafeMock.sol", + ], + "link": [ + "SafeMock:impl=SafeMigration" + ], + "loop_iter": "3", + "msg": "SafeMigration", + "optimistic_hashing": true, + "process": "emv", + // "rule_sanity": "advanced", + "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..a4e1cab86 --- /dev/null +++ b/certora/conf/SafeToL2Migration.conf @@ -0,0 +1,17 @@ +{ + "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", + // "rule_sanity": "advanced", + "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..67319cbb4 --- /dev/null +++ b/certora/conf/SafeToL2Setup.conf @@ -0,0 +1,16 @@ +{ + "files": [ + "contracts/libraries/SafeToL2Setup.sol", + "certora/mocks/SafeMock.sol" + ], + "link": [ + "SafeMock:impl=SafeToL2Setup" + ], + "loop_iter": "3", + "msg": "SafeToL2Setup", + "optimistic_hashing": true, + "process": "emv", + // "rule_sanity": "advanced", + "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..56874da93 --- /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, bytes memory data) = impl.delegatecall( + abi.encodeWithSignature("setupToL2(address)", l2Singleton) + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateSingleton() public { + (bool success, bytes memory data) = impl.delegatecall( + abi.encodeWithSignature("migrateSingleton()") + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateWithFallbackHandler() public { + (bool success, bytes memory data) = impl.delegatecall( + abi.encodeWithSignature("migrateWithFallbackHandler()") + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateL2Singleton() public { + (bool success, bytes memory data) = impl.delegatecall( + abi.encodeWithSignature("migrateL2Singleton()") + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateL2WithFallbackHandler() public { + (bool success, bytes memory data) = impl.delegatecall( + abi.encodeWithSignature("migrateL2WithFallbackHandler()") + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateToL2(address l2Singleton) public { + (bool success, bytes memory data) = impl.delegatecall( + abi.encodeWithSignature("migrateToL2(address)", l2Singleton) + ); + + if (!success) { + revert("Something went wrong"); + } + } + + function delegateMigrateFromV111(address l2Singleton, address fallbackHandlerAddr) public { + (bool success, bytes memory data) = impl.delegatecall( + abi.encodeWithSignature("migrateFromV111(address,address)", l2Singleton, fallbackHandlerAddr) + ); + + if (!success) { + revert("Something went wrong"); + } + } + +} \ No newline at end of file diff --git a/certora/specs/SafeMigration.spec b/certora/specs/SafeMigration.spec new file mode 100644 index 000000000..fb2802c9e --- /dev/null +++ b/certora/specs/SafeMigration.spec @@ -0,0 +1,84 @@ +// All rules of SafeMigration without sanity check +// https://prover.certora.com/output/80942/620608f8f84c40e498eeb6e672b27d91?anonymousKey=3b88dbb5a130bb1b7733e9c9ea9f6b84c375864e + +// All rules of SafeMigration with sanity check +// https://prover.certora.com/output/80942/19f6446a292242d4ae7448da7eb3a5ec?anonymousKey=8dba0d1d6a0028d5faa80e7b38bbdb80e1d373f2 + +using SafeMigration as SafeMigration; +using SafeMock as SafeMock; + +methods { + function _.setFallbackHandler(address) external => DISPATCHER(true); +} + +// MIGRATION_SINGLETON is always the current contract +// passes - https://prover.certora.com/output/80942/1f393e4a9f464500b6ab07e4f1670c70?anonymousKey=cae79ff7b651cc8da032d6cfba5597eacd0918e5 +invariant MIGRATION_SINGLETONisAlwaysCurrentContract() + SafeMigration.MIGRATION_SINGLETON == SafeMigration; + + +// all the function that are not view function will revert (if it is not delegateCall) +// passes - https://prover.certora.com/output/80942/1f393e4a9f464500b6ab07e4f1670c70?anonymousKey=cae79ff7b651cc8da032d6cfba5597eacd0918e5 +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) +// passes - https://prover.certora.com/output/80942/3518444596b84ae6ae47bd08d8ebfb60?anonymousKey=bc02b2447d81d7762d0b34b2d98a31a8dc225ca6 +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) +// passes - https://prover.certora.com/output/80942/7fcd95ecf2574139a1ee490f9b6b68c9?anonymousKey=fefdae9e8e8a0aebdd99d5ebd6288b2555b6a86e +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; +} \ No newline at end of file diff --git a/certora/specs/SafeToL2Migration.spec b/certora/specs/SafeToL2Migration.spec new file mode 100644 index 000000000..7d2f6b00e --- /dev/null +++ b/certora/specs/SafeToL2Migration.spec @@ -0,0 +1,75 @@ +// All rules of SafeToL2Migration without sanity check +// https://prover.certora.com/output/80942/0e6b9696724342b38f978129c826dd46?anonymousKey=fc6f2912ae59d097b105f8458fb7870f08694114 + +// All rules of SafeToL2Migration with sanity check +// https://prover.certora.com/output/80942/a95f00eed26c4aa89c3e24fc07c1c574?anonymousKey=a63ab3672b3ae8e42a5af1e6b1f36251227d9ce8 + +using SafeToL2Migration as SafeToL2Migration; +using SafeMock as SafeMock; + +methods { + function _.setFallbackHandler(address) external => DISPATCHER(true); +} + +// MIGRATION_SINGLETON is always the current contract +// passes - https://prover.certora.com/output/80942/3087ca5a9a27481891e7f84736ec6aaf?anonymousKey=f867049529614ee37a9c573ff1e479834e34ad52 +invariant MIGRATION_SINGLETONisAlwaysCurrentContract() + SafeToL2Migration.MIGRATION_SINGLETON == SafeToL2Migration; + + +// all the function that are not view function will revert (if it is not delegateCall) +// passes - https://prover.certora.com/output/80942/3349cd8b7e9645c1ba89bf874580649c?anonymousKey=5375971a67985c430f00936755857d20e61d3f5f +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 +// passes - https://prover.certora.com/output/80942/a809db0dd61140bbbbf2b8df6318491c?anonymousKey=71b8fdfdedc8523bda752739c743b8e3202f05a2 +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() +// passes - https://prover.certora.com/output/80942/2eec3578aa6a434686e6af3c2e08768f?anonymousKey=7df843e6bab53765efa0d2c29597ac1b2474930e +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() +// running (extended check) - https://prover.certora.com/output/80942/01b4a45695cb4f83bee86a0f4e9110e0?anonymousKey=b0d04846f6eb35c3037f0983da75aef8980dad28 +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; +} \ No newline at end of file diff --git a/certora/specs/SafeToL2Setup.spec b/certora/specs/SafeToL2Setup.spec new file mode 100644 index 000000000..f9142195d --- /dev/null +++ b/certora/specs/SafeToL2Setup.spec @@ -0,0 +1,55 @@ +// All rules of SafeToL2Setup without sanity check +// https://prover.certora.com/output/80942/0639d6b99acb41ea9939baad4781bfa1?anonymousKey=c279b3bd45442b66b5ecad7a017e5b4ad3be1e4e + +// All rules of SafeToL2Setup with sanity check +// https://prover.certora.com/output/80942/3cbb0c40489045488279deda0cfa9a4a?anonymousKey=f7fd8636ff12c6d589a46ac56d312e394a382004 + +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 +// passes - https://prover.certora.com/output/80942/a2558c3b8fcf46a8bf3df94600026345?anonymousKey=c168a08554d2c1d9226269a72567e82e0dc1805a +invariant _SELFisAlwaysCurrentContract() + SafeToL2Setup._SELF == SafeToL2Setup; + + +// all the non-view functions will revert when called directly (only delegateCall is allowed) +// passes - https://prover.certora.com/output/80942/a2558c3b8fcf46a8bf3df94600026345?anonymousKey=c168a08554d2c1d9226269a72567e82e0dc1805a +rule allNonViewFunctionRevert(env e, method f, calldataarg args) filtered { f -> !f.isView } { + requireInvariant _SELFisAlwaysCurrentContract; + SafeToL2Setup.f@withrevert(e,args); + assert lastReverted; +} + +// delegateCall to setupToL2() can succeed only if Safe's nonce is zero +// passes - https://prover.certora.com/output/80942/35c91add2768483d92deb5d864e7e5e4?anonymousKey=02d1291b5b390f7ff332b44d9f8465e7d0991651 +rule nonceMustBeZero(env e) { + // get current nonce of the Safe contract + uint256 currentNonce = SafeMock.getNonce(e); + address singletonContract; + + 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 +// passes - https://prover.certora.com/output/80942/7dc165e79c724608b79edb5f4b3a8cc3?anonymousKey=d99b351a5d6b09831496ed245f31b54bb8902a16 +rule theSingletonContractIsUpdatedCorrectly(env e) { + address newSingletonContract; // 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; +} +