Feature: Mark assembly blocks as memory-safe

.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-beta
+              run: pip install certora-cli-beta
+
+            - 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/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

@@ -107,7 +107,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)

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,24 @@
+diff -druN Safe.sol Safe.sol
+--- Safe.sol	2023-04-11 15:01:13
++++ Safe.sol	2023-04-11 15:01:55
+@@ -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
+     }
+
+     /**
+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 @@
+         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;
+         if (operation == Enum.Operation.DelegateCall) {
+             // solhint-disable-next-line no-inline-assembly
+             assembly {

certora/harnesses/SafeHarness.sol

@@ -0,0 +1,22 @@
+// 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];
+    }
+}

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 "

certora/specs/Safe.spec

@@ -0,0 +1,84 @@
+methods {
+    // 
+    function getThreshold() external returns (uint256) envfree;
+    function disableModule(address,address) external;
+    function nonce() external returns (uint256) envfree;
+
+    // harnessed
+    function getModule(address) external returns (address) envfree;
+
+    // optional
+    function execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation) external returns (bool, bytes memory);
+    function execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation) external returns (bool);
+    function execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes) external returns (bool);
+}
+
+definition noHavoc(method f) returns bool =
+    f.selector != sig:execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation).selector
+    && f.selector != sig:execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation).selector 
+    && f.selector != sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes).selector;
+
+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;
+
+/// Nonce must never decrease
+rule nonceMonotonicity(method f) filtered {
+    f -> noHavoc(f) && reachableOnly(f)
+} {
+    uint256 nonceBefore = nonce();
+
+    calldataarg args; env e;
+    f(e, args);
+
+    uint256 nonceAfter = nonce();
+
+    assert nonceAfter == nonceBefore || to_mathint(nonceAfter) == nonceBefore + 1;
+}
+
+
+/// The sentinel must never point to the zero address.
+/// @notice It should either point to itself or some nonzero value
+invariant liveSentinel()
+    getModule(1) != 0
+    filtered { f -> noHavoc(f) && reachableOnly(f) }
+    { preserved {
+        requireInvariant noDeadEnds(getModule(1), 1);
+    }}
+
+/// Threshold must always be nonzero.
+invariant nonzeroThreshold()
+    getThreshold() > 0
+    filtered { f -> noHavoc(f) && reachableOnly(f) }
+
+/// Two different modules must not point to the same module/
+invariant uniquePrevs(address prev1, address prev2)
+    prev1 != prev2 && getModule(prev1) != 0 => getModule(prev1) != getModule(prev2)
+    filtered { f -> noHavoc(f) && reachableOnly(f) }
+    { 
+        preserved {
+            requireInvariant noDeadEnds(getModule(prev1), prev1);
+            requireInvariant noDeadEnds(getModule(prev2), prev2);
+            requireInvariant uniquePrevs(prev1, 1);
+            requireInvariant uniquePrevs(prev2, 1);
+            requireInvariant uniquePrevs(prev1, getModule(prev2));
+            requireInvariant uniquePrevs(prev2, getModule(prev1));
+        }
+    }
+
+/// A module that points to the zero address must not have another module pointing to it.
+invariant noDeadEnds(address dead, address lost)
+    dead != 0 && getModule(dead) == 0 => getModule(lost) != dead
+    filtered { f -> noHavoc(f) && reachableOnly(f) }
+    {
+        preserved {
+            requireInvariant liveSentinel();
+            requireInvariant noDeadEnds(getModule(1), 1);
+        }
+        preserved disableModule(address prevModule, address module) with (env e) {
+            requireInvariant uniquePrevs(prevModule, lost);
+            requireInvariant uniquePrevs(prevModule, dead);
+            requireInvariant noDeadEnds(dead, module);
+            requireInvariant noDeadEnds(module, dead);
+        }
+    }

certora/specs/properties.md

@@ -0,0 +1,63 @@
+# Safe Contract implementation properties
+
+## Reminder on property categories
+
+The categories are based on Certora's workshop [notes](https://github.com/Certora/Tutorials/blob/40ad7970bfafd081f6f416fe36b31981e48c6857/3DayWorkshop/SymbolicPool/properties.md).
+
+1. Valid states
+   Usually, there can be only one valid state at any given time. Such properties ensure the system is always in exactly one of its valid states.
+
+2. State transitions
+   Such properties verify the correctness of transactions between valid states. E.g., confirm valid states change according to their correct order or transitions only occur under the right conditions.
+
+3. Variable transitions
+   Similar to state transitions, but for variables. E.g., verify that Safe nonce is monotonically increasing.
+
+4. High-level properties
+   The most powerful type of properties covering the entire system. E.g., for any given operation, Safe threshold must remain lower or equal to the number of owners.
+
+5. Unit test
+   Such properties target specific function individually to verify their correctness. E.g., verify that a specific function can only be called by a specific address.
+
+6. Risk assessment
+   Such properties verify that worst cases that can happen to the system are handled correctly. E.g., verify that a transaction cannot be replayed.
+
+## Safe Contract Properties
+
+Verification doesn't hold for the `DELEGATECALL` operation.
+
+### Valid states
+
+### State transitions
+
+### Variable transitions
+
+### High-level properties
+
+### Unit test
+
+### Risk assessment
+
+-   nonce monotonicity, it can only increase by 1 after execTransaction call
+
+-   consistency of owner and module lists
+
+verify that `ownerCount` is in sync with the linked list.
+always circular - each address for which `isModuleEnabled` returns true should be a part of the list
+
+-   configuration changes to safe can only be done by the safe
+    who can swap owner?
+    module management
+    who should be able to?
+
+who should be allowed to make contract do delegate calls?
+contract creator
+address specified by contract creator
+
+-   setup only be done once
+
+module states
+enabled
+cancelled
+
+execTransactionFromModuleReturnData

contracts/common/StorageAccessible.sol

@@ -43,12 +43,12 @@ abstract contract StorageAccessible {
         /// @solidity memory-safe-assembly
         assembly {
             let success := delegatecall(gas(), targetContract, add(calldataPayload, 0x20), mload(calldataPayload), 0, 0)
-
-            let freeMemoryPtr := mload(0x40)
-            mstore(freeMemoryPtr, success)
-            mstore(add(freeMemoryPtr, 0x20), returndatasize())
-            returndatacopy(add(freeMemoryPtr, 0x40), 0, returndatasize())
-            revert(freeMemoryPtr, add(returndatasize(), 0x40))
+            // Load free memory location
+            let ptr := mload(0x40)
+            mstore(ptr, success)
+            mstore(add(ptr, 0x20), returndatasize())
+            returndatacopy(add(ptr, 0x40), 0, returndatasize())
+            revert(ptr, add(returndatasize(), 0x40))
         }
     }
 }