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/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/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/extensible.conf

@@ -0,0 +1,27 @@
+{
+    "files": [
+        "certora/harnesses/SafeHarness.sol",
+        "certora/harnesses/ExtensibleFallbackHandlerHarness.sol",
+        "certora/mocks/DummyHandler.sol"
+    ],
+    "link": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/Extensible.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/fallback.conf

@@ -0,0 +1,27 @@
+{
+    "files": [
+        "certora/harnesses/SafeHarness.sol",
+        "certora/harnesses/ExtensibleFallbackHandlerHarness.sol",
+        "certora/mocks/DummyHandler.sol"
+    ],
+    "link": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/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/guards.conf

@@ -0,0 +1,35 @@
+// a conf file for safe module guards
+{
+    "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": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/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/hash.conf

@@ -0,0 +1,25 @@
+{
+    "files": [
+        "certora/harnesses/SafeHarness.sol"
+    ],
+    "link": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/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/run.conf

@@ -14,7 +14,6 @@
     ],
     "rule_sanity": "basic",
     "run_source": "MUTATION",
-    "send_only": true,
     "solc": "solc7.6",
     "verify": "SafeHarness:certora/specs/Safe.spec"
 }

certora/conf/setup.conf

@@ -0,0 +1,25 @@
+{
+    "files": [
+        "certora/harnesses/SafeHarness.sol"
+    ],
+    "link": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/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,11 @@
+// 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];
+    }
+
+}

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