From c73b5bc8afe6cc76543f51e4fff8aeea0fed8dbc Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 16 Dec 2024 13:44:19 +0000 Subject: [PATCH 01/19] apply a patch to the harness so the rule about hash collisions passes --- certora/applyHarness.patch | 25 ++++++++++++++++++------- 1 file changed, 18 insertions(+), 7 deletions(-) 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); From 7b7fab2bb7e8d61f7ea50346f5e9a435e2a75893 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 16 Dec 2024 13:51:29 +0000 Subject: [PATCH 02/19] a new specification for guards, including transaction guards and module guards; this commit ports a rule from Safe.spec so that rules on guards are in the same spec, adds some functionality to the Safe harness, and makes two mocks for the module and transaction guards. --- certora/conf/v1.5/guards.conf | 37 ++++++ certora/harnesses/SafeHarness.sol | 9 ++ certora/mocks/ModuleGuardMock.sol | 71 +++++++++++ certora/mocks/TxnGuardMock.sol | 78 ++++++++++++ certora/specs/Safe.spec | 15 --- certora/specs/v1.5/Guards.spec | 191 ++++++++++++++++++++++++++++++ 6 files changed, 386 insertions(+), 15 deletions(-) create mode 100644 certora/conf/v1.5/guards.conf create mode 100644 certora/mocks/ModuleGuardMock.sol create mode 100644 certora/mocks/TxnGuardMock.sol create mode 100644 certora/specs/v1.5/Guards.spec 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/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 + ); +} + From 4f7e6c6d348e1e1b14ca7a7074a3aba8895c441a Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 16 Dec 2024 13:52:20 +0000 Subject: [PATCH 03/19] a specification for execute, executionTxn, executeTxnFromModule, etc. and all its expected functionality --- certora/conf/v1.5/execute.conf | 36 ++++++++ certora/specs/v1.5/Execute.spec | 148 ++++++++++++++++++++++++++++++++ 2 files changed, 184 insertions(+) create mode 100644 certora/conf/v1.5/execute.conf create mode 100644 certora/specs/v1.5/Execute.spec 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/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 From 5730c067f2bd3a5b414fe95afb6e875c85127eaf Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 16 Dec 2024 14:02:15 +0000 Subject: [PATCH 04/19] fix execTxnModulePermissions so that it checks whether the caller was an enabled module before making the successful call, and adds documentation that refers to an added function to the Safe Harness --- certora/specs/v1.5/Execute.spec | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/certora/specs/v1.5/Execute.spec b/certora/specs/v1.5/Execute.spec index 552c2d0ce..1decac965 100644 --- a/certora/specs/v1.5/Execute.spec +++ b/certora/specs/v1.5/Execute.spec @@ -68,12 +68,13 @@ rule execTxnModulePermissions( 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 (isModuleEnabled(e,e.msg.sender)); + assert (module_enabled); } @@ -144,5 +145,6 @@ rule executeThresholdMet( 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 From 658bdaedb141b71b5aae065f333fbcc97fdc4622 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 16 Dec 2024 14:03:34 +0000 Subject: [PATCH 05/19] clean up two rule statements from bool == true to just bool --- certora/specs/v1.5/Guards.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/certora/specs/v1.5/Guards.spec b/certora/specs/v1.5/Guards.spec index a309e9752..62c0acd10 100644 --- a/certora/specs/v1.5/Guards.spec +++ b/certora/specs/v1.5/Guards.spec @@ -163,8 +163,8 @@ rule txnGuardCalled( // the pre- and post- module transaction guards were called assert ( - txnGuardMock.preCheckedTransactions() == true && - txnGuardMock.postCheckedTransactions() == true + txnGuardMock.preCheckedTransactions() && + txnGuardMock.postCheckedTransactions() ); } @@ -184,8 +184,8 @@ rule moduleGuardCalled( // the pre- and post- module transaction guards were called assert ( - modGuardMock.preCheckedTransactions() == true && - modGuardMock.postCheckedTransactions() == true + modGuardMock.preCheckedTransactions() && + modGuardMock.postCheckedTransactions() ); } From 654d3fefbc873115b13474d97db1644ca6c008a8 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 16 Dec 2024 14:23:37 +0000 Subject: [PATCH 06/19] duplicate new rules for execTransactionFromModule to identical rules but for execTransactionFromModuleReturnData --- certora/specs/v1.5/Execute.spec | 17 +++++++++++++++++ certora/specs/v1.5/Guards.spec | 21 +++++++++++++++++++++ 2 files changed, 38 insertions(+) diff --git a/certora/specs/v1.5/Execute.spec b/certora/specs/v1.5/Execute.spec index 1decac965..785207a35 100644 --- a/certora/specs/v1.5/Execute.spec +++ b/certora/specs/v1.5/Execute.spec @@ -77,6 +77,23 @@ rule execTxnModulePermissions( 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 diff --git a/certora/specs/v1.5/Guards.spec b/certora/specs/v1.5/Guards.spec index 62c0acd10..d18243add 100644 --- a/certora/specs/v1.5/Guards.spec +++ b/certora/specs/v1.5/Guards.spec @@ -189,3 +189,24 @@ rule moduleGuardCalled( ); } +/// @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() + ); +} + From f46fd96cd4fdfa35d75bf30f18f033edd2ec8e6d Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Mon, 16 Dec 2024 15:59:29 +0000 Subject: [PATCH 07/19] adding a spec file for rules about the setup, which contains two rules both of which are passing --- certora/conf/v1.5/setup.conf | 34 +++++++++++++++++++ certora/specs/v1.5/Setup.spec | 63 +++++++++++++++++++++++++++++++++++ 2 files changed, 97 insertions(+) create mode 100644 certora/conf/v1.5/setup.conf create mode 100644 certora/specs/v1.5/Setup.spec diff --git a/certora/conf/v1.5/setup.conf b/certora/conf/v1.5/setup.conf new file mode 100644 index 000000000..e9ed4b885 --- /dev/null +++ b/certora/conf/v1.5/setup.conf @@ -0,0 +1,34 @@ +{ + "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, + + "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/specs/v1.5/Setup.spec b/certora/specs/v1.5/Setup.spec new file mode 100644 index 000000000..ce0ca7f55 --- /dev/null +++ b/certora/specs/v1.5/Setup.spec @@ -0,0 +1,63 @@ +/* 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 +/// @status Done: https://prover.certora.com/output/39601/202435585f914643abd02fe37b8d1fc5?anonymousKey=e74abb4876b18456b372d84e44ad78e3a22a0566 + +rule setupThresholdZero( + 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); + + assert (old_threshold == 0); +} + +/// @dev setup sets threshold > 0 +/// @status Done: https://prover.certora.com/output/39601/202435585f914643abd02fe37b8d1fc5?anonymousKey=e74abb4876b18456b372d84e44ad78e3a22a0566 + +rule setupSetsPositiveThreshold( + address[] _owners, + uint256 _threshold, + address to, + bytes data, + address fallbackHandler, + address paymentToken, + uint256 payment, + address paymentReceiver) { + env e; + + // a successful call to setup + setup(e,_owners,_threshold,to,data,fallbackHandler, + paymentToken,payment,paymentReceiver); + + uint256 new_threshold = getThreshold(); + + assert (new_threshold > 0); +} \ No newline at end of file From f2ed3c9e3579367cb413ac75785b2c2cd9e895cc Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Tue, 17 Dec 2024 16:44:10 +0000 Subject: [PATCH 08/19] first draft of a fallback spec, with some TODOs including resolving sanity on the invariant fallbackHanlderNeverSelf, adding the static Dummy to the spec, and strengthening from satisfy to assert --- certora/conf/v1.5/fallback.conf | 37 +++++++++ .../ExtensibleFallbackHandlerHarness.sol | 15 ++++ certora/harnesses/SafeHarness.sol | 14 ++++ certora/mocks/DummyHandler.sol | 20 +++++ certora/specs/v1.5/Fallback.spec | 80 +++++++++++++++++++ 5 files changed, 166 insertions(+) create mode 100644 certora/conf/v1.5/fallback.conf create mode 100644 certora/harnesses/ExtensibleFallbackHandlerHarness.sol create mode 100644 certora/mocks/DummyHandler.sol create mode 100644 certora/specs/v1.5/Fallback.spec diff --git a/certora/conf/v1.5/fallback.conf b/certora/conf/v1.5/fallback.conf new file mode 100644 index 000000000..d6ef152e8 --- /dev/null +++ b/certora/conf/v1.5/fallback.conf @@ -0,0 +1,37 @@ +{ + "files": [ + "certora/harnesses/SafeHarness.sol", + "certora/harnesses/ExtensibleFallbackHandlerHarness.sol", + "certora/mocks/DummyHandler.sol", + "certora/mocks/DummyStaticHandler.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, + + "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/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 60cc85b69..d94159ff4 100644 --- a/certora/harnesses/SafeHarness.sol +++ b/certora/harnesses/SafeHarness.sol @@ -1,6 +1,7 @@ // 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"; contract SafeHarness is Safe { constructor( @@ -65,6 +66,19 @@ contract SafeHarness is Safe { return getOwners().length; } + function getFallbackHandler() public view returns (address) { + address handler; + assembly{ + handler := sload(FALLBACK_HANDLER_STORAGE_SLOT) + } + return handler ; + } + + // TODO deprecate this with CVL2 + function addressToBytes32(address addr) public pure returns (bytes32) { + return bytes32(uint256(uint160(addr))); + } + function getTransactionHashPublic( address to, uint256 value, diff --git a/certora/mocks/DummyHandler.sol b/certora/mocks/DummyHandler.sol new file mode 100644 index 000000000..35960d36d --- /dev/null +++ b/certora/mocks/DummyHandler.sol @@ -0,0 +1,20 @@ +// 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!"; // TODO + } +} \ 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..2c6a1555b --- /dev/null +++ b/certora/specs/v1.5/Fallback.spec @@ -0,0 +1,80 @@ +/* A specification for the exstensible fallback handler */ + +using ExtensibleFallbackHandlerHarness as fallbackHandler; +using DummyHandler as dummyHandler; +using DummyStaticHandler as dummyStaticHandler; +using SafeHarness as safe; + +// ---- Methods block ---------------------------------------------------------- +methods { + + function getFallbackHandler() external returns (address) envfree; + function addressToBytes32(address) external returns (bytes32) 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 +/// @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 (?)s: https://prover.certora.com/output/39601/103eb341ceef481c830e0ba04eb06766?anonymousKey=61cb4fd6726ab3d0fad887f6393865263eecf3f0 +invariant fallbackHanlderNeverSelf() + getFallbackHandler() != safe ; + + +/// @dev set safe method integrity: sets/modifies/removes handler +/// @status Done: https://prover.certora.com/output/39601/09912f9691e04917b4c0277e30ad8e38?anonymousKey=61db5fd06c13a287939455e3a531ff841442ee2e +rule setSafeMethodIntegrity(bytes4 selector, address newMethod_addr) { + env e; + + bytes32 newMethod = addressToBytes32(newMethod_addr); + + fallbackHandler.setSafeMethod(e,selector,newMethod); + bytes32 this_method = fallbackHandler.getSafeMethod(e,e.msg.sender,selector); + + assert (newMethod == this_method); +} + + +/// @dev a handler, once set via setSafeMethod, is possible to call +/// @status Done: https://prover.certora.com/output/39601/9fcde04ecd434963b9ce788f7ddea8c1?anonymousKey=a7efde58b28ef7c99264424b66984a8d39b78518 +rule hanlderCallableIfSet(bytes4 selector,method f) 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 = addressToBytes32(dummyHandler); // TODO to_bytes32 from CVL2 + // bytes4 selector = to_bytes4(00); // 0x00 indicates this is a non-static call + 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)); +} \ No newline at end of file From 8f011daf6fe6685ed30e59b19463bf0528cf352e Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 18 Dec 2024 09:20:27 +0000 Subject: [PATCH 09/19] remove unnecessary args in conf files --- certora/conf/v1.5/execute.conf | 9 --------- certora/conf/v1.5/fallback.conf | 11 +---------- certora/conf/v1.5/guards.conf | 11 +---------- certora/conf/v1.5/setup.conf | 9 --------- 4 files changed, 2 insertions(+), 38 deletions(-) diff --git a/certora/conf/v1.5/execute.conf b/certora/conf/v1.5/execute.conf index 356f6fcab..3972e17c0 100644 --- a/certora/conf/v1.5/execute.conf +++ b/certora/conf/v1.5/execute.conf @@ -24,13 +24,4 @@ "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/fallback.conf b/certora/conf/v1.5/fallback.conf index d6ef152e8..acb0b6047 100644 --- a/certora/conf/v1.5/fallback.conf +++ b/certora/conf/v1.5/fallback.conf @@ -24,14 +24,5 @@ "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" - ] + "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 index 566876795..0e67a93c5 100644 --- a/certora/conf/v1.5/guards.conf +++ b/certora/conf/v1.5/guards.conf @@ -24,14 +24,5 @@ "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" - ], + "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 index e9ed4b885..71a505028 100644 --- a/certora/conf/v1.5/setup.conf +++ b/certora/conf/v1.5/setup.conf @@ -22,13 +22,4 @@ "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 From a8561df91933075ab9a135bbaa9e33f9d00e10b7 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 18 Dec 2024 09:25:03 +0000 Subject: [PATCH 10/19] small style adjustment --- certora/specs/v1.5/Execute.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/v1.5/Execute.spec b/certora/specs/v1.5/Execute.spec index 785207a35..7934c62ed 100644 --- a/certora/specs/v1.5/Execute.spec +++ b/certora/specs/v1.5/Execute.spec @@ -102,7 +102,7 @@ rule executePermissions(method f) filtered { f.selector != sig:getStorageAt(uint256,uint256).selector } { env e; - require (execute_called == false); + require !execute_called; calldataarg args; f(e, args); From c97107a604b605fbac68ac68ee11727e0737dfe7 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 18 Dec 2024 09:44:16 +0000 Subject: [PATCH 11/19] combine the two setup rules into one more concise rules --- certora/specs/v1.5/Setup.spec | 34 ++++++++-------------------------- 1 file changed, 8 insertions(+), 26 deletions(-) diff --git a/certora/specs/v1.5/Setup.spec b/certora/specs/v1.5/Setup.spec index ce0ca7f55..67217d450 100644 --- a/certora/specs/v1.5/Setup.spec +++ b/certora/specs/v1.5/Setup.spec @@ -16,10 +16,10 @@ methods { // ---- Rules ------------------------------------------------------------------ -/// @dev setup can only be called if threshold = 0 -/// @status Done: https://prover.certora.com/output/39601/202435585f914643abd02fe37b8d1fc5?anonymousKey=e74abb4876b18456b372d84e44ad78e3a22a0566 +/// @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 setupThresholdZero( +rule setupThresholdZeroAndSetsPositiveThreshold( address[] _owners, uint256 _threshold, address to, @@ -36,28 +36,10 @@ rule setupThresholdZero( setup(e,_owners,_threshold,to,data,fallbackHandler, paymentToken,payment,paymentReceiver); - assert (old_threshold == 0); -} - -/// @dev setup sets threshold > 0 -/// @status Done: https://prover.certora.com/output/39601/202435585f914643abd02fe37b8d1fc5?anonymousKey=e74abb4876b18456b372d84e44ad78e3a22a0566 - -rule setupSetsPositiveThreshold( - address[] _owners, - uint256 _threshold, - address to, - bytes data, - address fallbackHandler, - address paymentToken, - uint256 payment, - address paymentReceiver) { - env e; - - // a successful call to setup - setup(e,_owners,_threshold,to,data,fallbackHandler, - paymentToken,payment,paymentReceiver); - uint256 new_threshold = getThreshold(); - assert (new_threshold > 0); -} \ No newline at end of file + assert ( + new_threshold > 0 && + old_threshold == 0 + ); +} From 019aef5ac83dd7c3f21a4becf5af8415021461cc Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 18 Dec 2024 09:59:04 +0000 Subject: [PATCH 12/19] reintroduce prover args to guards conf because moduleGuardCalledReturn and txnGuardCalled are vioalted otherwise --- certora/conf/v1.5/guards.conf | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/certora/conf/v1.5/guards.conf b/certora/conf/v1.5/guards.conf index 0e67a93c5..0c7f1484f 100644 --- a/certora/conf/v1.5/guards.conf +++ b/certora/conf/v1.5/guards.conf @@ -24,5 +24,10 @@ "rule_sanity": "basic", "solc": "solc7.6", - "solc_via_ir": false, + "solc_via_ir": false, + + "prover_args": [ + " -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on", + "-enableSolidityBasedInlining true" + ], } \ No newline at end of file From 206a82b73201f5831cd5929b674c8d9ce2b4d419 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Wed, 18 Dec 2024 14:43:32 +0000 Subject: [PATCH 13/19] extend some rules, deprecate/remove fixes used because I couldn't resolve some CVL issues, filter the invariant fallbackHanlderNeverSelf for sanity, etc. overall improvement of rules for fallback --- certora/harnesses/SafeHarness.sol | 5 --- certora/specs/v1.5/Fallback.spec | 64 ++++++++++++++++++++++++------- 2 files changed, 50 insertions(+), 19 deletions(-) diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol index d94159ff4..402ca86e2 100644 --- a/certora/harnesses/SafeHarness.sol +++ b/certora/harnesses/SafeHarness.sol @@ -74,11 +74,6 @@ contract SafeHarness is Safe { return handler ; } - // TODO deprecate this with CVL2 - function addressToBytes32(address addr) public pure returns (bytes32) { - return bytes32(uint256(uint160(addr))); - } - function getTransactionHashPublic( address to, uint256 value, diff --git a/certora/specs/v1.5/Fallback.spec b/certora/specs/v1.5/Fallback.spec index 2c6a1555b..5836a7a46 100644 --- a/certora/specs/v1.5/Fallback.spec +++ b/certora/specs/v1.5/Fallback.spec @@ -9,8 +9,7 @@ using SafeHarness as safe; methods { function getFallbackHandler() external returns (address) envfree; - function addressToBytes32(address) external returns (bytes32) envfree; - + function _.handle(address _safe, address sender, uint256 value, bytes data) external => DISPATCHER(true); } @@ -36,36 +35,73 @@ rule setFallbackIntegrity(address handler) { } /// @dev invariant: the address in fallback handler slot is never self -/// @status Done (?)s: https://prover.certora.com/output/39601/103eb341ceef481c830e0ba04eb06766?anonymousKey=61cb4fd6726ab3d0fad887f6393865263eecf3f0 -invariant fallbackHanlderNeverSelf() - getFallbackHandler() != safe ; +/// @status Done: https://prover.certora.com/output/39601/edb75f86f23445cdbc7cd7b5c4c420b6?anonymousKey=62191f4f70404bcbce784f5172e3ed7ab323d416 +invariant fallbackHanlderNeverSelf() + getFallbackHandler() != safe + filtered { + f -> f.selector != sig:simulateAndRevert(address,bytes).selector + } + +// for soundness of fallbackHanlderNeverSelf, we prove a rule that simulateAndRevert always reverts +rule simulateAndRevertReverts(address caddr, bytes b) { + env e; + simulateAndRevert@withrevert(e,caddr,b); + assert lastReverted; +} + +/// @dev 3 rules for set safe method integrity: sets/modifies/removes 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); + bytes32 thisMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector); + + assert (thisMethod == thisMethod); +} -/// @dev set safe method integrity: sets/modifies/removes handler -/// @status Done: https://prover.certora.com/output/39601/09912f9691e04917b4c0277e30ad8e38?anonymousKey=61db5fd06c13a287939455e3a531ff841442ee2e -rule setSafeMethodIntegrity(bytes4 selector, address newMethod_addr) { +/// @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 = addressToBytes32(newMethod_addr); + bytes32 newMethod = to_bytes32(0); // call setSafeMethod with the zero address fallbackHandler.setSafeMethod(e,selector,newMethod); - bytes32 this_method = fallbackHandler.getSafeMethod(e,e.msg.sender,selector); + bytes32 thisMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector); + + assert (thisMethod == to_bytes32(0)); // there is nothing stored +} + +/// @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); + + bytes32 thisMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector); - assert (newMethod == this_method); + 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(bytes4 selector,method f) filtered { f -> f.isFallback } { +rule hanlderCallableIfSet(method f) 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 = addressToBytes32(dummyHandler); // TODO to_bytes32 from CVL2 - // bytes4 selector = to_bytes4(00); // 0x00 indicates this is a non-static call + bytes32 dummy_bytes = to_bytes32(assert_uint256(dummyHandler)); + bytes4 selector = to_bytes4(00); // 0x00 indicates this is a non-static call 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 From e15d1a29dfcb6b34b0d11366e1ce68df63e2616f Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Thu, 19 Dec 2024 12:28:49 +0000 Subject: [PATCH 14/19] add rules on hashing --- certora/conf/v1.5/safe.conf | 25 ++++++++++++++++ certora/harnesses/SafeHarness.sol | 14 +++++++++ certora/specs/v1.5/Safe.spec | 47 +++++++++++++++++++++++++++++++ 3 files changed, 86 insertions(+) create mode 100644 certora/conf/v1.5/safe.conf create mode 100644 certora/specs/v1.5/Safe.spec diff --git a/certora/conf/v1.5/safe.conf b/certora/conf/v1.5/safe.conf new file mode 100644 index 000000000..4e4565d17 --- /dev/null +++ b/certora/conf/v1.5/safe.conf @@ -0,0 +1,25 @@ +{ + "files": [ + "certora/harnesses/SafeHarness.sol" + ], + "link": [ + + ], + "verify": "SafeHarness:certora/specs/v1.5/Safe.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/SafeHarness.sol b/certora/harnesses/SafeHarness.sol index 402ca86e2..f2d100e27 100644 --- a/certora/harnesses/SafeHarness.sol +++ b/certora/harnesses/SafeHarness.sol @@ -2,6 +2,8 @@ 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( @@ -66,6 +68,10 @@ 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{ @@ -74,6 +80,14 @@ contract SafeHarness is Safe { 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/specs/v1.5/Safe.spec b/certora/specs/v1.5/Safe.spec new file mode 100644 index 000000000..0e9b986dc --- /dev/null +++ b/certora/specs/v1.5/Safe.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 From 43f4cb11414cb2ba6cc7e324a80bf1199f9caa17 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Thu, 19 Dec 2024 12:29:43 +0000 Subject: [PATCH 15/19] change Safe spec to Hash spec for more accurate naming --- certora/conf/v1.5/{safe.conf => hash.conf} | 2 +- certora/specs/v1.5/Hash.spec | 45 +++++++++++++++++++++ certora/specs/v1.5/Safe.spec | 47 ---------------------- 3 files changed, 46 insertions(+), 48 deletions(-) rename certora/conf/v1.5/{safe.conf => hash.conf} (89%) create mode 100644 certora/specs/v1.5/Hash.spec delete mode 100644 certora/specs/v1.5/Safe.spec diff --git a/certora/conf/v1.5/safe.conf b/certora/conf/v1.5/hash.conf similarity index 89% rename from certora/conf/v1.5/safe.conf rename to certora/conf/v1.5/hash.conf index 4e4565d17..9e82324e9 100644 --- a/certora/conf/v1.5/safe.conf +++ b/certora/conf/v1.5/hash.conf @@ -5,7 +5,7 @@ "link": [ ], - "verify": "SafeHarness:certora/specs/v1.5/Safe.spec", + "verify": "SafeHarness:certora/specs/v1.5/Hash.spec", "assert_autofinder_success": true, "optimistic_summary_recursion": true, diff --git a/certora/specs/v1.5/Hash.spec b/certora/specs/v1.5/Hash.spec new file mode 100644 index 000000000..67217d450 --- /dev/null +++ b/certora/specs/v1.5/Hash.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 + ); +} diff --git a/certora/specs/v1.5/Safe.spec b/certora/specs/v1.5/Safe.spec deleted file mode 100644 index 0e9b986dc..000000000 --- a/certora/specs/v1.5/Safe.spec +++ /dev/null @@ -1,47 +0,0 @@ -/* 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 From 9743c131d92a2419e54e6d4cbe742c628f7b7e78 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Thu, 19 Dec 2024 14:23:00 +0000 Subject: [PATCH 16/19] committing the hash spec, there was some confusion with renaming this from before --- certora/specs/v1.5/Hash.spec | 42 +++++++++++++++++++----------------- 1 file changed, 22 insertions(+), 20 deletions(-) diff --git a/certora/specs/v1.5/Hash.spec b/certora/specs/v1.5/Hash.spec index 67217d450..0e9b986dc 100644 --- a/certora/specs/v1.5/Hash.spec +++ b/certora/specs/v1.5/Hash.spec @@ -16,30 +16,32 @@ methods { // ---- 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) { +/// @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 old_threshold = getThreshold(); + uint256 hashBefore = approvedHashVal(e,user,userHash); - // a successful call to setup - setup(e,_owners,_threshold,to,data,fallbackHandler, - paymentToken,payment,paymentReceiver); + calldataarg args; + f(e,args); - uint256 new_threshold = getThreshold(); + uint256 hashAfter = approvedHashVal(e,user,userHash); - assert ( - new_threshold > 0 && - old_threshold == 0 + 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 From 00349d69e54ede28cb23fe52f160c2c513557332 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Thu, 19 Dec 2024 14:28:42 +0000 Subject: [PATCH 17/19] update fallback to most current version. all but one passes (annotated) and it's our problem. will update if we can resolve it --- certora/conf/v1.5/fallback.conf | 3 +- certora/mocks/DummyHandler.sol | 6 +++- certora/specs/v1.5/Fallback.spec | 52 ++++++++++++++++++++++++++------ 3 files changed, 49 insertions(+), 12 deletions(-) diff --git a/certora/conf/v1.5/fallback.conf b/certora/conf/v1.5/fallback.conf index acb0b6047..4e7621973 100644 --- a/certora/conf/v1.5/fallback.conf +++ b/certora/conf/v1.5/fallback.conf @@ -2,8 +2,7 @@ "files": [ "certora/harnesses/SafeHarness.sol", "certora/harnesses/ExtensibleFallbackHandlerHarness.sol", - "certora/mocks/DummyHandler.sol", - "certora/mocks/DummyStaticHandler.sol" + "certora/mocks/DummyHandler.sol" ], "link": [ diff --git a/certora/mocks/DummyHandler.sol b/certora/mocks/DummyHandler.sol index 35960d36d..6a121cb94 100644 --- a/certora/mocks/DummyHandler.sol +++ b/certora/mocks/DummyHandler.sol @@ -15,6 +15,10 @@ contract DummyHandler is IFallbackMethod { function handle(ISafe safe, address sender, uint256 value, bytes calldata data) external override returns (bytes memory result) { methodCalled = true ; - return "Hello, world!"; // TODO + return "Hello, world!"; + } + + function dummyMethod() public { + methodCalled = true ; } } \ No newline at end of file diff --git a/certora/specs/v1.5/Fallback.spec b/certora/specs/v1.5/Fallback.spec index 5836a7a46..0dc7f4863 100644 --- a/certora/specs/v1.5/Fallback.spec +++ b/certora/specs/v1.5/Fallback.spec @@ -2,15 +2,22 @@ using ExtensibleFallbackHandlerHarness as fallbackHandler; using DummyHandler as dummyHandler; -using DummyStaticHandler as dummyStaticHandler; 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 SafeHarness._() => DISPATCH(use_fallback=true) [ + fallbackHandler._ + ] default NONDET; + + unresolved external in callDummyHandler(bytes4) => DISPATCH(use_fallback=true) [ + safe._ + ] default NONDET; + } // ---- Functions and ghosts --------------------------------------------------- @@ -42,26 +49,29 @@ invariant fallbackHanlderNeverSelf() f -> f.selector != sig:simulateAndRevert(address,bytes).selector } -// for soundness of fallbackHanlderNeverSelf, we prove a rule that simulateAndRevert always reverts +/// @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 3 rules for set safe method integrity: sets/modifies/removes handler +/// @dev setSafeMethod sets the handler /// @status Done: https://prover.certora.com/output/39601/bab9860cdfc44a83bed82e79d8c06218?anonymousKey=b4c5dbef050bb201ad78b3dd5af5cdca8ffa9f92 rule setSafeMethodSets(bytes4 selector, address newMethodCaddr) { - env e; + 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 == thisMethod); + 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) { @@ -70,11 +80,13 @@ rule setSafeMethodRemoves(bytes4 selector) { 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; @@ -84,7 +96,8 @@ rule setSafeMethodChanges(bytes4 selector, address newMethodCaddr) { 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); @@ -93,7 +106,7 @@ rule setSafeMethodChanges(bytes4 selector, address newMethodCaddr) { /// @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) filtered { f -> f.isFallback } { +rule hanlderCallableIfSet(method f, bytes4 selector) filtered { f -> f.isFallback } { env e; // the fallback handler is in the scene @@ -101,7 +114,6 @@ rule hanlderCallableIfSet(method f) filtered { f -> f.isFallback } { // the dummy (sub) handler is a valid handler for this safe bytes32 dummy_bytes = to_bytes32(assert_uint256(dummyHandler)); - bytes4 selector = to_bytes4(00); // 0x00 indicates this is a non-static call 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 @@ -113,4 +125,26 @@ rule hanlderCallableIfSet(method f) filtered { f -> f.isFallback } { // 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 dispatching issues (problem with the Prover) +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 From f2f39c539c69f444d157aa0153a29072235d1b43 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Thu, 19 Dec 2024 15:44:17 +0000 Subject: [PATCH 18/19] execute_summary() improvement so it's more general --- certora/specs/v1.5/Execute.spec | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/specs/v1.5/Execute.spec b/certora/specs/v1.5/Execute.spec index 7934c62ed..38b2f91ac 100644 --- a/certora/specs/v1.5/Execute.spec +++ b/certora/specs/v1.5/Execute.spec @@ -50,9 +50,9 @@ methods { persistent ghost bool execute_called { init_state axiom execute_called == false; } function execute_summary() returns bool { - execute_called = true ; - - return true ; + execute_called = true ; + bool new_var ; + return new_var ; } // ---- Invariants ------------------------------------------------------------- From d8b3e024a5d6a4d330a893cdb3266b8bde7f9138 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Fri, 20 Dec 2024 14:12:23 +0000 Subject: [PATCH 19/19] debugging handlerCalledIfSet rule, included an invariant that handler is never self nor the zero address, and now the Prover is misbehaving. Committing here and opening a ticket --- certora/specs/v1.5/Fallback.spec | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/certora/specs/v1.5/Fallback.spec b/certora/specs/v1.5/Fallback.spec index 0dc7f4863..c1ece76bc 100644 --- a/certora/specs/v1.5/Fallback.spec +++ b/certora/specs/v1.5/Fallback.spec @@ -10,7 +10,7 @@ methods { function getFallbackHandler() external returns (address) envfree; function _.handle(address _safe, address sender, uint256 value, bytes data) external => DISPATCHER(true); - unresolved external in SafeHarness._() => DISPATCH(use_fallback=true) [ + unresolved external in safe._ => DISPATCH(use_fallback=true) [ fallbackHandler._ ] default NONDET; @@ -49,6 +49,13 @@ invariant fallbackHanlderNeverSelf() 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) { @@ -128,10 +135,13 @@ rule hanlderCallableIfSet(method f, bytes4 selector) filtered { f -> f.isFallbac } /// @dev a handler is called under expected conditions -/// @status violated due to dispatching issues (problem with the Prover) +/// @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);