diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 00000000..7964b6cd --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,49 @@ +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: Install dependencies + run: yarn --frozen-lockfile + + - 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 }} 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/README.md b/README.md index 19c9ba67..8a0ceb8b 100644 --- a/README.md +++ b/README.md @@ -117,13 +117,13 @@ yarn ### Compile ```bash -npx hardhat compile +yarn hardhat compile ``` ### Test ```bash -npx hardhat test +yarn hardhat test ``` ### Deploy 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/confs/run.conf b/certora/confs/run.conf new file mode 100644 index 00000000..dd62d275 --- /dev/null +++ b/certora/confs/run.conf @@ -0,0 +1,24 @@ +{ + "files": [ + "contracts/SafeProtocolManager.sol", + "contracts/SafeProtocolRegistry.sol", + "contracts/test/TestExecutorCertora.sol", + "contracts/test/certora/TestExecutorCertoraOther.sol", + "contracts/test/TestFunctionHandlerCertora.sol", + "contracts/test/certora/TestHooksCertora.sol", + "contracts/test/TestPlugin.sol" + + ], + "hashing_length_bound": "320", + "link": [ + "SafeProtocolManager:registry=SafeProtocolRegistry" + ], + "loop_iter": "1", + "prover_args" : ["-copyLoopUnroll 11"], + "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 new file mode 100644 index 00000000..e468e31f --- /dev/null +++ b/certora/scripts/verifyManager.sh @@ -0,0 +1,3 @@ +#!/bin/bash + +certoraRun certora/confs/run.conf --solc solc8.18 diff --git a/certora/specs/Manager.spec b/certora/specs/Manager.spec new file mode 100644 index 00000000..54315885 --- /dev/null +++ b/certora/specs/Manager.spec @@ -0,0 +1,155 @@ +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; + + 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 => DISPATCHER(true); + + function _.preCheckRootAccess( + address, + SafeProtocolManager.SafeRootAccess, + uint256, + bytes + ) external => DISPATCHER(true); + + 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 { + f -> f.selector != sig:setRegistry(address).selector +} +{ + address registryBefore = registry(); + + calldataarg args; env e; + f(e, args); + + address registryAfter = registry(); + + assert registryBefore == registryAfter; + +} + +rule onlyEnabledAndListedPluginCanExecuteCall(method f) filtered { + f -> f.selector == sig:executeTransaction(address,SafeProtocolManager.SafeTransaction).selector || f.selector == sig:executeRootAccess(address,SafeProtocolManager.SafeRootAccess).selector +} { + + env e; calldataarg args; + + requireInvariant tempHooksStorage(e.msg.sender); + + require(testExecutorCertora.called() == false); + require(testFunctionHandlerCertora.called() == false); + require(testHooksCertora.called() == false); + + f(e, args); + + uint64 listedAt; + uint64 flagged; + + listedAt, flagged = contractRegistry.check(e.msg.sender); + + assert testExecutorCertora.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); + +} + +rule hooksUpdates(address safe, SafeProtocolManager.SafeTransaction transactionData){ + + // method f; + env e; calldataarg args; + storage initialStorage = lastStorage; + executeTransaction(e, safe, transactionData); + + env e2; + setHooks(e2, 0) at initialStorage; + + executeTransaction@withrevert(e, safe, transactionData); + + 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)) + 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; + 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]); +} diff --git a/contracts/SafeProtocolManager.sol b/contracts/SafeProtocolManager.sol index 37e5c1eb..fb269af3 100644 --- a/contracts/SafeProtocolManager.sol +++ b/contracts/SafeProtocolManager.sol @@ -83,6 +83,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(account, transaction, 1, abi.encode(msg.sender)); } @@ -140,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 0d903d93..4d94ea47 100644 --- a/contracts/base/FunctionHandlerManager.sol +++ b/contracts/base/FunctionHandlerManager.sol @@ -69,6 +69,8 @@ abstract contract FunctionHandlerManager is RegistryManager { revert FunctionHandlerNotSet(account, functionSelector); } + checkPermittedModule(functionHandler); + address sender; // solhint-disable-next-line no-inline-assembly assembly { diff --git a/contracts/test/TestExecutorCertora.sol b/contracts/test/TestExecutorCertora.sol new file mode 100644 index 00000000..6683a0de --- /dev/null +++ b/contracts/test/TestExecutorCertora.sol @@ -0,0 +1,112 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity ^0.8.18; +import {IAccount} from "../interfaces/Accounts.sol"; + +contract TestExecutorCertora is IAccount { + bool public called; + address public module; + address[] public owners; + address public fallbackHandler; + bytes public data; + + 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, uint256, bytes calldata, uint8) external returns (bool success) { + called = true; + success = true; + } + + function execTransactionFromModuleReturnData( + address, + uint256, + bytes memory, + uint8 + ) public returns (bool success, bytes memory returnData) { + called = true; + success = true; + returnData = data; + } + + function executeCallViaMock( + address payable to, + uint256 value, + bytes memory, + 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 {} +} diff --git a/contracts/test/TestFunctionHandlerCertora.sol b/contracts/test/TestFunctionHandlerCertora.sol new file mode 100644 index 00000000..c361372d --- /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 ""; + } +} 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..2e487064 --- /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 {IAccount} 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(address, SafeTransaction calldata, uint256, bytes calldata) external override returns (bytes memory) { + called = true; + return ""; + } + + function preCheckRootAccess(address, SafeRootAccess calldata, uint256, bytes calldata) external override returns (bytes memory) { + called = true; + return ""; + } + + function postCheck(address, bool, bytes calldata) external override { + called = true; + } +}