From 7fc684f3dc40e6b10f7773b7d1e43b38375c847a Mon Sep 17 00:00:00 2001 From: Akshay Date: Fri, 1 Sep 2023 14:24:15 +0200 Subject: [PATCH 01/14] [#95] Setup certora workflow --- .github/workflows/certora.yml | 45 ++++++++++++++++++++++++++++++++ .gitignore | 5 ++++ certora/README.md | 11 ++++++++ certora/scripts/verifyManager.sh | 17 ++++++++++++ certora/specs/Manager.spec | 19 ++++++++++++++ 5 files changed, 97 insertions(+) create mode 100644 .github/workflows/certora.yml create mode 100644 certora/README.md create mode 100644 certora/scripts/verifyManager.sh create mode 100644 certora/specs/Manager.spec diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 00000000..7a5f85e7 --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,45 @@ +name: certora + +on: + push: + branches: + - main + pull_request: + branches: + - main + + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + strategy: + matrix: + rule: ["verifyManager.sh"] + + steps: + - uses: actions/checkout@v3 + + - name: Install python + uses: actions/setup-python@v4 + with: { python-version: 3.11 } + + - name: Install java + uses: actions/setup-java@v3 + with: { java-version: "17", java-package: jre, distribution: semeru } + + - name: Install certora cli + run: pip install -Iv certora-cli + + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.18/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.18 + + - name: Verify rule ${{ matrix.rule }} + run: | + echo "key length" ${#CERTORAKEY} + ./certora/scripts/${{ matrix.rule }} + env: + CERTORAKEY: ${{ secrets.CERTORA_KEY }} \ No newline at end of file diff --git a/.gitignore b/.gitignore index 80aac338..9809f64e 100644 --- a/.gitignore +++ b/.gitignore @@ -11,3 +11,8 @@ artifacts deployments/ dist/ + +# Certora Formal Verification related files +.certora_internal +.certora_recent_jobs.json +.zip-output-url.txt diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 00000000..d5d9b0e2 --- /dev/null +++ b/certora/README.md @@ -0,0 +1,11 @@ +# Formal verification of Safe{Core} Protocol contracts + +## Setup + +- Install certora +- Setup key +- Execute + +```bash +sh certora/scripts/verifyManager.sh +``` \ No newline at end of file diff --git a/certora/scripts/verifyManager.sh b/certora/scripts/verifyManager.sh new file mode 100644 index 00000000..491231aa --- /dev/null +++ b/certora/scripts/verifyManager.sh @@ -0,0 +1,17 @@ +#!/bin/bash + +params=("--send_only") + +if [[ -n "$CI" ]]; then + params=() +fi + +certoraRun contracts/SafeProtocolManager.sol \ + --verify SafeProtocolManager:certora/specs/Manager.spec \ + --optimistic_loop \ + --loop_iter 3 \ + --optimistic_hashing \ + --hashing_length_bound 352 \ + --rule_sanity \ + "${params[@]}" \ + --msg "Safe Protocol $1" \ No newline at end of file diff --git a/certora/specs/Manager.spec b/certora/specs/Manager.spec new file mode 100644 index 00000000..417266cc --- /dev/null +++ b/certora/specs/Manager.spec @@ -0,0 +1,19 @@ +methods { + function setRegistry(address) external; + function registry() external returns (address) envfree; +} + +rule onlyOwnerCanSetRegistry (method f) filtered { + f -> f.selector != sig:setRegistry(address).selector +} +{ + address ownerBefore = registry() ; + + calldataarg args; env e; + f(e, args); + + address ownerAfter = registry(); + + assert ownerBefore == ownerAfter; + +} \ No newline at end of file From dddcbf5bf3385271c5a2b19a7907e95dacce5489 Mon Sep 17 00:00:00 2001 From: Akshay Date: Mon, 18 Sep 2023 10:33:52 +0200 Subject: [PATCH 02/14] [#95] Add execute permission to script --- .github/workflows/certora.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 7a5f85e7..f10c266e 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -40,6 +40,7 @@ jobs: - name: Verify rule ${{ matrix.rule }} run: | echo "key length" ${#CERTORAKEY} + chmod +x ./certora/scripts/${{ matrix.rule }} ./certora/scripts/${{ matrix.rule }} env: CERTORAKEY: ${{ secrets.CERTORA_KEY }} \ No newline at end of file From 40f1b8cf76551a5ea0a229696408791c5ef02501 Mon Sep 17 00:00:00 2001 From: Akshay Date: Mon, 18 Sep 2023 10:40:22 +0200 Subject: [PATCH 03/14] [#95] Add param --solc in verifyManager.sh --- certora/scripts/verifyManager.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/certora/scripts/verifyManager.sh b/certora/scripts/verifyManager.sh index 491231aa..bad01007 100644 --- a/certora/scripts/verifyManager.sh +++ b/certora/scripts/verifyManager.sh @@ -8,6 +8,7 @@ fi certoraRun contracts/SafeProtocolManager.sol \ --verify SafeProtocolManager:certora/specs/Manager.spec \ + --solc solc8.18 \ --optimistic_loop \ --loop_iter 3 \ --optimistic_hashing \ From 14ae1006378ff283473c48c5b4b6ddcb8a37edec Mon Sep 17 00:00:00 2001 From: Akshay Date: Mon, 18 Sep 2023 11:12:29 +0200 Subject: [PATCH 04/14] [#95] Install dependencies by running yarn --frozen-lockfile --- .github/workflows/certora.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index f10c266e..8237e09c 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -37,6 +37,9 @@ jobs: chmod +x solc-static-linux sudo mv solc-static-linux /usr/local/bin/solc8.18 + - name: Install dependencies + run: yarn --frozen-lockfile + - name: Verify rule ${{ matrix.rule }} run: | echo "key length" ${#CERTORAKEY} From 3b8b335948f5082e62f80ec66abdf5abc61820ce Mon Sep 17 00:00:00 2001 From: Akshay Date: Mon, 18 Sep 2023 11:18:44 +0200 Subject: [PATCH 05/14] [#95] Fix README, add newline at end of file --- .github/workflows/certora.yml | 2 +- README.md | 4 ++-- certora/specs/Manager.spec | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 8237e09c..7964b6cd 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -46,4 +46,4 @@ jobs: chmod +x ./certora/scripts/${{ matrix.rule }} ./certora/scripts/${{ matrix.rule }} env: - CERTORAKEY: ${{ secrets.CERTORA_KEY }} \ No newline at end of file + CERTORAKEY: ${{ secrets.CERTORA_KEY }} diff --git a/README.md b/README.md index cb74cece..2f41aaa4 100644 --- a/README.md +++ b/README.md @@ -114,13 +114,13 @@ yarn ### Compile ```bash -npx hardhat compile +yarn hardhat compile ``` ### Test ```bash -npx hardhat test +yarn hardhat test ``` ### Deploy diff --git a/certora/specs/Manager.spec b/certora/specs/Manager.spec index 417266cc..57e8599e 100644 --- a/certora/specs/Manager.spec +++ b/certora/specs/Manager.spec @@ -16,4 +16,4 @@ rule onlyOwnerCanSetRegistry (method f) filtered { assert ownerBefore == ownerAfter; -} \ No newline at end of file +} From f919192b3af0d9613d727f1bb172155249d8e2af Mon Sep 17 00:00:00 2001 From: Akshay Date: Mon, 18 Sep 2023 17:38:10 +0200 Subject: [PATCH 06/14] [#95] Add formal verification rules --- certora/scripts/verifyManager.sh | 4 +- certora/specs/Manager.spec | 61 ++++++++++++- contracts/test/TestExecutorCertora.sol | 113 +++++++++++++++++++++++++ 3 files changed, 173 insertions(+), 5 deletions(-) create mode 100644 contracts/test/TestExecutorCertora.sol diff --git a/certora/scripts/verifyManager.sh b/certora/scripts/verifyManager.sh index bad01007..937ab2e4 100644 --- a/certora/scripts/verifyManager.sh +++ b/certora/scripts/verifyManager.sh @@ -6,9 +6,9 @@ if [[ -n "$CI" ]]; then params=() fi -certoraRun contracts/SafeProtocolManager.sol \ +certoraRun contracts/SafeProtocolManager.sol contracts/SafeProtocolRegistry.sol contracts/test/TestExecutorCertora.sol \ --verify SafeProtocolManager:certora/specs/Manager.spec \ - --solc solc8.18 \ + --link "SafeProtocolManager:registry=SafeProtocolRegistry" \ --optimistic_loop \ --loop_iter 3 \ --optimistic_hashing \ diff --git a/certora/specs/Manager.spec b/certora/specs/Manager.spec index 57e8599e..e899e088 100644 --- a/certora/specs/Manager.spec +++ b/certora/specs/Manager.spec @@ -1,19 +1,74 @@ +using SafeProtocolRegistry as contractRegistry; +using TestExecutorCertora as testExecutorCertora; + methods { function setRegistry(address) external; function registry() external returns (address) envfree; + function testExecutorCertora.called() external returns (bool) envfree; + function contractRegistry.check(address module) external returns (uint64, uint64) envfree; + function _.execTransactionFromModule( + address, + uint256, + bytes, + uint8 + ) external => DISPATCHER(true); + + function _.execTransactionFromModuleReturnData( + address, + uint256, + bytes, + uint8 + ) external => DISPATCHER(true); + + function _.preCheck( + address, + SafeProtocolManager.SafeTransaction, + uint256, + bytes + ) external => NONDET; + + function _.postCheck(address, bool, bytes) external => NONDET; + } rule onlyOwnerCanSetRegistry (method f) filtered { f -> f.selector != sig:setRegistry(address).selector } { - address ownerBefore = registry() ; + address registryBefore = registry(); calldataarg args; env e; f(e, args); - address ownerAfter = registry(); + address registryAfter = registry(); - assert ownerBefore == ownerAfter; + assert registryBefore == registryAfter; } + +rule onlyEnabledAndListedPluginCanExecuteCall(){ + method f; env e; calldataarg args; + + require(testExecutorCertora.called() == false); + + f(e, args); + + uint64 listedAt; + uint64 flagged; + + listedAt, flagged = contractRegistry.check(e.msg.sender); + + assert testExecutorCertora.called() => (listedAt > 0 && flagged == 0); +} + +rule hookUpdates(){ + method f; env e; calldataarg args; + storage initialStorage = lastStorage; + f(e, args); + + env e2; + setHooks(e2, 0) at initialStorage; + f@withrevert(e, args); + + assert !lastReverted; +} \ No newline at end of file diff --git a/contracts/test/TestExecutorCertora.sol b/contracts/test/TestExecutorCertora.sol new file mode 100644 index 00000000..c0a45f1c --- /dev/null +++ b/contracts/test/TestExecutorCertora.sol @@ -0,0 +1,113 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity ^0.8.18; +import {ISafe} from "../interfaces/Accounts.sol"; + +contract TestExecutorCertora is ISafe { + bool public called; + address public module; + address[] public owners; + address public fallbackHandler; + + constructor(address _fallbackHandler) { + fallbackHandler = _fallbackHandler; + } + + function setModule(address _module) external { + module = _module; + } + + function setFallbackHandler(address _fallbackHandler) external { + fallbackHandler = _fallbackHandler; + } + + function exec(address payable to, uint256 value, bytes calldata data) external { + bool success; + bytes memory response; + (success, response) = to.call{value: value}(data); + if (!success) { + // solhint-disable-next-line no-inline-assembly + assembly { + revert(add(response, 0x20), mload(response)) + } + } + } + + function execTransactionFromModule( + address payable to, + uint256 value, + bytes calldata data, + uint8 operation + ) external returns (bool success) { + called = true; + } + + function execTransactionFromModuleReturnData( + address to, + uint256 value, + bytes memory data, + uint8 operation + ) public returns (bool success, bytes memory returnData) { + called = true; + } + + function executeCallViaMock( + address payable to, + uint256 value, + bytes memory data, + uint256 gas + ) external returns (bool success, bytes memory response) { + (success, response) = to.call{value: value, gas: gas}(data); + if (!success) { + // solhint-disable-next-line no-inline-assembly + assembly { + revert(add(response, 32), mload(response)) + } + } + } + + // @notice Forwards all calls to the fallback handler if set. Returns 0 if no handler is set. + // @dev Appends the non-padded caller address to the calldata to be optionally used in the handler + // The handler can make us of `HandlerContext.sol` to extract the address. + // This is done because in the next call frame the `msg.sender` will be FallbackManager's address + // and having the original caller address may enable additional verification scenarios. + // Source: https://github.com/safe-global/safe-contracts/blob/main/contracts/base/FallbackManager.sol#L62 + // solhint-disable-next-line payable-fallback,no-complex-fallback + fallback() external { + address handler = fallbackHandler; + // solhint-disable-next-line no-inline-assembly + assembly { + // When compiled with the optimizer, the compiler relies on a certain assumptions on how the + // memory is used, therefore we need to guarantee memory safety (keeping the free memory point 0x40 slot intact, + // not going beyond the scratch space, etc) + // Solidity docs: https://docs.soliditylang.org/en/latest/assembly.html#memory-safety + function allocate(length) -> pos { + pos := mload(0x40) + mstore(0x40, add(pos, length)) + } + + if iszero(handler) { + return(0, 0) + } + + let calldataPtr := allocate(calldatasize()) + calldatacopy(calldataPtr, 0, calldatasize()) + + // The msg.sender address is shifted to the left by 12 bytes to remove the padding + // Then the address without padding is stored right after the calldata + let senderPtr := allocate(20) + mstore(senderPtr, shl(96, caller())) + + // Add 20 bytes for the address appended add the end + let success := call(gas(), handler, 0, calldataPtr, add(calldatasize(), 20), 0, 0) + + let returnDataPtr := allocate(returndatasize()) + returndatacopy(returnDataPtr, 0, returndatasize()) + if iszero(success) { + revert(returnDataPtr, returndatasize()) + } + return(returnDataPtr, returndatasize()) + } + } + + receive() external payable {} +} From e3644ca105e40edfb8fd9023b0f0665a512294a1 Mon Sep 17 00:00:00 2001 From: Akshay Date: Tue, 19 Sep 2023 10:45:54 +0200 Subject: [PATCH 07/14] [#95] Update rule for hooks --- certora/scripts/verifyManager.sh | 3 ++- certora/specs/Manager.spec | 11 ++++++++--- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/certora/scripts/verifyManager.sh b/certora/scripts/verifyManager.sh index 937ab2e4..11599c15 100644 --- a/certora/scripts/verifyManager.sh +++ b/certora/scripts/verifyManager.sh @@ -9,8 +9,9 @@ fi certoraRun contracts/SafeProtocolManager.sol contracts/SafeProtocolRegistry.sol contracts/test/TestExecutorCertora.sol \ --verify SafeProtocolManager:certora/specs/Manager.spec \ --link "SafeProtocolManager:registry=SafeProtocolRegistry" \ + --solc solc8.18 \ --optimistic_loop \ - --loop_iter 3 \ + --loop_iter 1 \ --optimistic_hashing \ --hashing_length_bound 352 \ --rule_sanity \ diff --git a/certora/specs/Manager.spec b/certora/specs/Manager.spec index e899e088..60135bbd 100644 --- a/certora/specs/Manager.spec +++ b/certora/specs/Manager.spec @@ -4,6 +4,9 @@ using TestExecutorCertora as testExecutorCertora; methods { function setRegistry(address) external; function registry() external returns (address) envfree; + + function _.supportsInterface(bytes4) external => DISPATCHER(true); + function testExecutorCertora.called() external returns (bool) envfree; function contractRegistry.check(address module) external returns (uint64, uint64) envfree; function _.execTransactionFromModule( @@ -61,14 +64,16 @@ rule onlyEnabledAndListedPluginCanExecuteCall(){ assert testExecutorCertora.called() => (listedAt > 0 && flagged == 0); } -rule hookUpdates(){ +rule hooksUpdates(address safe, SafeProtocolManager.SafeTransaction transactionData){ + method f; env e; calldataarg args; storage initialStorage = lastStorage; - f(e, args); + executeTransaction(e, safe, transactionData); env e2; setHooks(e2, 0) at initialStorage; - f@withrevert(e, args); + + executeTransaction@withrevert(e, safe, transactionData); assert !lastReverted; } \ No newline at end of file From 8ef23d06ee9d24ee22b31e6f9e0a68888ae8e38e Mon Sep 17 00:00:00 2001 From: Akshay Date: Tue, 19 Sep 2023 12:22:30 +0200 Subject: [PATCH 08/14] [#95] Check if function handler is listed and not flagged --- certora/confs/run.conf | 19 +++++++++++++++ certora/scripts/verifyManager.sh | 18 +-------------- certora/specs/Manager.spec | 23 +++++++++++++++---- contracts/SafeProtocolManager.sol | 2 ++ contracts/base/FunctionHandlerManager.sol | 2 +- contracts/test/TestFunctionHandlerCertora.sol | 16 +++++++++++++ 6 files changed, 58 insertions(+), 22 deletions(-) create mode 100644 certora/confs/run.conf create mode 100644 contracts/test/TestFunctionHandlerCertora.sol diff --git a/certora/confs/run.conf b/certora/confs/run.conf new file mode 100644 index 00000000..9d9e899a --- /dev/null +++ b/certora/confs/run.conf @@ -0,0 +1,19 @@ +{ + "files": [ + "contracts/SafeProtocolManager.sol", + "contracts/SafeProtocolRegistry.sol", + "contracts/test/TestExecutorCertora.sol", + "contracts/test/TestFunctionHandlerCertora.sol" + ], + // "hashing_length_bound": "100", + "link": [ + "SafeProtocolManager:registry=SafeProtocolRegistry" + ], + "loop_iter": "1", + "msg": "Safe Protocol Manager", +// "optimistic_hashing": true, + "optimistic_loop": true, + "rule_sanity": "basic", +// "send_only": true, + "verify": "SafeProtocolManager:certora/specs/Manager.spec" +} \ No newline at end of file diff --git a/certora/scripts/verifyManager.sh b/certora/scripts/verifyManager.sh index 11599c15..57bf3006 100644 --- a/certora/scripts/verifyManager.sh +++ b/certora/scripts/verifyManager.sh @@ -1,19 +1,3 @@ #!/bin/bash -params=("--send_only") - -if [[ -n "$CI" ]]; then - params=() -fi - -certoraRun contracts/SafeProtocolManager.sol contracts/SafeProtocolRegistry.sol contracts/test/TestExecutorCertora.sol \ - --verify SafeProtocolManager:certora/specs/Manager.spec \ - --link "SafeProtocolManager:registry=SafeProtocolRegistry" \ - --solc solc8.18 \ - --optimistic_loop \ - --loop_iter 1 \ - --optimistic_hashing \ - --hashing_length_bound 352 \ - --rule_sanity \ - "${params[@]}" \ - --msg "Safe Protocol $1" \ No newline at end of file +certoraRun certora/confs/run.conf \ No newline at end of file diff --git a/certora/specs/Manager.spec b/certora/specs/Manager.spec index 60135bbd..3a18ec65 100644 --- a/certora/specs/Manager.spec +++ b/certora/specs/Manager.spec @@ -1,13 +1,14 @@ using SafeProtocolRegistry as contractRegistry; using TestExecutorCertora as testExecutorCertora; +using TestFunctionHandlerCertora as testFunctionHandlerCertora; methods { function setRegistry(address) external; function registry() external returns (address) envfree; function _.supportsInterface(bytes4) external => DISPATCHER(true); - function testExecutorCertora.called() external returns (bool) envfree; + function contractRegistry.check(address module) external returns (uint64, uint64) envfree; function _.execTransactionFromModule( address, @@ -28,10 +29,20 @@ methods { SafeProtocolManager.SafeTransaction, uint256, bytes - ) external => NONDET; + ) external => CONSTANT; - function _.postCheck(address, bool, bytes) external => NONDET; + function _.preCheckRootAccess( + address, + SafeProtocolManager.SafeTransaction, + uint256, + bytes + ) external => CONSTANT; + function _.postCheck(address, bool, bytes) external => CONSTANT; + + function _.handle(address, address, uint256, bytes) external => DISPATCHER(true); + + function testFunctionHandlerCertora.called() external returns (bool) envfree; } rule onlyOwnerCanSetRegistry (method f) filtered { @@ -62,11 +73,14 @@ rule onlyEnabledAndListedPluginCanExecuteCall(){ listedAt, flagged = contractRegistry.check(e.msg.sender); assert testExecutorCertora.called() => (listedAt > 0 && flagged == 0); + assert testFunctionHandlerCertora.called() => (listedAt > 0 && flagged == 0); + } rule hooksUpdates(address safe, SafeProtocolManager.SafeTransaction transactionData){ - method f; env e; calldataarg args; + // method f; + env e; calldataarg args; storage initialStorage = lastStorage; executeTransaction(e, safe, transactionData); @@ -76,4 +90,5 @@ rule hooksUpdates(address safe, SafeProtocolManager.SafeTransaction transactionD executeTransaction@withrevert(e, safe, transactionData); assert !lastReverted; + } \ No newline at end of file diff --git a/contracts/SafeProtocolManager.sol b/contracts/SafeProtocolManager.sol index e88575ad..0fff6db6 100644 --- a/contracts/SafeProtocolManager.sol +++ b/contracts/SafeProtocolManager.sol @@ -84,6 +84,8 @@ contract SafeProtocolManager is ISafeProtocolManager, RegistryManager, HooksMana if (areHooksEnabled) { // execution metadata for transaction execution through plugin is encoded address of the plugin i.e. msg.sender. // executionType = 1 for plugin flow + // should check below exist here? + // checkPermittedModule(hooksAddress); preCheckData = ISafeProtocolHooks(hooksAddress).preCheck(safe, transaction, 1, abi.encode(msg.sender)); } diff --git a/contracts/base/FunctionHandlerManager.sol b/contracts/base/FunctionHandlerManager.sol index e919a0b6..d8850841 100644 --- a/contracts/base/FunctionHandlerManager.sol +++ b/contracts/base/FunctionHandlerManager.sol @@ -63,7 +63,7 @@ abstract contract FunctionHandlerManager is RegistryManager { bytes4 functionSelector = bytes4(msg.data); address functionHandler = functionHandlers[safe][functionSelector]; - + checkPermittedModule(functionHandler); // Revert if functionHandler is not set if (functionHandler == address(0)) { revert FunctionHandlerNotSet(safe, functionSelector); diff --git a/contracts/test/TestFunctionHandlerCertora.sol b/contracts/test/TestFunctionHandlerCertora.sol new file mode 100644 index 00000000..b1f7482e --- /dev/null +++ b/contracts/test/TestFunctionHandlerCertora.sol @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity ^0.8.18; +import {ISafeProtocolFunctionHandler} from "../interfaces/Modules.sol"; + +contract TestFunctionHandlerCertora is ISafeProtocolFunctionHandler { + bool public called; + + function metadataProvider() external view returns (uint256 providerType, bytes memory location) {} + + function supportsInterface(bytes4 interfaceId) external view override returns (bool) {} + + function handle(address, address, uint256, bytes calldata) external override returns (bytes memory) { + called = true; + return ""; + } +} \ No newline at end of file From 7c9f352273756a1b89a645ba50b3ef38674e85c0 Mon Sep 17 00:00:00 2001 From: Akshay Date: Tue, 19 Sep 2023 17:15:26 +0200 Subject: [PATCH 09/14] [#95] Add rules for formal verification --- certora/confs/run.conf | 11 ++- certora/specs/Manager.spec | 68 +++++++++++++++++-- contracts/SafeProtocolManager.sol | 2 +- contracts/test/TestExecutorCertora.sol | 4 ++ contracts/test/TestFunctionHandlerCertora.sol | 2 +- .../test/certora/TestExecutorCertoraOther.sol | 7 ++ contracts/test/certora/TestHooksCertora.sol | 25 +++++++ 7 files changed, 107 insertions(+), 12 deletions(-) create mode 100644 contracts/test/certora/TestExecutorCertoraOther.sol create mode 100644 contracts/test/certora/TestHooksCertora.sol diff --git a/certora/confs/run.conf b/certora/confs/run.conf index 9d9e899a..7bf69ffc 100644 --- a/certora/confs/run.conf +++ b/certora/confs/run.conf @@ -3,15 +3,20 @@ "contracts/SafeProtocolManager.sol", "contracts/SafeProtocolRegistry.sol", "contracts/test/TestExecutorCertora.sol", - "contracts/test/TestFunctionHandlerCertora.sol" + "contracts/test/certora/TestExecutorCertoraOther.sol", + "contracts/test/TestFunctionHandlerCertora.sol", + "contracts/test/certora/TestHooksCertora.sol", + "contracts/test/TestPlugin.sol" + ], - // "hashing_length_bound": "100", + "hashing_length_bound": "100", "link": [ "SafeProtocolManager:registry=SafeProtocolRegistry" ], "loop_iter": "1", + "prover_args" : ["-copyLoopUnroll 11"], "msg": "Safe Protocol Manager", -// "optimistic_hashing": true, + "optimistic_hashing": true, "optimistic_loop": true, "rule_sanity": "basic", // "send_only": true, diff --git a/certora/specs/Manager.spec b/certora/specs/Manager.spec index 3a18ec65..1abd72ad 100644 --- a/certora/specs/Manager.spec +++ b/certora/specs/Manager.spec @@ -1,10 +1,14 @@ using SafeProtocolRegistry as contractRegistry; using TestExecutorCertora as testExecutorCertora; using TestFunctionHandlerCertora as testFunctionHandlerCertora; +using TestHooksCertora as testHooksCertora; +using TestExecutorCertoraOther as testExecutorCertoraOther; +using TestPlugin as testPlugin; methods { function setRegistry(address) external; function registry() external returns (address) envfree; + function tempHooksData(address) external returns (address, bytes) envfree; function _.supportsInterface(bytes4) external => DISPATCHER(true); function testExecutorCertora.called() external returns (bool) envfree; @@ -29,20 +33,24 @@ methods { SafeProtocolManager.SafeTransaction, uint256, bytes - ) external => CONSTANT; + ) external => DISPATCHER(true); function _.preCheckRootAccess( address, - SafeProtocolManager.SafeTransaction, + SafeProtocolManager.SafeRootAccess, uint256, - bytes - ) external => CONSTANT; + bytes + ) external => DISPATCHER(true); - function _.postCheck(address, bool, bytes) external => CONSTANT; + function _.postCheck(address, bool, bytes) external => DISPATCHER(true); function _.handle(address, address, uint256, bytes) external => DISPATCHER(true); function testFunctionHandlerCertora.called() external returns (bool) envfree; + + function testHooksCertora.called() external returns (bool) envfree; + + function _.requiresPermissions() external => DISPATCHER(true); } rule onlyOwnerCanSetRegistry (method f) filtered { @@ -60,10 +68,16 @@ rule onlyOwnerCanSetRegistry (method f) filtered { } -rule onlyEnabledAndListedPluginCanExecuteCall(){ +rule onlyEnabledAndListedPluginCanExecuteCall() { + + method f; env e; calldataarg args; + requireInvariant tempHooksStorage(e.msg.sender); + require(testExecutorCertora.called() == false); + require(testFunctionHandlerCertora.called() == false); + require(testHooksCertora.called() == false); f(e, args); @@ -73,7 +87,21 @@ rule onlyEnabledAndListedPluginCanExecuteCall(){ listedAt, flagged = contractRegistry.check(e.msg.sender); assert testExecutorCertora.called() => (listedAt > 0 && flagged == 0); - assert testFunctionHandlerCertora.called() => (listedAt > 0 && flagged == 0); + + uint64 listedAtHandler; + uint64 flaggedHandler; + + listedAtHandler, flaggedHandler = contractRegistry.check(testFunctionHandlerCertora); + + assert testFunctionHandlerCertora.called() => (listedAtHandler > 0 && flaggedHandler == 0); + + + uint64 listedAtHooks; + uint64 flaggedHooks; + + listedAtHooks, flaggedHooks = contractRegistry.check(testHooksCertora); + + assert testHooksCertora.called() => (listedAtHooks > 0 && flaggedHooks == 0); } @@ -91,4 +119,30 @@ rule hooksUpdates(address safe, SafeProtocolManager.SafeTransaction transactionD assert !lastReverted; +} + +function checkListedAndNotFlagged(address module) returns bool { + uint64 listedAtHooks; + uint64 flaggedHooks; + listedAtHooks, flaggedHooks = contractRegistry.check(module); + return (listedAtHooks > 0 && flaggedHooks == 0); +} + +function getTempHooksData(address account) returns address { + address hooksAddress; + bytes hooksData; + hooksAddress, hooksData = tempHooksData(account); + return hooksAddress; +} + +invariant tempHooksStorage(address plugin) + getTempHooksData(plugin) != 0 => checkListedAndNotFlagged(getTempHooksData(plugin)); + +rule onlyOneStorageUpdates{ + storage before = lastStorage; + method f; env e; calldataarg args; + f(e, args); + storage after = lastStorage; + // Either storage of testExecutorCertora is updated or storage of testExecutorCertoraOther is updated + assert (before[testExecutorCertora] == after[testExecutorCertora]) || (before[testExecutorCertoraOther] == after[testExecutorCertoraOther]); } \ No newline at end of file diff --git a/contracts/SafeProtocolManager.sol b/contracts/SafeProtocolManager.sol index 0fff6db6..d4948f2d 100644 --- a/contracts/SafeProtocolManager.sol +++ b/contracts/SafeProtocolManager.sol @@ -85,7 +85,7 @@ contract SafeProtocolManager is ISafeProtocolManager, RegistryManager, HooksMana // execution metadata for transaction execution through plugin is encoded address of the plugin i.e. msg.sender. // executionType = 1 for plugin flow // should check below exist here? - // checkPermittedModule(hooksAddress); + checkPermittedModule(hooksAddress); preCheckData = ISafeProtocolHooks(hooksAddress).preCheck(safe, transaction, 1, abi.encode(msg.sender)); } diff --git a/contracts/test/TestExecutorCertora.sol b/contracts/test/TestExecutorCertora.sol index c0a45f1c..e602c315 100644 --- a/contracts/test/TestExecutorCertora.sol +++ b/contracts/test/TestExecutorCertora.sol @@ -7,6 +7,7 @@ contract TestExecutorCertora is ISafe { address public module; address[] public owners; address public fallbackHandler; + bytes public data; constructor(address _fallbackHandler) { fallbackHandler = _fallbackHandler; @@ -39,6 +40,7 @@ contract TestExecutorCertora is ISafe { uint8 operation ) external returns (bool success) { called = true; + success = true; } function execTransactionFromModuleReturnData( @@ -48,6 +50,8 @@ contract TestExecutorCertora is ISafe { uint8 operation ) public returns (bool success, bytes memory returnData) { called = true; + success = true; + returnData = data; } function executeCallViaMock( diff --git a/contracts/test/TestFunctionHandlerCertora.sol b/contracts/test/TestFunctionHandlerCertora.sol index b1f7482e..c361372d 100644 --- a/contracts/test/TestFunctionHandlerCertora.sol +++ b/contracts/test/TestFunctionHandlerCertora.sol @@ -13,4 +13,4 @@ contract TestFunctionHandlerCertora is ISafeProtocolFunctionHandler { called = true; return ""; } -} \ No newline at end of file +} diff --git a/contracts/test/certora/TestExecutorCertoraOther.sol b/contracts/test/certora/TestExecutorCertoraOther.sol new file mode 100644 index 00000000..33f6b58a --- /dev/null +++ b/contracts/test/certora/TestExecutorCertoraOther.sol @@ -0,0 +1,7 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity ^0.8.18; +import {TestExecutorCertora} from "../TestExecutorCertora.sol"; + +contract TestExecutorCertoraOther is TestExecutorCertora { + constructor(address _fallbackHandler) TestExecutorCertora(_fallbackHandler) {} +} diff --git a/contracts/test/certora/TestHooksCertora.sol b/contracts/test/certora/TestHooksCertora.sol new file mode 100644 index 00000000..3fba03cc --- /dev/null +++ b/contracts/test/certora/TestHooksCertora.sol @@ -0,0 +1,25 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity ^0.8.18; +import {ISafeProtocolHooks} from "../../interfaces/Modules.sol"; +import {ISafe} from "../../interfaces/Accounts.sol"; +import {SafeProtocolAction, SafeTransaction, SafeRootAccess} from "../../DataTypes.sol"; + +contract TestHooksCertora is ISafeProtocolHooks { + bool public called; + + function supportsInterface(bytes4 interfaceId) external view override returns (bool) {} + + function preCheck(ISafe, SafeTransaction calldata, uint256, bytes calldata) external override returns (bytes memory) { + called = true; + return ""; + } + + function preCheckRootAccess(ISafe, SafeRootAccess calldata, uint256, bytes calldata) external override returns (bytes memory) { + called = true; + return ""; + } + + function postCheck(ISafe, bool, bytes calldata) external override { + called = true; + } +} From 19cba7aad31921b2ba8c9465f7929b87a236bba6 Mon Sep 17 00:00:00 2001 From: Akshay Date: Tue, 19 Sep 2023 17:21:13 +0200 Subject: [PATCH 10/14] [#95] Update hashing_length_bound to 320 --- certora/confs/run.conf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/confs/run.conf b/certora/confs/run.conf index 7bf69ffc..dd62d275 100644 --- a/certora/confs/run.conf +++ b/certora/confs/run.conf @@ -9,7 +9,7 @@ "contracts/test/TestPlugin.sol" ], - "hashing_length_bound": "100", + "hashing_length_bound": "320", "link": [ "SafeProtocolManager:registry=SafeProtocolRegistry" ], From 1b64211fcfe8d806b8e5d1532a1253e3796e98b3 Mon Sep 17 00:00:00 2001 From: Akshay Date: Fri, 22 Sep 2023 16:16:13 +0200 Subject: [PATCH 11/14] [#95] Append solc param in verifyManager.sh --- certora/scripts/verifyManager.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/scripts/verifyManager.sh b/certora/scripts/verifyManager.sh index 57bf3006..9f5f690a 100644 --- a/certora/scripts/verifyManager.sh +++ b/certora/scripts/verifyManager.sh @@ -1,3 +1,3 @@ #!/bin/bash -certoraRun certora/confs/run.conf \ No newline at end of file +certoraRun certora/confs/run.conf --solc solc8.2 From 6ef3c496aa032e06838f9b8fad541ba9410b7d21 Mon Sep 17 00:00:00 2001 From: Akshay Date: Fri, 22 Sep 2023 16:29:52 +0200 Subject: [PATCH 12/14] [#95] Fix failing build --- contracts/test/TestExecutorCertora.sol | 21 ++++++++------------- contracts/test/certora/TestHooksCertora.sol | 8 ++++---- 2 files changed, 12 insertions(+), 17 deletions(-) diff --git a/contracts/test/TestExecutorCertora.sol b/contracts/test/TestExecutorCertora.sol index e602c315..6683a0de 100644 --- a/contracts/test/TestExecutorCertora.sol +++ b/contracts/test/TestExecutorCertora.sol @@ -1,8 +1,8 @@ // SPDX-License-Identifier: LGPL-3.0-only pragma solidity ^0.8.18; -import {ISafe} from "../interfaces/Accounts.sol"; +import {IAccount} from "../interfaces/Accounts.sol"; -contract TestExecutorCertora is ISafe { +contract TestExecutorCertora is IAccount { bool public called; address public module; address[] public owners; @@ -33,21 +33,16 @@ contract TestExecutorCertora is ISafe { } } - function execTransactionFromModule( - address payable to, - uint256 value, - bytes calldata data, - uint8 operation - ) external returns (bool success) { + function execTransactionFromModule(address payable, uint256, bytes calldata, uint8) external returns (bool success) { called = true; success = true; } function execTransactionFromModuleReturnData( - address to, - uint256 value, - bytes memory data, - uint8 operation + address, + uint256, + bytes memory, + uint8 ) public returns (bool success, bytes memory returnData) { called = true; success = true; @@ -57,7 +52,7 @@ contract TestExecutorCertora is ISafe { function executeCallViaMock( address payable to, uint256 value, - bytes memory data, + bytes memory, uint256 gas ) external returns (bool success, bytes memory response) { (success, response) = to.call{value: value, gas: gas}(data); diff --git a/contracts/test/certora/TestHooksCertora.sol b/contracts/test/certora/TestHooksCertora.sol index 3fba03cc..2e487064 100644 --- a/contracts/test/certora/TestHooksCertora.sol +++ b/contracts/test/certora/TestHooksCertora.sol @@ -1,7 +1,7 @@ // SPDX-License-Identifier: LGPL-3.0-only pragma solidity ^0.8.18; import {ISafeProtocolHooks} from "../../interfaces/Modules.sol"; -import {ISafe} from "../../interfaces/Accounts.sol"; +import {IAccount} from "../../interfaces/Accounts.sol"; import {SafeProtocolAction, SafeTransaction, SafeRootAccess} from "../../DataTypes.sol"; contract TestHooksCertora is ISafeProtocolHooks { @@ -9,17 +9,17 @@ contract TestHooksCertora is ISafeProtocolHooks { function supportsInterface(bytes4 interfaceId) external view override returns (bool) {} - function preCheck(ISafe, SafeTransaction calldata, uint256, bytes calldata) external override returns (bytes memory) { + function preCheck(address, SafeTransaction calldata, uint256, bytes calldata) external override returns (bytes memory) { called = true; return ""; } - function preCheckRootAccess(ISafe, SafeRootAccess calldata, uint256, bytes calldata) external override returns (bytes memory) { + function preCheckRootAccess(address, SafeRootAccess calldata, uint256, bytes calldata) external override returns (bytes memory) { called = true; return ""; } - function postCheck(ISafe, bool, bytes calldata) external override { + function postCheck(address, bool, bytes calldata) external override { called = true; } } From ef786a7b6a8ed20677281347429e3afef0a2103b Mon Sep 17 00:00:00 2001 From: Akshay Date: Fri, 22 Sep 2023 16:56:29 +0200 Subject: [PATCH 13/14] [#95] Fix solc param in verifyManager.sh --- certora/scripts/verifyManager.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/scripts/verifyManager.sh b/certora/scripts/verifyManager.sh index 9f5f690a..e468e31f 100644 --- a/certora/scripts/verifyManager.sh +++ b/certora/scripts/verifyManager.sh @@ -1,3 +1,3 @@ #!/bin/bash -certoraRun certora/confs/run.conf --solc solc8.2 +certoraRun certora/confs/run.conf --solc solc8.18 From 4b3db3c090cae7b59a4cfa3befc027d4744b1204 Mon Sep 17 00:00:00 2001 From: Akshay Date: Mon, 25 Sep 2023 14:04:04 +0200 Subject: [PATCH 14/14] [#95] Add rules --- certora/specs/Manager.spec | 17 ++++++++++++----- contracts/SafeProtocolManager.sol | 2 ++ contracts/base/FunctionHandlerManager.sol | 3 ++- 3 files changed, 16 insertions(+), 6 deletions(-) diff --git a/certora/specs/Manager.spec b/certora/specs/Manager.spec index 1abd72ad..54315885 100644 --- a/certora/specs/Manager.spec +++ b/certora/specs/Manager.spec @@ -68,10 +68,11 @@ rule onlyOwnerCanSetRegistry (method f) filtered { } -rule onlyEnabledAndListedPluginCanExecuteCall() { +rule onlyEnabledAndListedPluginCanExecuteCall(method f) filtered { + f -> f.selector == sig:executeTransaction(address,SafeProtocolManager.SafeTransaction).selector || f.selector == sig:executeRootAccess(address,SafeProtocolManager.SafeRootAccess).selector +} { - - method f; env e; calldataarg args; + env e; calldataarg args; requireInvariant tempHooksStorage(e.msg.sender); @@ -136,7 +137,13 @@ function getTempHooksData(address account) returns address { } invariant tempHooksStorage(address plugin) - getTempHooksData(plugin) != 0 => checkListedAndNotFlagged(getTempHooksData(plugin)); + getTempHooksData(plugin) != 0 => checkListedAndNotFlagged(getTempHooksData(plugin)) + filtered { f -> f.selector != sig:checkModuleTransaction(address,uint256,bytes,Enum.Operation,address).selector} + +invariant tempHooksStorageIsAlwaysEmpty(address plugin) + getTempHooksData(plugin) == 0 + filtered { f -> f.selector != sig:checkModuleTransaction(address,uint256,bytes,Enum.Operation,address).selector} + rule onlyOneStorageUpdates{ storage before = lastStorage; @@ -145,4 +152,4 @@ rule onlyOneStorageUpdates{ storage after = lastStorage; // Either storage of testExecutorCertora is updated or storage of testExecutorCertoraOther is updated assert (before[testExecutorCertora] == after[testExecutorCertora]) || (before[testExecutorCertoraOther] == after[testExecutorCertoraOther]); -} \ No newline at end of file +} diff --git a/contracts/SafeProtocolManager.sol b/contracts/SafeProtocolManager.sol index 039cef10..fb269af3 100644 --- a/contracts/SafeProtocolManager.sol +++ b/contracts/SafeProtocolManager.sol @@ -142,6 +142,8 @@ contract SafeProtocolManager is ISafeProtocolManager, RegistryManager, HooksMana if (areHooksEnabled) { // execution metadata for transaction execution through plugin is encoded address of the plugin i.e. msg.sender. // executionType = 1 for plugin flow + // should check below exist here? + checkPermittedModule(hooksAddress); preCheckData = ISafeProtocolHooks(hooksAddress).preCheckRootAccess(account, rootAccess, 1, abi.encode(msg.sender)); } diff --git a/contracts/base/FunctionHandlerManager.sol b/contracts/base/FunctionHandlerManager.sol index de346926..4d94ea47 100644 --- a/contracts/base/FunctionHandlerManager.sol +++ b/contracts/base/FunctionHandlerManager.sol @@ -63,13 +63,14 @@ abstract contract FunctionHandlerManager is RegistryManager { bytes4 functionSelector = bytes4(msg.data); address functionHandler = functionHandlers[account][functionSelector]; - checkPermittedModule(functionHandler); // Revert if functionHandler is not set if (functionHandler == address(0)) { revert FunctionHandlerNotSet(account, functionSelector); } + checkPermittedModule(functionHandler); + address sender; // solhint-disable-next-line no-inline-assembly assembly {