Audit Draft PR for Code Review

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);

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"
+    ],
+}

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"
+    ],
+}

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"
+    ]
+}

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;
     }

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
+    }
+
+}

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
+    }
+
+}

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) }