diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch index 3f6742286..6351b1ca3 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-11 12:09:10 ++++ Safe.sol 2024-12-12 17:55:22 @@ -75,22 +75,24 @@ * so we create a Safe with 0 owners and threshold 1. * This is an unusable Safe, perfect for the singleton @@ -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 +@@ -450,7 +451,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-11 12:09:10 ++++ base/Executor.sol 2024-12-12 17:55:22 @@ -26,12 +26,8 @@ uint256 txGas ) internal returns (bool success) { @@ -70,8 +81,8 @@ diff -druN base/Executor.sol base/Executor.sol /* solhint-disable no-inline-assembly */ /// @solidity memory-safe-assembly 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 +--- interfaces/ISafe.sol 2024-12-11 12:09:10 ++++ interfaces/ISafe.sol 2024-12-12 17:55:22 @@ -110,7 +110,7 @@ */ function domainSeparator() external view returns (bytes32); diff --git a/certora/conf/v1.5/execute.conf b/certora/conf/v1.5/execute.conf new file mode 100644 index 000000000..3972e17c0 --- /dev/null +++ b/certora/conf/v1.5/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/v1.5/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/v1.5/fallback.conf b/certora/conf/v1.5/fallback.conf new file mode 100644 index 000000000..4e7621973 --- /dev/null +++ b/certora/conf/v1.5/fallback.conf @@ -0,0 +1,27 @@ +{ + "files": [ + "certora/harnesses/SafeHarness.sol", + "certora/harnesses/ExtensibleFallbackHandlerHarness.sol", + "certora/mocks/DummyHandler.sol" + ], + "link": [ + + ], + "verify": "SafeHarness:certora/specs/v1.5/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/v1.5/guards.conf b/certora/conf/v1.5/guards.conf new file mode 100644 index 000000000..0c7f1484f --- /dev/null +++ b/certora/conf/v1.5/guards.conf @@ -0,0 +1,33 @@ +// a conf file for safe module guards +{ + "files": [ + "certora/harnesses/SafeHarness.sol", + "certora/mocks/ModuleGuardMock.sol", // a module guard + "certora/mocks/TxnGuardMock.sol", // a (safe) guard + ], + "link": [ + + ], + "verify": "SafeHarness:certora/specs/v1.5/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/v1.5/hash.conf b/certora/conf/v1.5/hash.conf new file mode 100644 index 000000000..9e82324e9 --- /dev/null +++ b/certora/conf/v1.5/hash.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "certora/harnesses/SafeHarness.sol" + ], + "link": [ + + ], + "verify": "SafeHarness:certora/specs/v1.5/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/v1.5/setup.conf b/certora/conf/v1.5/setup.conf new file mode 100644 index 000000000..71a505028 --- /dev/null +++ b/certora/conf/v1.5/setup.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "certora/harnesses/SafeHarness.sol" + ], + "link": [ + + ], + "verify": "SafeHarness:certora/specs/v1.5/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..590d5bd33 --- /dev/null +++ b/certora/harnesses/ExtensibleFallbackHandlerHarness.sol @@ -0,0 +1,15 @@ +// 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]; + } + + function getContextAndHandler() external view returns (ISafe safe, address sender, bool isStatic, address handler) { + _getContextAndHandler(); + } + +} \ 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/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/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/v1.5/Execute.spec b/certora/specs/v1.5/Execute.spec new file mode 100644 index 000000000..38b2f91ac --- /dev/null +++ b/certora/specs/v1.5/Execute.spec @@ -0,0 +1,167 @@ +/* A specification for the exstensible fallback handler */ + + +// ---- Methods block ---------------------------------------------------------- +methods { + + // envfree + function numSigsSufficient(bytes signatures,uint256 requiredSignatures) external returns (bool) envfree; + + // function _.isValidSignature(bytes32 _hash, bytes _signature) 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) => 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 +/// @status Done: https://prover.certora.com/output/39601/dcc09acbeead4df9868519a4ac0e3ee5?anonymousKey=327efa3ac9dde7907db389b3a2688ce42094ef41 +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 +/// @status Done: https://prover.certora.com/output/39601/49c3745804084c5aa7284792f805316b?anonymousKey=356721ccd4d2592e83a5fbf1ee58ed278e8dd9ff +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 +/// @status Done: https://prover.certora.com/output/39601/9b60b63b5aa84428b9fca530f870c4b6?anonymousKey=4b731a650337bea416faf81e806d96a7b040f8e8 +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 +/// @status Done: https://prover.certora.com/output/39601/9f364fac5e8c43e0acc2d93cea3f5560?anonymousKey=d37fb383bff8fa2fe0dacf60b61130e1aadf2ad4 +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/v1.5/Fallback.spec b/certora/specs/v1.5/Fallback.spec new file mode 100644 index 000000000..c1ece76bc --- /dev/null +++ b/certora/specs/v1.5/Fallback.spec @@ -0,0 +1,160 @@ +/* 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 fallback handler gets set by setFallbackHandler +/// @status Done: https://prover.certora.com/output/39601/ab995049df0b454b888f3cd6a27331d5?anonymousKey=1a710fa917c8c60a9a420e026d6570d91e1e923b +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 +/// @status Done: https://prover.certora.com/output/39601/edb75f86f23445cdbc7cd7b5c4c420b6?anonymousKey=62191f4f70404bcbce784f5172e3ed7ab323d416 +invariant fallbackHanlderNeverSelf() + getFallbackHandler() != safe + filtered { + f -> f.selector != sig:simulateAndRevert(address,bytes).selector + } + +/// @status TODOviolation: https://prover.certora.com/output/39601/cfde79a198b34aa78dbc5714a5e416b6?anonymousKey=f3e41441fbb2f941efc2033b10cccdee7c84249e +invariant fallbackHanlderNeverZero() + getFallbackHandler() != 0 + filtered { + f -> f.selector != sig:simulateAndRevert(address,bytes).selector + } + +/// @dev for soundness of fallbackHanlderNeverSelf, we prove a rule that simulateAndRevert always reverts +/// @status Done: https://prover.certora.com/output/39601/38653935d0db460994d1a8c5bfdf57bb?anonymousKey=988218ca4f784fd27ea96fd2f14644719e2e9468 +rule simulateAndRevertReverts(address caddr, bytes b) { + env e; + simulateAndRevert@withrevert(e,caddr,b); + assert lastReverted; +} + +/// @dev setSafeMethod sets the handler +/// @status Done: https://prover.certora.com/output/39601/bab9860cdfc44a83bed82e79d8c06218?anonymousKey=b4c5dbef050bb201ad78b3dd5af5cdca8ffa9f92 +rule setSafeMethodSets(bytes4 selector, address newMethodCaddr) { + env e; + + bytes32 newMethod = to_bytes32(assert_uint256(newMethodCaddr)); + + fallbackHandler.setSafeMethod(e,selector,newMethod); + // callSetSafeMethod(e,selector,newMethod); + bytes32 thisMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector); + + assert (thisMethod == newMethod); +} + +/// @dev setSafeMethod removes the handler +/// @status Done: https://prover.certora.com/output/39601/8591535c4a434f3e826af00b95ea1ca8?anonymousKey=a7b6743a3161a3289883f99014619a9d6e7196e1 +/// note this is a special case of the rule above, but we still include it here for illustration +rule setSafeMethodRemoves(bytes4 selector) { + env e; + + bytes32 newMethod = to_bytes32(0); // call setSafeMethod with the zero address + + fallbackHandler.setSafeMethod(e,selector,newMethod); + // callSetSafeMethod(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 +/// @status Done: https://prover.certora.com/output/39601/b44efe9ef3bd4ff5a1af710a7d3d7ee4?anonymousKey=7fd15cc355164c803123c27b41660fed34548647 +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); + // callSetSafeMethod(e,selector,newMethod); + + bytes32 thisMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector); + + assert (thisMethod == newMethod); +} + + +/// @dev a handler, once set via setSafeMethod, is possible to call +/// @status Done: https://prover.certora.com/output/39601/9fcde04ecd434963b9ce788f7ddea8c1?anonymousKey=a7efde58b28ef7c99264424b66984a8d39b78518 +rule hanlderCallableIfSet(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 +/// @status violated due to Prover bug: https://prover.certora.com/output/39601/c3379d53af8d4639b2236d0be41af6b9?anonymousKey=df18d967edb98b99e5851a280d84728ce18724cb +rule handlerCalledIfSet() { + env e; + + requireInvariant fallbackHanlderNeverSelf(); + requireInvariant fallbackHanlderNeverZero(); + + // 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/v1.5/Guards.spec b/certora/specs/v1.5/Guards.spec new file mode 100644 index 000000000..d18243add --- /dev/null +++ b/certora/specs/v1.5/Guards.spec @@ -0,0 +1,212 @@ +/* A specification of the safe guard and module guard */ + +using ModuleGuardMock as modGuardMock; +using TxnGuardMock as txnGuardMock; +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 +/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d +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 +/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d + +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 +/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d +rule setGetCorrespondenceGuard(address guard) { + env e; + setGuard(e,guard); + address gotGuard = getSafeGuard(); + assert guard == gotGuard; +} + +/// @dev set-get correspodnence for module guard +/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d +rule setGetCorrespondenceModuleGuard(address guard) { + env e; + setModuleGuard(e,guard); + address gotGuard = getModuleGuardExternal(); + assert guard == gotGuard; +} + +/// @dev setGuard can only be called by contract itself. +/// @status Done: https://prover.certora.com/output/39601/b78bb57e77e444ad9d89861a8dc66e9f?anonymousKey=b6452b2c9f788d4a4dcd8d3c41f16a3e66e64a66 +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. +/// @status Done: https://prover.certora.com/output/39601/8147e74eda404e61bcb6fc8e8849c5f3?anonymousKey=5c1e77468b6f5bff22c376894dca846f5ea83aab +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 +/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d +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); + + // execTxn passes + 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() + ); +} + +/// @dev the module guard gets called both pre- and post- any execTransactionFromModule +/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d +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 + execTransactionFromModule(e,to,value,data,operation); + + // the pre- and post- module transaction guards were called + assert ( + modGuardMock.preCheckedTransactions() && + modGuardMock.postCheckedTransactions() + ); +} + +/// @dev the module guard gets called both pre- and post- any execTransactionFromModuleReturnData +/// @status Done: https://prover.certora.com/output/39601/15cfd3430d794986a26d304c9e2fbc6e?anonymousKey=92f0976aba6cb3fe40cf6c728d34b140a438bbae +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 + execTransactionFromModuleReturnData(e,to,value,data,operation); + + // the pre- and post- module transaction guards were called + assert ( + modGuardMock.preCheckedTransactions() && + modGuardMock.postCheckedTransactions() + ); +} + diff --git a/certora/specs/v1.5/Hash.spec b/certora/specs/v1.5/Hash.spec new file mode 100644 index 000000000..0e9b986dc --- /dev/null +++ b/certora/specs/v1.5/Hash.spec @@ -0,0 +1,47 @@ +/* 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 +/// @status Done: https://prover.certora.com/output/39601/bb515eafa67e4edd99bb5aa51a63877b?anonymousKey=9c42e3105c1c3a3fbc95c8a24fa43b3dd43a05d6 + +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 +/// @status Done: https://prover.certora.com/output/39601/bb515eafa67e4edd99bb5aa51a63877b?anonymousKey=9c42e3105c1c3a3fbc95c8a24fa43b3dd43a05d6 + +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/v1.5/Setup.spec b/certora/specs/v1.5/Setup.spec new file mode 100644 index 000000000..67217d450 --- /dev/null +++ b/certora/specs/v1.5/Setup.spec @@ -0,0 +1,45 @@ +/* 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 +/// @status Done: https://prover.certora.com/output/39601/7849e9a464e042ea89bfe68fc226edbc?anonymousKey=5c1387afecb8bc86f23df3be5eb886a5cd82787f + +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 + ); +}