From 0644d7ab78ff18b32e09e27a299e84a667a8ff16 Mon Sep 17 00:00:00 2001 From: Derek Sorensen Date: Tue, 7 Jan 2025 08:47:14 -0500 Subject: [PATCH] enhances rules about module and transaction guards to include the proposition that the correct guard is called --- certora/conf/v1.5/guards.conf | 2 + certora/mocks/ModuleGuardMockDuplicate.sol | 71 ++++++++++++++++++++ certora/mocks/TxnGuardMockDuplicate.sol | 78 ++++++++++++++++++++++ certora/specs/v1.5/Guards.spec | 31 +++++++-- 4 files changed, 175 insertions(+), 7 deletions(-) create mode 100644 certora/mocks/ModuleGuardMockDuplicate.sol create mode 100644 certora/mocks/TxnGuardMockDuplicate.sol diff --git a/certora/conf/v1.5/guards.conf b/certora/conf/v1.5/guards.conf index 0c7f1484f..6701a24a5 100644 --- a/certora/conf/v1.5/guards.conf +++ b/certora/conf/v1.5/guards.conf @@ -3,7 +3,9 @@ "files": [ "certora/harnesses/SafeHarness.sol", "certora/mocks/ModuleGuardMock.sol", // a module guard + "certora/mocks/ModuleGuardMockDuplicate.sol", "certora/mocks/TxnGuardMock.sol", // a (safe) guard + "certora/mocks/TxnGuardMockDuplicate.sol", ], "link": [ diff --git a/certora/mocks/ModuleGuardMockDuplicate.sol b/certora/mocks/ModuleGuardMockDuplicate.sol new file mode 100644 index 000000000..0bb7e3420 --- /dev/null +++ b/certora/mocks/ModuleGuardMockDuplicate.sol @@ -0,0 +1,71 @@ +// SPDX-License-Identifier: LGPL-3.0-only +/* solhint-disable one-contract-per-file */ +pragma solidity >=0.7.0 <0.9.0; +import {IModuleGuard} from "../munged/base/ModuleManager.sol"; +import {IERC165} from "../munged/interfaces/IERC165.sol"; +import "../munged/libraries/Enum.sol"; + +contract ModuleGuardMockDuplicate is IModuleGuard { + + constructor(){ + preCheckedTransactions = false ; + postCheckedTransactions = false ; + } + + // some mock variables + bool public preCheckedTransactions ; + bool public postCheckedTransactions ; + + function resetChecks() external { + preCheckedTransactions = false ; + postCheckedTransactions = false ; + } + + /** + * @notice Checks the module transaction details. + * @dev The function needs to implement module transaction validation logic. + * @param to The address to which the transaction is intended. + * @param value The value of the transaction in Wei. + * @param data The transaction data. + * @param operation The type of operation of the module transaction. + * @param module The module involved in the transaction. + * @return moduleTxHash The hash of the module transaction. + */ + function checkModuleTransaction( + address to, + uint256 value, + bytes memory data, + Enum.Operation operation, + address module + ) external override returns (bytes32 moduleTxHash) { + // updates transaction checked + preCheckedTransactions = true ; + // if it passes, it returns a string of bytes + return bytes32(0); + } + + /** + * @notice Checks after execution of module transaction. + * @dev The function needs to implement a check after the execution of the module transaction. + * @param txHash The hash of the module transaction. + * @param success The status of the module transaction execution. + */ + function checkAfterModuleExecution(bytes32 txHash, bool success) external override { + postCheckedTransactions = true; + } + + /** + * @dev Returns true if this contract implements the interface defined by `interfaceId`. + * See the corresponding EIP section + * https://eips.ethereum.org/EIPS/eip-165#how-interfaces-are-identified + * to learn more about how these ids are created. + * + * This function call must use less than 30 000 gas. + */ + function supportsInterface(bytes4 interfaceId) external view virtual override returns (bool) { + return + interfaceId == type(IModuleGuard).interfaceId || // 0x58401ed8 + interfaceId == type(IERC165).interfaceId; // 0x01ffc9a7 + } + +} \ No newline at end of file diff --git a/certora/mocks/TxnGuardMockDuplicate.sol b/certora/mocks/TxnGuardMockDuplicate.sol new file mode 100644 index 000000000..8b7ad8a27 --- /dev/null +++ b/certora/mocks/TxnGuardMockDuplicate.sol @@ -0,0 +1,78 @@ +// SPDX-License-Identifier: LGPL-3.0-only +/* solhint-disable one-contract-per-file */ +pragma solidity >=0.7.0 <0.9.0; +import {ITransactionGuard} from "../munged/base/GuardManager.sol"; +import {IERC165} from "../munged/interfaces/IERC165.sol"; +import "../munged/libraries/Enum.sol"; + +contract TxnGuardMockDuplicate is ITransactionGuard { + + constructor(){} + + // some mock variables + bool public preCheckedTransactions ; + bool public postCheckedTransactions ; + + function resetChecks() external { + preCheckedTransactions = false ; + postCheckedTransactions = false ; + } + + /** + * @notice Checks the transaction details. + * @dev The function needs to implement transaction validation logic. + * @param to The address to which the transaction is intended. + * @param value The value of the transaction in Wei. + * @param data The transaction data. + * @param operation The type of operation of the transaction. + * @param safeTxGas Gas used for the transaction. + * @param baseGas The base gas for the transaction. + * @param gasPrice The price of gas in Wei for the transaction. + * @param gasToken The token used to pay for gas. + * @param refundReceiver The address which should receive the refund. + * @param signatures The signatures of the transaction. + * @param msgSender The address of the message sender. + */ + function checkTransaction( + address to, + uint256 value, + bytes memory data, + Enum.Operation operation, + uint256 safeTxGas, + uint256 baseGas, + uint256 gasPrice, + address gasToken, + address payable refundReceiver, + bytes memory signatures, + address msgSender + ) external override { + // updates transaction checked + preCheckedTransactions = true; + } + + /** + * @notice Checks after execution of the transaction. + * @dev The function needs to implement a check after the execution of the transaction. + * @param hash The hash of the transaction. + * @param success The status of the transaction execution. + */ + function checkAfterExecution(bytes32 hash, bool success) external override { + // updates transaction checked + postCheckedTransactions = true ; + } + + /** + * @dev Returns true if this contract implements the interface defined by `interfaceId`. + * See the corresponding EIP section + * https://eips.ethereum.org/EIPS/eip-165#how-interfaces-are-identified + * to learn more about how these ids are created. + * + * This function call must use less than 30 000 gas. + */ + function supportsInterface(bytes4 interfaceId) external view virtual override returns (bool) { + return + interfaceId == type(ITransactionGuard).interfaceId || // 0xe6d7a83a + interfaceId == type(IERC165).interfaceId; // 0x01ffc9a7 + } + +} \ No newline at end of file diff --git a/certora/specs/v1.5/Guards.spec b/certora/specs/v1.5/Guards.spec index d18243add..a39247fd6 100644 --- a/certora/specs/v1.5/Guards.spec +++ b/certora/specs/v1.5/Guards.spec @@ -1,7 +1,9 @@ /* A specification of the safe guard and module guard */ using ModuleGuardMock as modGuardMock; +using ModuleGuardMockDuplicate as modGuardMock2; using TxnGuardMock as txnGuardMock; +using TxnGuardMockDuplicate as txnGuardMock2; using SafeHarness as safe; // ---- Methods block ---------------------------------------------------------- @@ -140,7 +142,7 @@ rule setModuleGuardReentrant(address guard) { /// @dev the transaction guard gets called both pre- and post- any execTransaction -/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d +/// @status Done: https://prover.certora.com/output/39601/a9a8eaeba7994e10bf29dbe8813798b9?anonymousKey=fbddda2f78b44a7df3dff4707715b90b2d08ab63 rule txnGuardCalled( address to, uint256 value, @@ -157,19 +159,24 @@ rule txnGuardCalled( // the txn guard is the mock require (getSafeGuard() == txnGuardMock); - // execTxn passes + txnGuardMock.resetChecks(e); // reset the check triggers + txnGuardMock2.resetChecks(e); + execTransaction(e,to,value,data,operation,safeTxGas,baseGas, gasPrice,gasToken,refundReceiver,signatures); // the pre- and post- module transaction guards were called assert ( txnGuardMock.preCheckedTransactions() && - txnGuardMock.postCheckedTransactions() + txnGuardMock.postCheckedTransactions() && + // the right guard was called + !txnGuardMock2.preCheckedTransactions(e) && + !txnGuardMock2.postCheckedTransactions(e) ); } /// @dev the module guard gets called both pre- and post- any execTransactionFromModule -/// @status Done: https://prover.certora.com/output/39601/a05e24787c68404d877ae4acce693734?anonymousKey=02030d2ca97a19d0d7a70deb5a91dc4b75bca89d +/// @status Done: https://prover.certora.com/output/39601/7591e8c61e6d407b847e38bbe8238e13?anonymousKey=5d99429f5046e77825a4ed015af0a6a0d088538d rule moduleGuardCalled( address to, uint256 value, @@ -180,17 +187,22 @@ rule moduleGuardCalled( require (getModuleGuardExternal() == modGuardMock); modGuardMock.resetChecks(e); // reset the check triggers + modGuardMock2.resetChecks(e); + execTransactionFromModule(e,to,value,data,operation); // the pre- and post- module transaction guards were called assert ( modGuardMock.preCheckedTransactions() && - modGuardMock.postCheckedTransactions() + modGuardMock.postCheckedTransactions() && + // the correct guard was called + !modGuardMock2.preCheckedTransactions(e) && + !modGuardMock2.postCheckedTransactions(e) ); } /// @dev the module guard gets called both pre- and post- any execTransactionFromModuleReturnData -/// @status Done: https://prover.certora.com/output/39601/15cfd3430d794986a26d304c9e2fbc6e?anonymousKey=92f0976aba6cb3fe40cf6c728d34b140a438bbae +/// @status Done: https://prover.certora.com/output/39601/2de5a471d628464e8aaf4b9022e515de?anonymousKey=c4997fd77ba3808cf9bdc6a432f9b20eea551c95 rule moduleGuardCalledReturn( address to, uint256 value, @@ -201,12 +213,17 @@ rule moduleGuardCalledReturn( require (getModuleGuardExternal() == modGuardMock); modGuardMock.resetChecks(e); // reset the check triggers + modGuardMock2.resetChecks(e); + execTransactionFromModuleReturnData(e,to,value,data,operation); // the pre- and post- module transaction guards were called assert ( modGuardMock.preCheckedTransactions() && - modGuardMock.postCheckedTransactions() + modGuardMock.postCheckedTransactions() && + // the correct guard was called + !modGuardMock2.preCheckedTransactions(e) && + !modGuardMock2.postCheckedTransactions(e) ); }