Merge pull request #560 from safe-global/formal-verification

Bootstrap formal verification setup

.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

.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

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