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,27 @@
+{
+    "files": [
+        "certora/harnesses/SafeHarness.sol",
+        "certora/mocks/ModuleGuardMock.sol", // a module guard 
+        "certora/mocks/TxnGuardMock.sol", // a (safe) guard
+    ],
+    "link": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/v1.5/Execute.spec", 
+
+    "assert_autofinder_success": true,
+    "optimistic_summary_recursion": true,
+    "optimistic_contract_recursion": true,
+
+    "summary_recursion_limit": "2",
+    "contract_recursion_limit": "2",
+    "loop_iter": "3",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "optimistic_fallback": true,
+
+    "rule_sanity": "basic",
+
+    "solc": "solc7.6",
+    "solc_via_ir": false,  
+}

certora/conf/v1.5/fallback.conf

@@ -0,0 +1,27 @@
+{
+    "files": [
+        "certora/harnesses/SafeHarness.sol",
+        "certora/harnesses/ExtensibleFallbackHandlerHarness.sol",
+        "certora/mocks/DummyHandler.sol"
+    ],
+    "link": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/v1.5/Fallback.spec",
+
+    "assert_autofinder_success": true,
+    "optimistic_summary_recursion": true,
+    "optimistic_contract_recursion": true,
+
+    "summary_recursion_limit": "2",
+    "contract_recursion_limit": "2",
+    "loop_iter": "3",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "optimistic_fallback": true,
+
+    "rule_sanity": "basic",
+
+    "solc": "solc7.6",
+    "solc_via_ir": false,
+}

certora/conf/v1.5/guards.conf

@@ -0,0 +1,33 @@
+// a conf file for safe module guards
+{
+    "files": [
+        "certora/harnesses/SafeHarness.sol",
+        "certora/mocks/ModuleGuardMock.sol", // a module guard 
+        "certora/mocks/TxnGuardMock.sol", // a (safe) guard
+    ],
+    "link": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/v1.5/Guards.spec", 
+
+    "assert_autofinder_success": true,
+    "optimistic_summary_recursion": true,
+    "optimistic_contract_recursion": true,
+
+    "summary_recursion_limit": "2",
+    "contract_recursion_limit": "2",
+    "loop_iter": "3",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "optimistic_fallback": true,
+
+    "rule_sanity": "basic",
+
+    "solc": "solc7.6",
+    "solc_via_ir": false,  
+
+    "prover_args": [
+        " -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on",
+        "-enableSolidityBasedInlining true"
+    ],
+}

certora/conf/v1.5/hash.conf

@@ -0,0 +1,25 @@
+{
+    "files": [
+        "certora/harnesses/SafeHarness.sol"
+    ],
+    "link": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/v1.5/Hash.spec",
+
+    "assert_autofinder_success": true,
+    "optimistic_summary_recursion": true,
+    "optimistic_contract_recursion": true,
+
+    "summary_recursion_limit": "2",
+    "contract_recursion_limit": "2",
+    "loop_iter": "3",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "optimistic_fallback": true,
+
+    "rule_sanity": "basic",
+
+    "solc": "solc7.6",
+    "solc_via_ir": false,  
+}

certora/conf/v1.5/setup.conf

@@ -0,0 +1,25 @@
+{
+    "files": [
+        "certora/harnesses/SafeHarness.sol"
+    ],
+    "link": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/v1.5/Setup.spec",
+
+    "assert_autofinder_success": true,
+    "optimistic_summary_recursion": true,
+    "optimistic_contract_recursion": true,
+
+    "summary_recursion_limit": "2",
+    "contract_recursion_limit": "2",
+    "loop_iter": "3",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "optimistic_fallback": true,
+
+    "rule_sanity": "basic",
+
+    "solc": "solc7.6",
+    "solc_via_ir": false,  
+}

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();
+    }
+
+}

certora/harnesses/SafeHarness.sol

@@ -1,5 +1,9 @@
 // SPDX-License-Identifier: LGPL-3.0-only
 import "../munged/Safe.sol";
+import {SafeMath} from "../munged/external/SafeMath.sol";
+import {ISafe, IStaticFallbackMethod, IFallbackMethod, ExtensibleBase} from "../munged/handler/extensible/ExtensibleBase.sol";
+import {IFallbackHandler, FallbackHandler} from "../munged/handler/extensible/FallbackHandler.sol";
+
 
 contract SafeHarness is Safe {
     constructor(
@@ -31,6 +35,10 @@ contract SafeHarness is Safe {
         }
     }
 
+    function numSigsSufficient(bytes memory signatures,uint256 requiredSignatures) public pure returns (bool) {
+        return (signatures.length >= SafeMath.mul(requiredSignatures,65));
+    }
+
     // harnessed getters
     function getModule(address module) public view returns (address) {
         return modules[module];
@@ -40,6 +48,10 @@ contract SafeHarness is Safe {
         return getGuard();
     }
 
+    function getModuleGuardExternal() public view returns (address) {
+        return getModuleGuard();
+    }
+
     function getNativeTokenBalance() public view returns (uint256) {
         return address(this).balance;
     }
@@ -56,6 +68,26 @@ contract SafeHarness is Safe {
         return getOwners().length;
     }
 
+    function approvedHashVal(address a, bytes32 hashInQuestion) public view returns (uint256) {
+        return approvedHashes[a][hashInQuestion];
+    }
+
+    function getFallbackHandler() public view returns (address) {
+        address handler;
+        assembly{
+            handler := sload(FALLBACK_HANDLER_STORAGE_SLOT)
+        }
+        return handler ;
+    }
+
+    function callSetSafeMethod(bytes4 selector, bytes32 newMethod) public {
+        IFallbackHandler(address(this)).setSafeMethod(selector,newMethod);
+    }
+
+    function callDummyHandler(bytes4 selector) public {
+        address(this).call(abi.encodeWithSelector(selector));
+    }
+
     function getTransactionHashPublic(
         address to,
         uint256 value,

certora/mocks/DummyHandler.sol

@@ -0,0 +1,24 @@
+// a dummy handler contract 
+import {ISafe, IStaticFallbackMethod, IFallbackMethod, ExtensibleBase} from "../munged/handler/extensible/ExtensibleBase.sol";
+
+contract DummyHandler is IFallbackMethod {
+    constructor(){
+        methodCalled = false ;
+    }
+
+    bool public methodCalled ;
+    function resetMethodCalled() public {
+        methodCalled = false; 
+    }
+
+    // the DUMMY method
+    function handle(ISafe safe, address sender, uint256 value, bytes calldata data) external override returns (bytes memory result) {
+        methodCalled = true ;
+
+        return "Hello, world!";
+    }
+
+    function dummyMethod() public {
+        methodCalled = true ;
+    }
+}

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