Feature: Mark assembly blocks as memory-safe (#545)

* add setup and rules about modules

* fix run script

* use solc7.6 for fv

* Mark assembly blocks as memory-safe

* use solidity 0.8.19 for github action benchmark

* Update makefile

* fix the harness patch

* properties doc skeleton

* properties notes

* use 10m optimizer runs

* Write calldata/return data to the memory allocated via the free memory pointer

* memory-safe simulateAndRevert

* Update CLA github action to v2.3.0

* add certora workflow

* Fix changelog mention of createChainSpecificProxyWithNonce

* fix script path

* use cvl2

* Remove gasleft in setupModules, add erc4337 compatibility test

* Fix typechecking in test files (#573)

* verify that guard can only be updated through setGuard

* Verify functions that may change the fallback handler address (#566)

* Add an invariant for singleton address (#565)

* Add an optimistic assumption about DELEGATECALL, update nonce monotonicity rule (#574)

* Pump version to 1.4.1 (#579)

* Formal verification: native token balance updates (#582)

* Add an optimistic assumption about DELEGATECALL, update nonce monotonicity rule

* Add a rule for token balance

* Add more rules for native token balance transition

* Fix addresses for 1.4.1 in changelog (#590)

* Fix certora CI action

* Formal verification: No message can be signed through the core contract (#583)

* Add a rule for no signed messages

* Add a rule for no signed messages

* fix munged patch

---------

Co-authored-by: teryanarmen <61996358+teryanarmen@users.noreply.github.com>
Co-authored-by: Uxio Fuentefria <Uxio0@users.noreply.github.com>
Co-authored-by: Francisco Giordano <fg@frang.io>
Co-authored-by: Richard Meissner <rmeissner@users.noreply.github.com>
Co-authored-by: Mikhail Mikheev <mmv@pop-os.localdomain>

Author: 6 people

.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
+     }
+ 
+     /**