Formal Verification for Safe v1.5 Audit (#901)

This pull request corresponds to the formal verification aspect of the Safe v1.5 audit done by Certora. ## Summary of Changes ### Added Configuration and Specification files corresponding to new rules: * `execute.conf` and `Execute.spec` * `extensible.conf` and `Extensible.spec` * `fallback.conf` and `Fallback.spec` * `guards.conf` and `Guards.spec` * `hash.conf` and `Hash.spec` * `setup.conf` and `Setup.spec` Harness: * `ExtensibleFallbackHandlerHarness.sol` to reason about the fallback handler Mocks: * `DummyHandler.sol` for reasoning about the fallback handler * `TxnGuardMock.sol` and `TxnGuardMockDuplicate.sol` for reasoning about the transaction guard * `ModuleGuardMock.sol` and `ModuleGuardMockDuplicate.sol` for reasoning about the module guard ### Modified * `applyHarness.patch` - added some minor munging as explained in the audit report * `run.conf` - remove a deprecated configuration tag that was giving errors to the Prover * `Safe.spec` - moved a rule about guards to `Guard.spec` for logical continuity * `SafeHarness.sol` - added some view functionality to the Safe harness for some rules Co-authored-by: Derek Sorensen <[email protected]>
safe-global · Jan 16, 2025 · 8677f32 · 8677f32
1 parent 0372c8a
commit 8677f32
Show file tree

Hide file tree

Showing 22 changed files with 1,191 additions and 28 deletions.
diff --git 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-16 07:43:06
++++ Safe.sol	2025-01-13 11:58:17
 @@ -75,22 +75,24 @@
           * so we create a Safe with 0 owners and threshold 1.
           * This is an unusable Safe, perfect for the singleton
@@ -30,7 +30,7 @@ diff -druN Safe.sol Safe.sol
          // setupOwners checks if the Threshold is already set, therefore preventing this method from being called more than once
          setupOwners(_owners, _threshold);
          if (fallbackHandler != address(0)) internalSetFallbackHandler(fallbackHandler);
-@@ -386,9 +388,6 @@
+@@ -388,9 +390,6 @@
          return keccak256(abi.encode(DOMAIN_SEPARATOR_TYPEHASH, chainId, this));
      }
 
@@ -40,7 +40,7 @@ diff -druN Safe.sol Safe.sol
      function getTransactionHash(
          address to,
          uint256 value,
-@@ -400,7 +399,9 @@
+@@ -402,7 +401,9 @@
          address gasToken,
          address refundReceiver,
          uint256 _nonce
@@ -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
+@@ -452,7 +453,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-16 07:43:06
++++ base/Executor.sol	2025-01-13 11:58:17
 @@ -26,12 +26,8 @@
          uint256 txGas
      ) internal returns (bool success) {
@@ -69,10 +80,23 @@ diff -druN base/Executor.sol base/Executor.sol
          } else {
              /* solhint-disable no-inline-assembly */
              /// @solidity memory-safe-assembly
+diff -druN base/FallbackManager.sol base/FallbackManager.sol
+--- base/FallbackManager.sol	2024-12-16 07:43:06
++++ base/FallbackManager.sol	2025-01-13 12:07:42
+@@ -63,7 +63,8 @@
+             // not going beyond the scratch space, etc)
+             // Solidity docs: https://docs.soliditylang.org/en/latest/assembly.html#memory-safety
+
+-            let handler := sload(FALLBACK_HANDLER_STORAGE_SLOT)
++            // let handler := sload(FALLBACK_HANDLER_STORAGE_SLOT)
++            let handler := and(0xffffffffffffffffffffffffffffffffffffffff, sload(FALLBACK_HANDLER_STORAGE_SLOT))
+
+             if iszero(handler) {
+                 return(0, 0)
 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
-@@ -110,7 +110,7 @@
+--- interfaces/ISafe.sol	2024-12-16 07:43:06
++++ interfaces/ISafe.sol	2025-01-13 11:58:17
+@@ -113,7 +113,7 @@
       */
      function domainSeparator() external view returns (bytes32);
 
@@ -81,15 +105,15 @@ diff -druN interfaces/ISafe.sol interfaces/ISafe.sol
       * @notice Returns transaction hash to be signed by owners.
       * @param to Destination address.
       * @param value Ether value.
-@@ -123,7 +123,6 @@
+@@ -126,7 +126,6 @@
       * @param refundReceiver Address of receiver of gas payment (or 0 if tx.origin).
       * @param _nonce Transaction nonce.
       * @return Transaction hash.
 -     */
      function getTransactionHash(
          address to,
          uint256 value,
-@@ -136,6 +135,8 @@
+@@ -139,6 +138,8 @@
          address refundReceiver,
          uint256 _nonce
      ) external view returns (bytes32);

diff --git a/certora/conf/execute.conf b/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,  
+}
diff --git a/certora/conf/extensible.conf b/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,
+}
diff --git a/certora/conf/fallback.conf b/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,
+}
diff --git a/certora/conf/guards.conf b/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"
+    ],
+}
diff --git a/certora/conf/hash.conf b/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,  
+}
diff --git a/certora/conf/run.conf b/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"
 }
diff --git a/certora/conf/setup.conf b/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,  
+}
diff --git a/certora/harnesses/ExtensibleFallbackHandlerHarness.sol b/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];
+    }
+
+}
diff --git a/certora/harnesses/SafeHarness.sol b/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,

diff --git a/certora/mocks/DummyHandler.sol b/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 ;
+    }
+}