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..356f6fcab --- /dev/null +++ b/certora/conf/v1.5/execute.conf @@ -0,0 +1,36 @@ +{ + "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, + + "java_args": [ + " -ea -Dlevel.setup.helpers=info" + ], + "process": "emv", + "prover_args": [ + " -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on", + "-enableSolidityBasedInlining true" + ], +} \ 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..566876795 --- /dev/null +++ b/certora/conf/v1.5/guards.conf @@ -0,0 +1,37 @@ +// 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, + + "java_args": [ + " -ea -Dlevel.setup.helpers=info" + ], + "process": "emv", + "prover_args": [ + " -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on", + "-enableSolidityBasedInlining true" + ], +} \ No newline at end of file diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol index c3380ac73..60cc85b69 100644 --- a/certora/harnesses/SafeHarness.sol +++ b/certora/harnesses/SafeHarness.sol @@ -1,5 +1,6 @@ // SPDX-License-Identifier: LGPL-3.0-only import "../munged/Safe.sol"; +import {SafeMath} from "../munged/external/SafeMath.sol"; contract SafeHarness is Safe { constructor( @@ -31,6 +32,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 +45,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; } 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..552c2d0ce --- /dev/null +++ b/certora/specs/v1.5/Execute.spec @@ -0,0 +1,148 @@ +/* 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 ; + + return true ; +} + +// ---- 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; + + // execTxn from module passes + execTransactionFromModule(e,to,value,data,operation); + + // msg sender is the module + assert (isModuleEnabled(e,e.msg.sender)); +} + + +/// @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 == false); + + 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); + + assert (numSigsSufficient(signatures,threshold)); +} \ 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..a309e9752 --- /dev/null +++ b/certora/specs/v1.5/Guards.spec @@ -0,0 +1,191 @@ +/* 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() == true && + txnGuardMock.postCheckedTransactions() == true + ); +} + +/// @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() == true && + modGuardMock.postCheckedTransactions() == true + ); +} +