Feature: Mark assembly blocks as memory-safe

.env.sample

@@ -4,3 +4,8 @@ INFURA_KEY=""
 # Used for custom network
 NODE_URL=""
 ETHERSCAN_API_KEY=""
+# (Optional) Used to run ERC-4337 compatibility test. MNEMONIC is also required.
+ERC4337_TEST_BUNDLER_URL=
+ERC4337_TEST_NODE_URL=
+ERC4337_TEST_SINGLETON_ADDRESS=
+ERC4337_TEST_SAFE_FACTORY_ADDRESS=

.github/workflows/certora.yml

@@ -26,7 +26,7 @@ jobs:
               with: { java-version: "17", java-package: jre, distribution: semeru }
 
             - name: Install certora cli-beta
-              run: pip install certora-cli-beta
+              run: pip install -Iv certora-cli-beta==4.2.0
 
             - name: Install solc
               run: |

CHANGELOG.md

@@ -2,6 +2,52 @@
 
 This changelog only contains changes starting from version 1.3.0
 
+# Version 1.4.1
+
+## Compiler settings
+
+Solidity compiler: [0.7.6](https://github.com/ethereum/solidity/releases/tag/v0.7.6) (for more info see issue [#251](https://github.com/safe-global/safe-contracts/issues/251))
+
+Solidity optimizer: `disabled`
+
+## Expected addresses with [Safe Singleton Factory](https://github.com/safe-global/safe-singleton-factory)
+
+### Core contracts
+
+-   `Safe` at `0x41675C099F32341bf84BFc5382aF534df5C7461a`
+-   `SafeL2` at `0x29fcB43b46531BcA003ddC8FCB67FFE91900C762`
+
+### Factory contracts
+
+-   `SafeProxyFactory` at `0x4e1DCf7AD4e460CfD30791CCC4F9c8a4f820ec67`
+
+### Handler contracts
+
+-   `TokenCallbackHandler` at `0xeDCF620325E82e3B9836eaaeFdc4283E99Dd7562`
+-   `CompatibilityFallbackHandler` at `0xfd0732Dc9E303f09fCEf3a7388Ad10A83459Ec99`
+
+### Lib contracts
+
+-   `MultiSend` at `0x38869bf66a61cF6bDB996A6aE40D5853Fd43B526`
+-   `MultiSendCallOnly` at `0x9641d764fc13c8B624c04430C7356C1C7C8102e2`
+-   `CreateCall` at `0x9b35Af71d77eaf8d7e40252370304687390A1A52`
+-   `SignMessageLib` at `0xd53cd0aB83D845Ac265BE939c57F53AD838012c9`
+
+### Storage reader contracts
+
+-   `SimulateTxAccessor` at `0x3d4BA2E0884aa488718476ca2FB8Efc291A46199`
+
+## Changes
+
+### Bugfixes
+
+#### Remove `gasleft()` usage in `setupModules`
+
+Issue: [#568](https://github.com/safe-global/safe-contracts/issues/568)
+
+`setupModules` made a call to `gasleft()` that is invalid in the ERC-4337 standard. The call was replaced with `type(uint256).max` to forward all the available gas instead.
+
+
 # Version 1.4.0
 
 ## Compiler settings

README.md

@@ -15,13 +15,29 @@ Usage
 yarn
 ```
 
-### Run all tests:
+### Testing
+
+To run the tests:
 
 ```bash
 yarn build
 yarn test
 ```
 
+Optionally, if you want to run the ERC-4337 compatibility test, it uses a live bundler and node, so it contains some pre-requisites:
+
+1. Define the environment variables:
+
+```
+ERC4337_TEST_BUNDLER_URL=
+ERC4337_TEST_NODE_URL=
+ERC4337_TEST_SINGLETON_ADDRESS=
+ERC4337_TEST_SAFE_FACTORY_ADDRESS=
+MNEMONIC=
+```
+
+2. Pre-fund the executor account derived from the mnemonic with some Native Token to cover the deployment of an ERC4337 module and the pre-fund of the Safe for the test operation.
+
 ### Deployments
 
 A collection of the different Safe contract deployments and their addresses can be found in the [Safe deployments](https://github.com/safe-global/safe-deployments) repository.
@@ -92,7 +108,7 @@ Documentation
 
 Audits/ Formal Verification
 ---------
-- [for Version 1.4.0 by Ackee Blockchain](docs/audit_1_4_0.md)
+- [for Version 1.4.0/1.4.1 by Ackee Blockchain](docs/audit_1_4_0.md)
 - [for Version 1.3.0 by G0 Group](docs/audit_1_3_0.md)
 - [for Version 1.2.0 by G0 Group](docs/audit_1_2_0.md)
 - [for Version 1.1.1 by G0 Group](docs/audit_1_1_1.md)

certora/applyHarness.patch

@@ -1,6 +1,6 @@
 diff -druN Safe.sol Safe.sol
---- Safe.sol	2023-04-11 15:01:13
-+++ Safe.sol	2023-04-11 15:01:55
+--- Safe.sol	2023-05-16 15:08:39
++++ Safe.sol	2023-05-25 16:23:56
 @@ -76,7 +76,7 @@
           * so we create a Safe with 0 owners and threshold 1.
           * This is an unusable Safe, perfect for the singleton
@@ -11,14 +11,19 @@ diff -druN Safe.sol Safe.sol
 
      /**
 diff -druN base/Executor.sol base/Executor.sol
---- base/Executor.sol	2023-04-11 15:01:13
-+++ base/Executor.sol	2023-04-11 15:01:18
-@@ -25,6 +25,8 @@
+--- base/Executor.sol	2023-05-16 15:08:39
++++ base/Executor.sol	2023-05-25 16:23:31
+@@ -25,11 +25,9 @@
          Enum.Operation operation,
          uint256 txGas
      ) internal returns (bool success) {
-+        // MUNGED lets just be a bit more optimistic, `execute` does nothing and always returns true
-+        return true;
++        // MUNGED lets just be a bit more optimistic, `execute` does nothing for `DELEGATECALL` and always returns true
          if (operation == Enum.Operation.DelegateCall) {
+-            // solhint-disable-next-line no-inline-assembly
+-            assembly {
+-                success := delegatecall(txGas, to, add(data, 0x20), mload(data), 0, 0)
+-            }
++            return true;
+         } else {
              // solhint-disable-next-line no-inline-assembly
              assembly {

certora/harnesses/SafeHarness.sol

@@ -19,4 +19,12 @@ contract SafeHarness is Safe {
     function getModule(address module) public view returns (address) {
         return modules[module];
     }
+
+    function getSafeGuard() public view returns (address) {
+        return getGuard();
+    }
+
+    function getNativeTokenBalance() public view returns (uint256) {
+        return address(this).balance;
+    }
 }

certora/scripts/verifySafe.sh

@@ -10,7 +10,7 @@ certoraRun  certora/harnesses/SafeHarness.sol \
     --verify SafeHarness:certora/specs/Safe.spec \
     --solc solc7.6 \
     --optimistic_loop \
-    --settings -optimisticFallback=true \
+    --prover_args "-optimisticFallback true" \
     --loop_iter 3 \
     --optimistic_hashing \
     --hashing_length_bound 352 \

certora/specs/Safe.spec

@@ -3,9 +3,12 @@ methods {
     function getThreshold() external returns (uint256) envfree;
     function disableModule(address,address) external;
     function nonce() external returns (uint256) envfree;
+    function signedMessages(bytes32) external returns (uint256) envfree;
 
     // harnessed
     function getModule(address) external returns (address) envfree;
+    function getSafeGuard() external returns (address) envfree;
+    function getNativeTokenBalance() external returns (uint256) envfree;
 
     // optional
     function execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation) external returns (bool, bytes memory);
@@ -20,20 +23,30 @@ definition noHavoc(method f) returns bool =
 
 definition reachableOnly(method f) returns bool =
     f.selector != sig:setup(address[],uint256,address,bytes,address,address,uint256,address).selector
-    && f.selector != sig:simulateAndRevert(address,bytes).selector;
+    && f.selector != sig:simulateAndRevert(address,bytes).selector
+    // getStorageAt cannot be used because we have a hook to sstore
+    // A quote from the Certora team:
+    // "If it’s called from an internal context it is fine but as a public function that can be called with any argument it cannot have hooks applied on."
+    && f.selector != sig:getStorageAt(uint256,uint256).selector;
+
+definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffff;
 
 /// Nonce must never decrease
 rule nonceMonotonicity(method f) filtered {
-    f -> noHavoc(f) && reachableOnly(f)
+    f -> reachableOnly(f)
 } {
     uint256 nonceBefore = nonce();
 
+    // The nonce may overflow, but since it's increased only by 1 with each transaction, it is not realistically possible to overflow it.
+    require nonceBefore < MAX_UINT256();
+
     calldataarg args; env e;
     f(e, args);
 
     uint256 nonceAfter = nonce();
 
-    assert nonceAfter == nonceBefore || to_mathint(nonceAfter) == nonceBefore + 1;
+    assert nonceAfter != nonceBefore => 
+        to_mathint(nonceAfter) == nonceBefore + 1 && f.selector == sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes).selector;
 }
 
 
@@ -81,4 +94,147 @@ invariant noDeadEnds(address dead, address lost)
             requireInvariant noDeadEnds(dead, module);
             requireInvariant noDeadEnds(module, dead);
         }
-    }
+    }
+
+
+// The singleton is a private variable, so we need to use a ghost variable to track it.
+ghost address ghostSingletonAddress {
+    init_state axiom ghostSingletonAddress == 0;
+}
+
+hook Sstore SafeHarness.(slot 0) address newSingletonAddress STORAGE {
+    ghostSingletonAddress = newSingletonAddress;
+}
+
+// This is EIP-1967's singleton storage slot:
+// 0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc
+// converted to decimal because certora doesn't seem to support hex yet.
+hook Sstore SafeHarness.(slot 24440054405305269366569402256811496959409073762505157381672968839269610695612) address newSingletonAddress STORAGE {
+    ghostSingletonAddress = newSingletonAddress;
+}
+
+invariant sigletonAddressNeverChanges()
+    ghostSingletonAddress == 0
+    filtered { f -> reachableOnly(f) && f.selector != sig:getStorageAt(uint256,uint256).selector }
+
+ghost address fallbackHandlerAddress {
+    init_state axiom fallbackHandlerAddress == 0;
+}
+
+// This is Safe's fallback handler storage slot:
+// 0x6c9a6c4a39284e37ed1cf53d337577d14212a4870fb976a4366c693b939918d5
+// converted to decimal because certora doesn't seem to support hex yet.
+hook Sstore SafeHarness.(slot 49122629484629529244014240937346711770925847994644146912111677022347558721749) address newFallbackHandlerAddress STORAGE {
+    fallbackHandlerAddress = newFallbackHandlerAddress;
+}
+
+rule fallbackHandlerAddressChange(method f) filtered {
+    f -> f.selector != sig:simulateAndRevert(address,bytes).selector &&
+         f.selector != sig:getStorageAt(uint256,uint256).selector
+} {
+    address fbHandlerBefore = fallbackHandlerAddress;
+
+    calldataarg args; env e;
+    f(e, args);
+
+    address fbHandlerAfter = fallbackHandlerAddress;
+
+    assert fbHandlerBefore != fbHandlerAfter =>
+        f.selector == sig:setup(address[],uint256,address,bytes,address,address,uint256,address).selector || f.selector == sig:setFallbackHandler(address).selector;
+}
+
+
+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) }
+
+rule nativeTokenBalanceSpending(method f) filtered {
+    f -> reachableOnly(f)
+} {
+    uint256 balanceBefore = getNativeTokenBalance();
+
+    calldataarg args; env e;
+    f(e, args);
+
+    uint256 balanceAfter = getNativeTokenBalance();
+
+    assert balanceAfter < balanceBefore => 
+        f.selector == sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes).selector
+        || f.selector == sig:execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation).selector
+        || f.selector == sig:execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation).selector;
+}
+
+rule nativeTokenBalanceSpendingExecTransaction(
+        address to,
+        uint256 value,
+        bytes data,
+        SafeHarness.Operation operation,
+        uint256 safeTxGas,
+        uint256 baseGas, 
+        uint256 gasPrice, 
+        address gasToken, 
+        address refundReceiver, 
+        bytes signatures
+    ) {
+    uint256 balanceBefore = getNativeTokenBalance();
+
+    env e;
+    execTransaction(e, to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, signatures);
+
+    uint256 balanceAfter = getNativeTokenBalance();
+
+    assert 
+        gasPrice == 0 => to_mathint(balanceBefore - value) <= to_mathint(balanceAfter)
+        // When the gas price is non-zero and the gas token is zero (zero = native token), the refund params should also be taken into account.
+        || gasPrice > 0 && gasToken == 0 => to_mathint(balanceBefore - value - (gasPrice * (baseGas + safeTxGas))) <= to_mathint(balanceAfter);
+}
+
+rule nativeTokenBalanceSpendingExecTransactionFromModule(
+        address to,
+        uint256 value,
+        bytes data,
+        SafeHarness.Operation operation
+    ) {
+    uint256 balanceBefore = getNativeTokenBalance();
+    env e;
+
+    execTransactionFromModule(e, to, value, data, operation);
+
+    uint256 balanceAfter = getNativeTokenBalance();
+
+    assert balanceAfter < balanceBefore => 
+        to_mathint(balanceBefore - value) <= to_mathint(balanceAfter);
+}
+
+
+rule nativeTokenBalanceSpendingExecTransactionFromModuleReturnData(
+        address to,
+        uint256 value,
+        bytes data,
+        SafeHarness.Operation operation
+) {
+    uint256 balanceBefore = getNativeTokenBalance();
+    env e;
+
+    execTransactionFromModuleReturnData(e, to, value, data, operation);
+
+    uint256 balanceAfter = getNativeTokenBalance();
+
+    assert balanceAfter < balanceBefore => 
+        to_mathint(balanceBefore - value) <= to_mathint(balanceAfter);
+}

contracts/Safe.sol

@@ -44,7 +44,7 @@ contract Safe is
 {
     using SafeMath for uint256;
 
-    string public constant VERSION = "1.4.0";
+    string public constant VERSION = "1.4.1";
 
     // keccak256(
     //     "EIP712Domain(uint256 chainId,address verifyingContract)"

contracts/base/ModuleManager.sol

@@ -35,7 +35,7 @@ abstract contract ModuleManager is SelfAuthorized, Executor {
         if (to != address(0)) {
             require(isContract(to), "GS002");
             // Setup has to complete successfully or transaction fails.
-            require(execute(to, 0, data, Enum.Operation.DelegateCall, gasleft()), "GS000");
+            require(execute(to, 0, data, Enum.Operation.DelegateCall, type(uint256).max), "GS000");
         }
     }