From 8677f3239d2707c35d41293a00c6c806d64a6240 Mon Sep 17 00:00:00 2001 From: Derek <158146599+derek-certora@users.noreply.github.com> Date: Thu, 16 Jan 2025 08:45:56 +0000 Subject: [PATCH] Formal Verification for Safe v1.5 Audit (#901) This pull request corresponds to the formal verification aspect of the Safe v1.5 audit done by Certora. ## Summary of Changes ### Added Configuration and Specification files corresponding to new rules: * `execute.conf` and `Execute.spec` * `extensible.conf` and `Extensible.spec` * `fallback.conf` and `Fallback.spec` * `guards.conf` and `Guards.spec` * `hash.conf` and `Hash.spec` * `setup.conf` and `Setup.spec` Harness: * `ExtensibleFallbackHandlerHarness.sol` to reason about the fallback handler Mocks: * `DummyHandler.sol` for reasoning about the fallback handler * `TxnGuardMock.sol` and `TxnGuardMockDuplicate.sol` for reasoning about the transaction guard * `ModuleGuardMock.sol` and `ModuleGuardMockDuplicate.sol` for reasoning about the module guard ### Modified * `applyHarness.patch` - added some minor munging as explained in the audit report * `run.conf` - remove a deprecated configuration tag that was giving errors to the Prover * `Safe.spec` - moved a rule about guards to `Guard.spec` for logical continuity * `SafeHarness.sol` - added some view functionality to the Safe harness for some rules Co-authored-by: Derek Sorensen --- certora/applyHarness.patch | 48 +++- certora/conf/execute.conf | 27 +++ certora/conf/extensible.conf | 27 +++ certora/conf/fallback.conf | 27 +++ certora/conf/guards.conf | 35 +++ certora/conf/hash.conf | 25 ++ certora/conf/run.conf | 1 - certora/conf/setup.conf | 25 ++ .../ExtensibleFallbackHandlerHarness.sol | 11 + certora/harnesses/SafeHarness.sol | 32 +++ certora/mocks/DummyHandler.sol | 24 ++ certora/mocks/ModuleGuardMock.sol | 71 ++++++ certora/mocks/ModuleGuardMockDuplicate.sol | 71 ++++++ certora/mocks/TxnGuardMock.sol | 78 +++++++ certora/mocks/TxnGuardMockDuplicate.sol | 78 +++++++ certora/specs/Execute.spec | 161 +++++++++++++ certora/specs/Extensible.spec | 74 ++++++ certora/specs/Fallback.spec | 84 +++++++ certora/specs/Guards.spec | 219 ++++++++++++++++++ certora/specs/Hash.spec | 43 ++++ certora/specs/Safe.spec | 15 -- certora/specs/Setup.spec | 43 ++++ 22 files changed, 1191 insertions(+), 28 deletions(-) create mode 100644 certora/conf/execute.conf create mode 100644 certora/conf/extensible.conf create mode 100644 certora/conf/fallback.conf create mode 100644 certora/conf/guards.conf create mode 100644 certora/conf/hash.conf create mode 100644 certora/conf/setup.conf create mode 100644 certora/harnesses/ExtensibleFallbackHandlerHarness.sol create mode 100644 certora/mocks/DummyHandler.sol create mode 100644 certora/mocks/ModuleGuardMock.sol create mode 100644 certora/mocks/ModuleGuardMockDuplicate.sol create mode 100644 certora/mocks/TxnGuardMock.sol create mode 100644 certora/mocks/TxnGuardMockDuplicate.sol create mode 100644 certora/specs/Execute.spec create mode 100644 certora/specs/Extensible.spec create mode 100644 certora/specs/Fallback.spec create mode 100644 certora/specs/Guards.spec create mode 100644 certora/specs/Hash.spec create mode 100644 certora/specs/Setup.spec diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 3f6742286..662b4dda5 100644 --- a/certora/applyHarness.patch +++ b/certora/applyHarness.patch @@ -1,6 +1,6 @@ diff -druN Safe.sol Safe.sol ---- Safe.sol 2024-10-23 15:00:06 -+++ Safe.sol 2024-10-23 15:04:05 +--- Safe.sol 2024-12-16 07:43:06 ++++ Safe.sol 2025-01-13 11:58:17 @@ -75,22 +75,24 @@ * so we create a Safe with 0 owners and threshold 1. * This is an unusable Safe, perfect for the singleton @@ -30,7 +30,7 @@ diff -druN Safe.sol Safe.sol // setupOwners checks if the Threshold is already set, therefore preventing this method from being called more than once setupOwners(_owners, _threshold); if (fallbackHandler != address(0)) internalSetFallbackHandler(fallbackHandler); -@@ -386,9 +388,6 @@ +@@ -388,9 +390,6 @@ return keccak256(abi.encode(DOMAIN_SEPARATOR_TYPEHASH, chainId, this)); } @@ -40,7 +40,7 @@ diff -druN Safe.sol Safe.sol function getTransactionHash( address to, uint256 value, -@@ -400,7 +399,9 @@ +@@ -402,7 +401,9 @@ address gasToken, address refundReceiver, uint256 _nonce @@ -50,10 +50,21 @@ diff -druN Safe.sol Safe.sol + bytes32 domainHash = domainSeparator(); - // We opted out for using assembly code here, because the way Solidity compiler we use (0.7.6) + // We opted for using assembly code here, because the way Solidity compiler we use (0.7.6) allocates memory is +@@ -452,7 +453,8 @@ + // Store the domain separator + mstore(add(ptr, 32), domainHash) + // Calculate the hash +- txHash := keccak256(add(ptr, 30), 66) ++ //txHash := keccak256(add(ptr, 30), 66) // old ++ txHash := keccak256(add(ptr, 0), 128) // new + } + /* solhint-enable no-inline-assembly */ + } + diff -druN base/Executor.sol base/Executor.sol ---- base/Executor.sol 2024-10-18 15:20:48 -+++ base/Executor.sol 2024-10-23 15:03:22 +--- base/Executor.sol 2024-12-16 07:43:06 ++++ base/Executor.sol 2025-01-13 11:58:17 @@ -26,12 +26,8 @@ uint256 txGas ) internal returns (bool success) { @@ -69,10 +80,23 @@ diff -druN base/Executor.sol base/Executor.sol } else { /* solhint-disable no-inline-assembly */ /// @solidity memory-safe-assembly +diff -druN base/FallbackManager.sol base/FallbackManager.sol +--- base/FallbackManager.sol 2024-12-16 07:43:06 ++++ base/FallbackManager.sol 2025-01-13 12:07:42 +@@ -63,7 +63,8 @@ + // not going beyond the scratch space, etc) + // Solidity docs: https://docs.soliditylang.org/en/latest/assembly.html#memory-safety + +- let handler := sload(FALLBACK_HANDLER_STORAGE_SLOT) ++ // let handler := sload(FALLBACK_HANDLER_STORAGE_SLOT) ++ let handler := and(0xffffffffffffffffffffffffffffffffffffffff, sload(FALLBACK_HANDLER_STORAGE_SLOT)) + + if iszero(handler) { + return(0, 0) diff -druN interfaces/ISafe.sol interfaces/ISafe.sol ---- interfaces/ISafe.sol 2024-10-18 15:20:48 -+++ interfaces/ISafe.sol 2024-10-23 15:03:22 -@@ -110,7 +110,7 @@ +--- interfaces/ISafe.sol 2024-12-16 07:43:06 ++++ interfaces/ISafe.sol 2025-01-13 11:58:17 +@@ -113,7 +113,7 @@ */ function domainSeparator() external view returns (bytes32); @@ -81,7 +105,7 @@ diff -druN interfaces/ISafe.sol interfaces/ISafe.sol * @notice Returns transaction hash to be signed by owners. * @param to Destination address. * @param value Ether value. -@@ -123,7 +123,6 @@ +@@ -126,7 +126,6 @@ * @param refundReceiver Address of receiver of gas payment (or 0 if tx.origin). * @param _nonce Transaction nonce. * @return Transaction hash. @@ -89,7 +113,7 @@ diff -druN interfaces/ISafe.sol interfaces/ISafe.sol function getTransactionHash( address to, uint256 value, -@@ -136,6 +135,8 @@ +@@ -139,6 +138,8 @@ address refundReceiver, uint256 _nonce ) external view returns (bytes32); diff --git a/certora/conf/execute.conf b/certora/conf/execute.conf new file mode 100644 index 000000000..69af1c53d --- /dev/null +++ b/certora/conf/execute.conf @@ -0,0 +1,27 @@ +{ + "files": [ + "certora/harnesses/SafeHarness.sol", + "certora/mocks/ModuleGuardMock.sol", // a module guard + "certora/mocks/TxnGuardMock.sol", // a (safe) guard + ], + "link": [ + + ], + "verify": "SafeHarness:certora/specs/Execute.spec", + + "assert_autofinder_success": true, + "optimistic_summary_recursion": true, + "optimistic_contract_recursion": true, + + "summary_recursion_limit": "2", + "contract_recursion_limit": "2", + "loop_iter": "3", + "optimistic_loop": true, + "optimistic_hashing": true, + "optimistic_fallback": true, + + "rule_sanity": "basic", + + "solc": "solc7.6", + "solc_via_ir": false, +} \ No newline at end of file diff --git a/certora/conf/extensible.conf b/certora/conf/extensible.conf new file mode 100644 index 000000000..beb336137 --- /dev/null +++ b/certora/conf/extensible.conf @@ -0,0 +1,27 @@ +{ + "files": [ + "certora/harnesses/SafeHarness.sol", + "certora/harnesses/ExtensibleFallbackHandlerHarness.sol", + "certora/mocks/DummyHandler.sol" + ], + "link": [ + + ], + "verify": "SafeHarness:certora/specs/Extensible.spec", + + "assert_autofinder_success": true, + "optimistic_summary_recursion": true, + "optimistic_contract_recursion": true, + + "summary_recursion_limit": "2", + "contract_recursion_limit": "2", + "loop_iter": "3", + "optimistic_loop": true, + "optimistic_hashing": true, + "optimistic_fallback": true, + + "rule_sanity": "basic", + + "solc": "solc7.6", + "solc_via_ir": false, +} \ No newline at end of file diff --git a/certora/conf/fallback.conf b/certora/conf/fallback.conf new file mode 100644 index 000000000..1c8ecf8b3 --- /dev/null +++ b/certora/conf/fallback.conf @@ -0,0 +1,27 @@ +{ + "files": [ + "certora/harnesses/SafeHarness.sol", + "certora/harnesses/ExtensibleFallbackHandlerHarness.sol", + "certora/mocks/DummyHandler.sol" + ], + "link": [ + + ], + "verify": "SafeHarness:certora/specs/Fallback.spec", + + "assert_autofinder_success": true, + "optimistic_summary_recursion": true, + "optimistic_contract_recursion": true, + + "summary_recursion_limit": "2", + "contract_recursion_limit": "2", + "loop_iter": "3", + "optimistic_loop": true, + "optimistic_hashing": true, + "optimistic_fallback": true, + + "rule_sanity": "basic", + + "solc": "solc7.6", + "solc_via_ir": false, +} \ No newline at end of file diff --git a/certora/conf/guards.conf b/certora/conf/guards.conf new file mode 100644 index 000000000..e367ba943 --- /dev/null +++ b/certora/conf/guards.conf @@ -0,0 +1,35 @@ +// a conf file for safe module guards +{ + "files": [ + "certora/harnesses/SafeHarness.sol", + "certora/mocks/ModuleGuardMock.sol", // a module guard + "certora/mocks/ModuleGuardMockDuplicate.sol", + "certora/mocks/TxnGuardMock.sol", // a (safe) guard + "certora/mocks/TxnGuardMockDuplicate.sol", + ], + "link": [ + + ], + "verify": "SafeHarness:certora/specs/Guards.spec", + + "assert_autofinder_success": true, + "optimistic_summary_recursion": true, + "optimistic_contract_recursion": true, + + "summary_recursion_limit": "2", + "contract_recursion_limit": "2", + "loop_iter": "3", + "optimistic_loop": true, + "optimistic_hashing": true, + "optimistic_fallback": true, + + "rule_sanity": "basic", + + "solc": "solc7.6", + "solc_via_ir": false, + + "prover_args": [ + " -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on", + "-enableSolidityBasedInlining true" + ], +} \ No newline at end of file diff --git a/certora/conf/hash.conf b/certora/conf/hash.conf new file mode 100644 index 000000000..527d89415 --- /dev/null +++ b/certora/conf/hash.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "certora/harnesses/SafeHarness.sol" + ], + "link": [ + + ], + "verify": "SafeHarness:certora/specs/Hash.spec", + + "assert_autofinder_success": true, + "optimistic_summary_recursion": true, + "optimistic_contract_recursion": true, + + "summary_recursion_limit": "2", + "contract_recursion_limit": "2", + "loop_iter": "3", + "optimistic_loop": true, + "optimistic_hashing": true, + "optimistic_fallback": true, + + "rule_sanity": "basic", + + "solc": "solc7.6", + "solc_via_ir": false, +} \ No newline at end of file diff --git a/certora/conf/run.conf b/certora/conf/run.conf index c3137e83d..4a27a8c15 100644 --- a/certora/conf/run.conf +++ b/certora/conf/run.conf @@ -14,7 +14,6 @@ ], "rule_sanity": "basic", "run_source": "MUTATION", - "send_only": true, "solc": "solc7.6", "verify": "SafeHarness:certora/specs/Safe.spec" } \ No newline at end of file diff --git a/certora/conf/setup.conf b/certora/conf/setup.conf new file mode 100644 index 000000000..8b0407ff0 --- /dev/null +++ b/certora/conf/setup.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "certora/harnesses/SafeHarness.sol" + ], + "link": [ + + ], + "verify": "SafeHarness:certora/specs/Setup.spec", + + "assert_autofinder_success": true, + "optimistic_summary_recursion": true, + "optimistic_contract_recursion": true, + + "summary_recursion_limit": "2", + "contract_recursion_limit": "2", + "loop_iter": "3", + "optimistic_loop": true, + "optimistic_hashing": true, + "optimistic_fallback": true, + + "rule_sanity": "basic", + + "solc": "solc7.6", + "solc_via_ir": false, +} \ No newline at end of file diff --git a/certora/harnesses/ExtensibleFallbackHandlerHarness.sol b/certora/harnesses/ExtensibleFallbackHandlerHarness.sol new file mode 100644 index 000000000..02c1730d7 --- /dev/null +++ b/certora/harnesses/ExtensibleFallbackHandlerHarness.sol @@ -0,0 +1,11 @@ +// SPDX-License-Identifier: LGPL-3.0-only +import "../munged/handler/ExtensibleFallbackHandler.sol"; +import {ISafe} from "../munged/interfaces/ISafe.sol"; + +contract ExtensibleFallbackHandlerHarness is ExtensibleFallbackHandler { + + function getSafeMethod(ISafe safe, bytes4 selector) public view returns (bytes32) { + return safeMethods[safe][selector]; + } + +} \ No newline at end of file diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol index c3380ac73..f2d100e27 100644 --- a/certora/harnesses/SafeHarness.sol +++ b/certora/harnesses/SafeHarness.sol @@ -1,5 +1,9 @@ // SPDX-License-Identifier: LGPL-3.0-only import "../munged/Safe.sol"; +import {SafeMath} from "../munged/external/SafeMath.sol"; +import {ISafe, IStaticFallbackMethod, IFallbackMethod, ExtensibleBase} from "../munged/handler/extensible/ExtensibleBase.sol"; +import {IFallbackHandler, FallbackHandler} from "../munged/handler/extensible/FallbackHandler.sol"; + contract SafeHarness is Safe { constructor( @@ -31,6 +35,10 @@ contract SafeHarness is Safe { } } + function numSigsSufficient(bytes memory signatures,uint256 requiredSignatures) public pure returns (bool) { + return (signatures.length >= SafeMath.mul(requiredSignatures,65)); + } + // harnessed getters function getModule(address module) public view returns (address) { return modules[module]; @@ -40,6 +48,10 @@ contract SafeHarness is Safe { return getGuard(); } + function getModuleGuardExternal() public view returns (address) { + return getModuleGuard(); + } + function getNativeTokenBalance() public view returns (uint256) { return address(this).balance; } @@ -56,6 +68,26 @@ contract SafeHarness is Safe { return getOwners().length; } + function approvedHashVal(address a, bytes32 hashInQuestion) public view returns (uint256) { + return approvedHashes[a][hashInQuestion]; + } + + function getFallbackHandler() public view returns (address) { + address handler; + assembly{ + handler := sload(FALLBACK_HANDLER_STORAGE_SLOT) + } + return handler ; + } + + function callSetSafeMethod(bytes4 selector, bytes32 newMethod) public { + IFallbackHandler(address(this)).setSafeMethod(selector,newMethod); + } + + function callDummyHandler(bytes4 selector) public { + address(this).call(abi.encodeWithSelector(selector)); + } + function getTransactionHashPublic( address to, uint256 value, diff --git a/certora/mocks/DummyHandler.sol b/certora/mocks/DummyHandler.sol new file mode 100644 index 000000000..6a121cb94 --- /dev/null +++ b/certora/mocks/DummyHandler.sol @@ -0,0 +1,24 @@ +// a dummy handler contract +import {ISafe, IStaticFallbackMethod, IFallbackMethod, ExtensibleBase} from "../munged/handler/extensible/ExtensibleBase.sol"; + +contract DummyHandler is IFallbackMethod { + constructor(){ + methodCalled = false ; + } + + bool public methodCalled ; + function resetMethodCalled() public { + methodCalled = false; + } + + // the DUMMY method + function handle(ISafe safe, address sender, uint256 value, bytes calldata data) external override returns (bytes memory result) { + methodCalled = true ; + + return "Hello, world!"; + } + + function dummyMethod() public { + methodCalled = true ; + } +} \ No newline at end of file diff --git a/certora/mocks/ModuleGuardMock.sol b/certora/mocks/ModuleGuardMock.sol new file mode 100644 index 000000000..299d29c9a --- /dev/null +++ b/certora/mocks/ModuleGuardMock.sol @@ -0,0 +1,71 @@ +// SPDX-License-Identifier: LGPL-3.0-only +/* solhint-disable one-contract-per-file */ +pragma solidity >=0.7.0 <0.9.0; +import {IModuleGuard} from "../munged/base/ModuleManager.sol"; +import {IERC165} from "../munged/interfaces/IERC165.sol"; +import "../munged/libraries/Enum.sol"; + +contract ModuleGuardMock is IModuleGuard { + + constructor(){ + preCheckedTransactions = false ; + postCheckedTransactions = false ; + } + + // some mock variables + bool public preCheckedTransactions ; + bool public postCheckedTransactions ; + + function resetChecks() external { + preCheckedTransactions = false ; + postCheckedTransactions = false ; + } + + /** + * @notice Checks the module transaction details. + * @dev The function needs to implement module transaction validation logic. + * @param to The address to which the transaction is intended. + * @param value The value of the transaction in Wei. + * @param data The transaction data. + * @param operation The type of operation of the module transaction. + * @param module The module involved in the transaction. + * @return moduleTxHash The hash of the module transaction. + */ + function checkModuleTransaction( + address to, + uint256 value, + bytes memory data, + Enum.Operation operation, + address module + ) external override returns (bytes32 moduleTxHash) { + // updates transaction checked + preCheckedTransactions = true ; + // if it passes, it returns a string of bytes + return bytes32(0); + } + + /** + * @notice Checks after execution of module transaction. + * @dev The function needs to implement a check after the execution of the module transaction. + * @param txHash The hash of the module transaction. + * @param success The status of the module transaction execution. + */ + function checkAfterModuleExecution(bytes32 txHash, bool success) external override { + postCheckedTransactions = true; + } + + /** + * @dev Returns true if this contract implements the interface defined by `interfaceId`. + * See the corresponding EIP section + * https://eips.ethereum.org/EIPS/eip-165#how-interfaces-are-identified + * to learn more about how these ids are created. + * + * This function call must use less than 30 000 gas. + */ + function supportsInterface(bytes4 interfaceId) external view virtual override returns (bool) { + return + interfaceId == type(IModuleGuard).interfaceId || // 0x58401ed8 + interfaceId == type(IERC165).interfaceId; // 0x01ffc9a7 + } + +} \ No newline at end of file diff --git a/certora/mocks/ModuleGuardMockDuplicate.sol b/certora/mocks/ModuleGuardMockDuplicate.sol new file mode 100644 index 000000000..0bb7e3420 --- /dev/null +++ b/certora/mocks/ModuleGuardMockDuplicate.sol @@ -0,0 +1,71 @@ +// SPDX-License-Identifier: LGPL-3.0-only +/* solhint-disable one-contract-per-file */ +pragma solidity >=0.7.0 <0.9.0; +import {IModuleGuard} from "../munged/base/ModuleManager.sol"; +import {IERC165} from "../munged/interfaces/IERC165.sol"; +import "../munged/libraries/Enum.sol"; + +contract ModuleGuardMockDuplicate is IModuleGuard { + + constructor(){ + preCheckedTransactions = false ; + postCheckedTransactions = false ; + } + + // some mock variables + bool public preCheckedTransactions ; + bool public postCheckedTransactions ; + + function resetChecks() external { + preCheckedTransactions = false ; + postCheckedTransactions = false ; + } + + /** + * @notice Checks the module transaction details. + * @dev The function needs to implement module transaction validation logic. + * @param to The address to which the transaction is intended. + * @param value The value of the transaction in Wei. + * @param data The transaction data. + * @param operation The type of operation of the module transaction. + * @param module The module involved in the transaction. + * @return moduleTxHash The hash of the module transaction. + */ + function checkModuleTransaction( + address to, + uint256 value, + bytes memory data, + Enum.Operation operation, + address module + ) external override returns (bytes32 moduleTxHash) { + // updates transaction checked + preCheckedTransactions = true ; + // if it passes, it returns a string of bytes + return bytes32(0); + } + + /** + * @notice Checks after execution of module transaction. + * @dev The function needs to implement a check after the execution of the module transaction. + * @param txHash The hash of the module transaction. + * @param success The status of the module transaction execution. + */ + function checkAfterModuleExecution(bytes32 txHash, bool success) external override { + postCheckedTransactions = true; + } + + /** + * @dev Returns true if this contract implements the interface defined by `interfaceId`. + * See the corresponding EIP section + * https://eips.ethereum.org/EIPS/eip-165#how-interfaces-are-identified + * to learn more about how these ids are created. + * + * This function call must use less than 30 000 gas. + */ + function supportsInterface(bytes4 interfaceId) external view virtual override returns (bool) { + return + interfaceId == type(IModuleGuard).interfaceId || // 0x58401ed8 + interfaceId == type(IERC165).interfaceId; // 0x01ffc9a7 + } + +} \ No newline at end of file diff --git a/certora/mocks/TxnGuardMock.sol b/certora/mocks/TxnGuardMock.sol new file mode 100644 index 000000000..7d8c921be --- /dev/null +++ b/certora/mocks/TxnGuardMock.sol @@ -0,0 +1,78 @@ +// SPDX-License-Identifier: LGPL-3.0-only +/* solhint-disable one-contract-per-file */ +pragma solidity >=0.7.0 <0.9.0; +import {ITransactionGuard} from "../munged/base/GuardManager.sol"; +import {IERC165} from "../munged/interfaces/IERC165.sol"; +import "../munged/libraries/Enum.sol"; + +contract TxnGuardMock is ITransactionGuard { + + constructor(){} + + // some mock variables + bool public preCheckedTransactions ; + bool public postCheckedTransactions ; + + function resetChecks() external { + preCheckedTransactions = false ; + postCheckedTransactions = false ; + } + + /** + * @notice Checks the transaction details. + * @dev The function needs to implement transaction validation logic. + * @param to The address to which the transaction is intended. + * @param value The value of the transaction in Wei. + * @param data The transaction data. + * @param operation The type of operation of the transaction. + * @param safeTxGas Gas used for the transaction. + * @param baseGas The base gas for the transaction. + * @param gasPrice The price of gas in Wei for the transaction. + * @param gasToken The token used to pay for gas. + * @param refundReceiver The address which should receive the refund. + * @param signatures The signatures of the transaction. + * @param msgSender The address of the message sender. + */ + function checkTransaction( + address to, + uint256 value, + bytes memory data, + Enum.Operation operation, + uint256 safeTxGas, + uint256 baseGas, + uint256 gasPrice, + address gasToken, + address payable refundReceiver, + bytes memory signatures, + address msgSender + ) external override { + // updates transaction checked + preCheckedTransactions = true; + } + + /** + * @notice Checks after execution of the transaction. + * @dev The function needs to implement a check after the execution of the transaction. + * @param hash The hash of the transaction. + * @param success The status of the transaction execution. + */ + function checkAfterExecution(bytes32 hash, bool success) external override { + // updates transaction checked + postCheckedTransactions = true ; + } + + /** + * @dev Returns true if this contract implements the interface defined by `interfaceId`. + * See the corresponding EIP section + * https://eips.ethereum.org/EIPS/eip-165#how-interfaces-are-identified + * to learn more about how these ids are created. + * + * This function call must use less than 30 000 gas. + */ + function supportsInterface(bytes4 interfaceId) external view virtual override returns (bool) { + return + interfaceId == type(ITransactionGuard).interfaceId || // 0xe6d7a83a + interfaceId == type(IERC165).interfaceId; // 0x01ffc9a7 + } + +} \ No newline at end of file diff --git a/certora/mocks/TxnGuardMockDuplicate.sol b/certora/mocks/TxnGuardMockDuplicate.sol new file mode 100644 index 000000000..8b7ad8a27 --- /dev/null +++ b/certora/mocks/TxnGuardMockDuplicate.sol @@ -0,0 +1,78 @@ +// SPDX-License-Identifier: LGPL-3.0-only +/* solhint-disable one-contract-per-file */ +pragma solidity >=0.7.0 <0.9.0; +import {ITransactionGuard} from "../munged/base/GuardManager.sol"; +import {IERC165} from "../munged/interfaces/IERC165.sol"; +import "../munged/libraries/Enum.sol"; + +contract TxnGuardMockDuplicate is ITransactionGuard { + + constructor(){} + + // some mock variables + bool public preCheckedTransactions ; + bool public postCheckedTransactions ; + + function resetChecks() external { + preCheckedTransactions = false ; + postCheckedTransactions = false ; + } + + /** + * @notice Checks the transaction details. + * @dev The function needs to implement transaction validation logic. + * @param to The address to which the transaction is intended. + * @param value The value of the transaction in Wei. + * @param data The transaction data. + * @param operation The type of operation of the transaction. + * @param safeTxGas Gas used for the transaction. + * @param baseGas The base gas for the transaction. + * @param gasPrice The price of gas in Wei for the transaction. + * @param gasToken The token used to pay for gas. + * @param refundReceiver The address which should receive the refund. + * @param signatures The signatures of the transaction. + * @param msgSender The address of the message sender. + */ + function checkTransaction( + address to, + uint256 value, + bytes memory data, + Enum.Operation operation, + uint256 safeTxGas, + uint256 baseGas, + uint256 gasPrice, + address gasToken, + address payable refundReceiver, + bytes memory signatures, + address msgSender + ) external override { + // updates transaction checked + preCheckedTransactions = true; + } + + /** + * @notice Checks after execution of the transaction. + * @dev The function needs to implement a check after the execution of the transaction. + * @param hash The hash of the transaction. + * @param success The status of the transaction execution. + */ + function checkAfterExecution(bytes32 hash, bool success) external override { + // updates transaction checked + postCheckedTransactions = true ; + } + + /** + * @dev Returns true if this contract implements the interface defined by `interfaceId`. + * See the corresponding EIP section + * https://eips.ethereum.org/EIPS/eip-165#how-interfaces-are-identified + * to learn more about how these ids are created. + * + * This function call must use less than 30 000 gas. + */ + function supportsInterface(bytes4 interfaceId) external view virtual override returns (bool) { + return + interfaceId == type(ITransactionGuard).interfaceId || // 0xe6d7a83a + interfaceId == type(IERC165).interfaceId; // 0x01ffc9a7 + } + +} \ No newline at end of file diff --git a/certora/specs/Execute.spec b/certora/specs/Execute.spec new file mode 100644 index 000000000..5271f339b --- /dev/null +++ b/certora/specs/Execute.spec @@ -0,0 +1,161 @@ +/* A specification for the exstensible fallback handler */ + + +// ---- Methods block ---------------------------------------------------------- +methods { + + // envfree + function numSigsSufficient(bytes signatures,uint256 requiredSignatures) external returns (bool) envfree; + + function _.checkTransaction( + address to, + uint256 value, + bytes data, + Enum.Operation operation, + uint256 safeTxGas, + uint256 baseGas, + uint256 gasPrice, + address gasToken, + address refundReceiver, + bytes signatures, + address msgSender + ) external => DISPATCHER(true) ; + + function _.checkAfterExecution(bytes32 hash, bool success) external + => DISPATCHER(true); + + function Executor.execute( + address to, + uint256 value, + bytes memory data, + Enum.Operation operation, + uint256 txGas + ) internal returns (bool) => execute_summary(); + + function SecuredTokenTransfer.transferToken(address token, address receiver, uint256 amount) internal returns (bool) => NONDET ; + function Safe.handlePayment( + uint256 gasUsed, + uint256 baseGas, + uint256 gasPrice, + address gasToken, + address refundReceiver + ) internal returns (uint256) => NONDET ; + +} + +// ---- Functions and ghosts --------------------------------------------------- + +persistent ghost bool execute_called { init_state axiom execute_called == false; } + +function execute_summary() returns bool { + execute_called = true ; + bool new_var ; + return new_var ; +} + +// ---- Invariants ------------------------------------------------------------- + + +// ---- Rules ------------------------------------------------------------------ + +/// @dev a successful call to execTransactionFromModule must be from enabled module +rule execTxnModulePermissions( + address to, + uint256 value, + bytes data, + Enum.Operation operation) { + env e; + bool module_enabled = isModuleEnabled(e,e.msg.sender) ; + + // execTxn from module passes + execTransactionFromModule(e,to,value,data,operation); + + // msg sender is the module + assert (module_enabled); +} + +/// @dev a successful call to execTransactionFromModuleReturnData must be from enabled module +rule execTxnModuleReturnDataPermissions( + address to, + uint256 value, + bytes data, + Enum.Operation operation) { + env e; + bool module_enabled = isModuleEnabled(e,e.msg.sender) ; + + // execTxn from module passes + execTransactionFromModuleReturnData(e,to,value,data,operation); + + // msg sender is the module + assert (module_enabled); +} + + +/// @dev execute can only be called by execTransaction or execTransactionFromModule +rule executePermissions(method f) filtered { + f -> f.selector != sig:simulateAndRevert(address,bytes).selector && + f.selector != sig:getStorageAt(uint256,uint256).selector +} { + env e; + require !execute_called; + + calldataarg args; + f(e, args); + + assert (execute_called => + f.selector == sig:execTransaction( + address, + uint256, + bytes, + Enum.Operation, + uint256, + uint256, + uint256, + address, + address, + bytes).selector || + f.selector == sig:execTransactionFromModule( + address, + uint256, + bytes, + Enum.Operation).selector) || + f.selector == sig:execTransactionFromModuleReturnData( + address, + uint256, + bytes, + Enum.Operation).selector || + f.selector == sig:setup( + address[], + uint256, + address, + bytes, + address, + address, + uint256, + address).selector; +} + + +/// @dev at least "threshold" signatures provided +rule executeThresholdMet( + address to, + uint256 value, + bytes data, + Enum.Operation operation, + uint256 safeTxGas, + uint256 baseGas, + uint256 gasPrice, + address gasToken, + address refundReceiver, + bytes signatures +) { + env e; + uint256 threshold = getThreshold(e); + + // a call to execTxn succeeds + execTransaction(e,to,value,data,operation,safeTxGas,baseGas, + gasPrice,gasToken,refundReceiver,signatures); + + // an added function to the harness SafeHarness.sol that checks signature numbers + assert (numSigsSufficient(signatures,threshold)); +} \ No newline at end of file diff --git a/certora/specs/Extensible.spec b/certora/specs/Extensible.spec new file mode 100644 index 000000000..9044b9dc9 --- /dev/null +++ b/certora/specs/Extensible.spec @@ -0,0 +1,74 @@ +/* A specification for the exstensible fallback handler */ + +using ExtensibleFallbackHandlerHarness as fallbackHandler; +using DummyHandler as dummyHandler; +using SafeHarness as safe; + +// ---- Methods block ---------------------------------------------------------- +methods { + + function getFallbackHandler() external returns (address) envfree; + function _.handle(address _safe, address sender, uint256 value, bytes data) external => DISPATCHER(true); + + unresolved external in safe._ => DISPATCH(use_fallback=true) [ + fallbackHandler._ + ] default NONDET; + + unresolved external in callDummyHandler(bytes4) => DISPATCH(use_fallback=true) [ + safe._ + ] default NONDET; + +} + +// ---- Functions and ghosts --------------------------------------------------- + + + +// ---- Invariants ------------------------------------------------------------- + + + +// ---- Rules ------------------------------------------------------------------ + +/// @dev a handler, once set via setSafeMethod, is possible to call +rule handlerCallableIfSet(method f, bytes4 selector) filtered { f -> f.isFallback } { + env e; + + // the fallback handler is in the scene + require (getFallbackHandler() == fallbackHandler); + + // the dummy (sub) handler is a valid handler for this safe + bytes32 dummy_bytes = to_bytes32(assert_uint256(dummyHandler)); + fallbackHandler.setSafeMethod(e,selector,dummy_bytes); // we've set the dummy as a handler + + // reset the check to see if dummy handler has been called + dummyHandler.resetMethodCalled(e); + + // call the fallback method of the Safe contract + calldataarg args ; + f(e,args); + + // there is an execution path that calls the connected dummy handler + satisfy (dummyHandler.methodCalled(e)); +} + +/// @dev a handler is called under expected conditions +rule handlerCalledIfSet() { + env e; + + // the fallback handler is in the scene + require (getFallbackHandler() == fallbackHandler); + + // the dummy (sub) handler is a valid handler for this safe + bytes32 dummy = to_bytes32(assert_uint256(dummyHandler)); + bytes4 selector = to_bytes4(sig:dummyHandler.dummyMethod().selector); + callSetSafeMethod(e,selector,dummy); // we've set the dummy as a handler + + // reset the check to see if dummy handler has been called + dummyHandler.resetMethodCalled(e); + + callDummyHandler(e,selector); + + // there is an execution path that calls the connected dummy handler + assert (dummyHandler.methodCalled(e)); +} \ No newline at end of file diff --git a/certora/specs/Fallback.spec b/certora/specs/Fallback.spec new file mode 100644 index 000000000..07c02164d --- /dev/null +++ b/certora/specs/Fallback.spec @@ -0,0 +1,84 @@ +/* A specification for the exstensible fallback handler */ + +using ExtensibleFallbackHandlerHarness as fallbackHandler; +using SafeHarness as safe; + +// ---- Methods block ---------------------------------------------------------- +methods { + + function getFallbackHandler() external returns (address) envfree; + function _.handle(address _safe, address sender, uint256 value, bytes data) external => DISPATCHER(true); + +} + +// ---- Functions and ghosts --------------------------------------------------- + + + +// ---- Invariants ------------------------------------------------------------- + + + +// ---- Rules ------------------------------------------------------------------ + +/// @dev fallback handler gets set by setFallbackHandler +rule setFallbackIntegrity(address handler) { + env e; + + setFallbackHandler(e,handler); + address this_handler = getFallbackHandler(); + + assert (this_handler == handler); +} + +/// @dev invariant: the address in fallback handler slot is never self +invariant fallbackHandlerNeverSelf() + getFallbackHandler() != safe + filtered { + f -> f.selector != sig:simulateAndRevert(address,bytes).selector + } + +/// @dev for soundness of fallbackHandlerNeverSelf, we prove a rule that simulateAndRevert always reverts +rule simulateAndRevertReverts(address caddr, bytes b) { + env e; + simulateAndRevert@withrevert(e,caddr,b); + assert lastReverted; +} + +/// @dev setSafeMethod sets the handler +rule setSafeMethodSets(bytes4 selector, address newMethodCaddr) { + env e; + + bytes32 newMethod = to_bytes32(assert_uint256(newMethodCaddr)); + + fallbackHandler.setSafeMethod(e,selector,newMethod); + bytes32 thisMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector); + + assert (thisMethod == newMethod); +} + +/// @dev setSafeMethod removes the handler +rule setSafeMethodRemoves(bytes4 selector) { + env e; + + bytes32 newMethod = to_bytes32(0); // call setSafeMethod with the zero address + + fallbackHandler.setSafeMethod(e,selector,newMethod); + bytes32 thisMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector); + + assert (thisMethod == to_bytes32(0)); // there is nothing stored +} + +/// @dev setSafeMethod changes the handler +rule setSafeMethodChanges(bytes4 selector, address newMethodCaddr) { + env e; + + bytes32 newMethod = to_bytes32(assert_uint256(newMethodCaddr)); + bytes32 oldMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector); + require (newMethod != oldMethod); // we are changing the method address + + fallbackHandler.setSafeMethod(e,selector,newMethod); + bytes32 thisMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector); + + assert (thisMethod == newMethod); +} \ No newline at end of file diff --git a/certora/specs/Guards.spec b/certora/specs/Guards.spec new file mode 100644 index 000000000..b32999d70 --- /dev/null +++ b/certora/specs/Guards.spec @@ -0,0 +1,219 @@ +/* A specification of the safe guard and module guard */ + +using ModuleGuardMock as modGuardMock; +using ModuleGuardMockDuplicate as modGuardMock2; +using TxnGuardMock as txnGuardMock; +using TxnGuardMockDuplicate as txnGuardMock2; +using SafeHarness as safe; + +// ---- Methods block ---------------------------------------------------------- +methods { + function getModuleGuardExternal() external returns (address) envfree; + function getSafeGuard() external returns (address) envfree; + + function txnGuardMock.preCheckedTransactions() external returns (bool) envfree; + function txnGuardMock.postCheckedTransactions() external returns (bool) envfree; + function modGuardMock.preCheckedTransactions() external returns (bool) envfree; + function modGuardMock.postCheckedTransactions() external returns (bool) envfree; + + function _.checkModuleTransaction( + address to, + uint256 value, + bytes data, + Enum.Operation operation, + address module + ) external => DISPATCHER(true) ; + + function _.checkAfterModuleExecution(bytes32 txHash, bool success) external + => DISPATCHER(true) ; + + function _.checkTransaction( + address to, + uint256 value, + bytes data, + Enum.Operation operation, + uint256 safeTxGas, + uint256 baseGas, + uint256 gasPrice, + address gasToken, + address refundReceiver, + bytes signatures, + address msgSender + ) external => DISPATCHER(true) ; + + function _.checkAfterExecution(bytes32 hash, bool success) external + => DISPATCHER(true); + + function Executor.execute( + address to, + uint256 value, + bytes memory data, + Enum.Operation operation, + uint256 txGas + ) internal returns (bool) => NONDET; + + function SecuredTokenTransfer.transferToken(address token, address receiver, uint256 amount) internal returns (bool) => NONDET ; + function Safe.handlePayment( + uint256 gasUsed, + uint256 baseGas, + uint256 gasPrice, + address gasToken, + address refundReceiver + ) internal returns (uint256) => NONDET ; + +} + +// ---- Functions and ghosts --------------------------------------------------- + + +// ---- Invariants ------------------------------------------------------------- + + +// ---- Rules ------------------------------------------------------------------ + +/// @dev the only method that can change the guard is setGuard +rule guardAddressChange(method f) filtered { + f -> f.selector != sig:simulateAndRevert(address,bytes).selector && + f.selector != sig:getStorageAt(uint256,uint256).selector +} { + address guardBefore = getSafeGuard(); + + calldataarg args; env e; + f(e, args); + + address guardAfter = getSafeGuard(); + + assert guardBefore != guardAfter => + f.selector == sig:setGuard(address).selector; +} + +/// @dev the only method that can change the module guard is setModuleGuard +rule moduleGuardAddressChange(method f) filtered { + f -> f.selector != sig:simulateAndRevert(address,bytes).selector && + f.selector != sig:getStorageAt(uint256,uint256).selector +} { + address guardBefore = getModuleGuardExternal(); + + calldataarg args; env e; + f(e,args); + + address guardAfter = getModuleGuardExternal(); + + assert guardBefore != guardAfter => + f.selector == sig:setModuleGuard(address).selector; +} + +/// @dev set-get correspondence for (regular) guard +rule setGetCorrespondenceGuard(address guard) { + env e; + setGuard(e,guard); + address gotGuard = getSafeGuard(); + assert guard == gotGuard; +} + +/// @dev set-get correspodnence for module guard +rule setGetCorrespondenceModuleGuard(address guard) { + env e; + setModuleGuard(e,guard); + address gotGuard = getModuleGuardExternal(); + assert guard == gotGuard; +} + +/// @dev setGuard can only be called by contract itself. +rule setGuardReentrant(address guard) { + env e; + setGuard(e,guard); // a successful call to setGuard + assert (e.msg.sender == safe); +} + +/// @dev setModuleGuard can only be called by contract itself. +rule setModuleGuardReentrant(address guard) { + env e; + setModuleGuard(e,guard); + assert(e.msg.sender == safe); +} + + +/// @dev the transaction guard gets called both pre- and post- any execTransaction +rule txnGuardCalled( + address to, + uint256 value, + bytes data, + Enum.Operation operation, + uint256 safeTxGas, + uint256 baseGas, + uint256 gasPrice, + address gasToken, + address refundReceiver, + bytes signatures +) { + env e; + // the txn guard is the mock + require (getSafeGuard() == txnGuardMock); + + txnGuardMock.resetChecks(e); // reset the check triggers + txnGuardMock2.resetChecks(e); + + execTransaction(e,to,value,data,operation,safeTxGas,baseGas, + gasPrice,gasToken,refundReceiver,signatures); + + // the pre- and post- module transaction guards were called + assert ( + txnGuardMock.preCheckedTransactions() && + txnGuardMock.postCheckedTransactions() && + // the right guard was called + !txnGuardMock2.preCheckedTransactions(e) && + !txnGuardMock2.postCheckedTransactions(e) + ); +} + +/// @dev the module guard gets called both pre- and post- any execTransactionFromModule +rule moduleGuardCalled( + address to, + uint256 value, + bytes data, + Enum.Operation operation) { + env e; + // the module guard is the mock + require (getModuleGuardExternal() == modGuardMock); + + modGuardMock.resetChecks(e); // reset the check triggers + modGuardMock2.resetChecks(e); + + execTransactionFromModule(e,to,value,data,operation); + + // the pre- and post- module transaction guards were called + assert ( + modGuardMock.preCheckedTransactions() && + modGuardMock.postCheckedTransactions() && + // the correct guard was called + !modGuardMock2.preCheckedTransactions(e) && + !modGuardMock2.postCheckedTransactions(e) + ); +} + +/// @dev the module guard gets called both pre- and post- any execTransactionFromModuleReturnData +rule moduleGuardCalledReturn( + address to, + uint256 value, + bytes data, + Enum.Operation operation) { + env e; + // the module guard is the mock + require (getModuleGuardExternal() == modGuardMock); + + modGuardMock.resetChecks(e); // reset the check triggers + modGuardMock2.resetChecks(e); + + execTransactionFromModuleReturnData(e,to,value,data,operation); + + // the pre- and post- module transaction guards were called + assert ( + modGuardMock.preCheckedTransactions() && + modGuardMock.postCheckedTransactions() && + // the correct guard was called + !modGuardMock2.preCheckedTransactions(e) && + !modGuardMock2.postCheckedTransactions(e) + ); +} + diff --git a/certora/specs/Hash.spec b/certora/specs/Hash.spec new file mode 100644 index 000000000..218ebdc4a --- /dev/null +++ b/certora/specs/Hash.spec @@ -0,0 +1,43 @@ +/* A specification for the Safe setup function */ + + +// ---- Methods block ---------------------------------------------------------- +methods { + function getThreshold() external returns (uint256) envfree; + + function SecuredTokenTransfer.transferToken(address token, address receiver, uint256 amount) internal returns (bool) => NONDET ; +} + +// ---- Functions and ghosts --------------------------------------------------- + + +// ---- Invariants ------------------------------------------------------------- + + +// ---- Rules ------------------------------------------------------------------ + +/// @dev approvedHashes[user][hash] can only be changed by msg.sender==user +rule approvedHashesUpdate(method f,bytes32 userHash,address user) filtered { + f -> f.selector != sig:simulateAndRevert(address,bytes).selector +} { + env e; + + uint256 hashBefore = approvedHashVal(e,user,userHash); + + calldataarg args; + f(e,args); + + uint256 hashAfter = approvedHashVal(e,user,userHash); + + assert (hashBefore != hashAfter => + (e.msg.sender == user) + ); +} + + +/// @dev approvedHashes is set when calling approveHash +rule approvedHashesSet(bytes32 hashToApprove) { + env e; + approveHash(e,hashToApprove); + assert(approvedHashVal(e,e.msg.sender,hashToApprove) == 1); +} \ No newline at end of file diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec index cdb749726..2795523d8 100644 --- a/certora/specs/Safe.spec +++ b/certora/specs/Safe.spec @@ -131,21 +131,6 @@ rule setupCorrectlyConfiguresSafe( } -rule guardAddressChange(method f) filtered { - f -> f.selector != sig:simulateAndRevert(address,bytes).selector && - f.selector != sig:getStorageAt(uint256,uint256).selector -} { - address guardBefore = getSafeGuard(); - - calldataarg args; env e; - f(e, args); - - address guardAfter = getSafeGuard(); - - assert guardBefore != guardAfter => - f.selector == sig:setGuard(address).selector; -} - invariant noSignedMessages(bytes32 message) signedMessages(message) == 0 filtered { f -> reachableOnly(f) } diff --git a/certora/specs/Setup.spec b/certora/specs/Setup.spec new file mode 100644 index 000000000..9b413fd61 --- /dev/null +++ b/certora/specs/Setup.spec @@ -0,0 +1,43 @@ +/* A specification for the Safe setup function */ + + +// ---- Methods block ---------------------------------------------------------- +methods { + function getThreshold() external returns (uint256) envfree; + + function SecuredTokenTransfer.transferToken(address token, address receiver, uint256 amount) internal returns (bool) => NONDET ; +} + +// ---- Functions and ghosts --------------------------------------------------- + + +// ---- Invariants ------------------------------------------------------------- + + +// ---- Rules ------------------------------------------------------------------ + +/// @dev setup can only be called if threshold = 0 and setup sets threshold > 0 +rule setupThresholdZeroAndSetsPositiveThreshold( + address[] _owners, + uint256 _threshold, + address to, + bytes data, + address fallbackHandler, + address paymentToken, + uint256 payment, + address paymentReceiver) { + env e; + + uint256 old_threshold = getThreshold(); + + // a successful call to setup + setup(e,_owners,_threshold,to,data,fallbackHandler, + paymentToken,payment,paymentReceiver); + + uint256 new_threshold = getThreshold(); + + assert ( + new_threshold > 0 && + old_threshold == 0 + ); +}