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

@@ -0,0 +1,53 @@
+name: certora
+
+on:
+    push:
+        branches:
+            - main
+    pull_request:
+        branches:
+            - main
+
+    workflow_dispatch:
+
+jobs:
+    verify:
+        runs-on: ubuntu-latest
+
+        steps:
+            - uses: actions/checkout@v3
+
+            - name: Install python
+              uses: actions/setup-python@v4
+              with: { python-version: 3.11 }
+
+            - name: Install java
+              uses: actions/setup-java@v3
+              with: { java-version: "17", java-package: jre, distribution: semeru }
+
+            - name: Install certora cli
+              run: pip install -Iv certora-cli
+
+            - name: Install solc
+              run: |
+                  wget https://github.com/ethereum/solidity/releases/download/v0.7.6/solc-static-linux
+                  chmod +x solc-static-linux
+                  sudo mv solc-static-linux /usr/local/bin/solc7.6
+
+            - name: Verify rule ${{ matrix.rule }}
+              run: |
+                  cd certora
+                  touch applyHarness.patch
+                  make munged
+                  cd ..
+                  echo "key length" ${#CERTORAKEY}
+                  ./certora/scripts/${{ matrix.rule }}
+              env:
+                  CERTORAKEY: ${{ secrets.CERTORA_KEY }}
+
+        strategy:
+            fail-fast: false
+            max-parallel: 16
+            matrix:
+                rule:
+                    - verifySafe.sh

.github/workflows/ci.yml

@@ -62,10 +62,10 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        solidity: ["0.7.6", "0.8.2"]
+        solidity: ["0.7.6", "0.8.19"]
         include:
-        - solidity: "0.8.2"
-          settings: '{"viaIR":true,"optimizer":{"enabled":true,"runs":10000}}'
+        - solidity: "0.8.19"
+          settings: '{"viaIR":true,"optimizer":{"enabled":true,"runs":1000000}}'
     env:
       SOLIDITY_VERSION: ${{ matrix.solidity }}
       SOLIDITY_SETTINGS: ${{ matrix.settings }}

.github/workflows/cla.yml

@@ -12,7 +12,7 @@ jobs:
       - name: "CLA Assistant"
         if: (github.event.comment.body == 'recheck' || github.event.comment.body == 'I have read the CLA Document and I hereby sign the CLA') || github.event_name == 'pull_request_target'
         # Beta Release
-        uses: cla-assistant/github-action@v2.1.3-beta
+        uses: cla-assistant/github-action@v2.3.0
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
           # the below token should have repo scope and must be manually added by you in the repository's secret
@@ -33,4 +33,4 @@ jobs:
           #custom-pr-sign-comment: 'The signature to be committed in order to sign the CLA'
           #custom-allsigned-prcomment: 'pull request comment when all contributors has signed, defaults to **CLA Assistant Lite bot** All Contributors have signed the CLA.'
           #lock-pullrequest-aftermerge: false - if you don't want this bot to automatically lock the pull request after merging (default - true)
-          #use-dco-flag: true - If you are using DCO instead of CLA
+          #use-dco-flag: true - If you are using DCO instead of CLA

.gitignore

@@ -11,4 +11,9 @@ bin/
 solc
 coverage/
 coverage.json
-yarn-error.log
+yarn-error.log
+
+# Certora Formal Verification related files
+.certora_internal
+.certora_recent_jobs.json
+.zip-output-url.txt

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
@@ -107,7 +153,7 @@ This method uses the `CREATE` opcode, which is not counterfactual for a specific
 
 If the initializer data is provided, the Factory now checks that the Singleton contract exists and the success of the call to avoid a proxy being deployed uninitialized
 
-#### Add `createNetworkSpecificProxy`
+#### Add `createChainSpecificProxyWithNonce`
 
 This method will use the chain id in the `CREATE2` salt; therefore, deploying a proxy to the same address on other networks is impossible.
 This method should enable the creation of proxies that should exist only on one network (e.g. specific governance or admin accounts)

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/.gitignore

@@ -0,0 +1 @@
+munged

certora/Makefile

@@ -0,0 +1,25 @@
+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../contracts
+MUNGED_DIR    = munged
+
+help:
+	@echo "usage:"
+	@echo "  make clean:  remove all generated files (those ignored by git)"
+	@echo "  make munged: create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
+	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
+
+munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
+	rm -rf $@
+	cp -r $(CONTRACTS_DIR) $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	diff -druN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH)
+
+refresh: munged record
+
+clean:
+	git clean -fdX
+	touch $(PATCH)

certora/applyHarness.patch

@@ -0,0 +1,32 @@
+diff -druN base/Executor.sol base/Executor.sol
+--- base/Executor.sol	2023-06-22 14:42:39.769357540 +0200
++++ base/Executor.sol	2023-06-22 15:34:09.211725615 +0200
+@@ -26,11 +26,13 @@
+         uint256 txGas
+     ) internal returns (bool success) {
+         if (operation == Enum.Operation.DelegateCall) {
++            // MUNGED lets just be a bit more optimistic, `execute` does nothing for `DELEGATECALL` and always returns true
+             // solhint-disable-next-line no-inline-assembly
+             /// @solidity memory-safe-assembly
+-            assembly {
+-                success := delegatecall(txGas, to, add(data, 0x20), mload(data), 0, 0)
+-            }
++            // assembly {
++            //     success := delegatecall(txGas, to, add(data, 0x20), mload(data), 0, 0)
++            // }
++            return true;
+         } else {
+             // solhint-disable-next-line no-inline-assembly
+             /// @solidity memory-safe-assembly
+diff -druN Safe.sol Safe.sol
+--- Safe.sol	2023-06-22 14:43:53.738861263 +0200
++++ Safe.sol	2023-06-22 15:28:00.436277677 +0200
+@@ -76,7 +76,7 @@
+          * so we create a Safe with 0 owners and threshold 1.
+          * This is an unusable Safe, perfect for the singleton
+          */
+-        threshold = 1;
++        // threshold = 1; MUNGED: remove and add to constructor of the harness
+     }
+
+     /**

certora/harnesses/SafeHarness.sol

@@ -0,0 +1,30 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+import "../munged/Safe.sol";
+
+contract SafeHarness is Safe {
+    constructor(
+        address[] memory _owners,
+        uint256 _threshold,
+        address to,
+        bytes memory data,
+        address fallbackHandler,
+        address paymentToken,
+        uint256 payment,
+        address payable paymentReceiver
+    ) {
+        this.setup(_owners, _threshold, to, data, fallbackHandler, paymentToken, payment, paymentReceiver);
+    }
+
+    // harnessed getters
+    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

@@ -0,0 +1,19 @@
+#!/bin/bash
+
+params=("--send_only")
+
+if [[ -n "$CI" ]]; then
+    params=()
+fi
+
+certoraRun  certora/harnesses/SafeHarness.sol \
+    --verify SafeHarness:certora/specs/Safe.spec \
+    --solc solc7.6 \
+    --optimistic_loop \
+    --settings -optimisticFallback=true \
+    --loop_iter 3 \
+    --optimistic_hashing \
+    --hashing_length_bound 352 \
+    --rule_sanity \
+    "${params[@]}" \
+    --msg "Safe $1 "