shenanigans

.github/workflows/certora.yml

@@ -15,7 +15,7 @@ jobs:
         runs-on: ubuntu-latest
         strategy:
             matrix:
-                rule: ["verifyOwners.sh", "verifySafe.sh", "verifyModules.sh"]
+                rule: ["verifyOwners.sh", "verifySafe.sh", "verifyModules.sh", "verifyNativeTokenRefund.sh"]
 
         steps:
             - uses: actions/checkout@v3

certora/conf/module.conf

@@ -11,7 +11,6 @@
     "prover_args": [
         " -smt_groundQuantifiers false"
     ],
-    "send_only": true,
     "solc": "solc7.6",
     "verify": "SafeHarness:certora/specs/ModuleReach.spec"
 }

certora/conf/owner.conf

@@ -11,7 +11,6 @@
     "prover_args": [
         " -smt_groundQuantifiers false"
     ],
-    "send_only": true,
     "solc": "solc7.6",
     "verify": "SafeHarness:certora/specs/OwnerReach.spec"
 }

certora/conf/safe.conf

@@ -12,7 +12,6 @@
         " -optimisticFallback true -s z3 -copyLoopUnroll 5 -mediumTimeout 5 -depth 30"
     ],
     "rule_sanity": "basic",
-    "send_only": true,
     "solc": "solc7.6",
     "verify": "SafeHarness:certora/specs/Safe.spec"
 }

certora/harnesses/SafeHarness.sol

@@ -28,6 +28,10 @@ contract SafeHarness is Safe {
         return address(this).balance;
     }
 
+    function getNativeTokenBalanceFor(address addr) public view returns (uint256) {
+        return addr.balance;
+    }
+
     function getOwnersCount() public view returns (uint256) {
         return ownerCount;
     }

certora/mutationTesting.md

@@ -1,4 +1,4 @@
-To run gambit you run ```certoraMutate``` with the prover conf file and the gambit conf file. A prover conf file is generated everytime you run the prover using your script. Prover conf files are an alternate way to run the prover by calling certoraRun and giving it the prover file ```certoraRun path/to/prover/conf/file.conf```. Auto generated prover conf files can be found in ```.certora_internal/latest/run.conf```. Copy this to a conf file in ```./certora/conf```. The gambit conf file points to the contract that you want to mutate and num_mutants specifies the number of mutations to be generated. Gambit runs the spec with the original code as well as the mutations generated. Analyzing which mutations your spec caught/ failed to catch, can give you a pretty good understanding of your spec coverage.
+To run gambit you run `certoraMutate` with the prover conf file and the gambit conf file. A prover conf file is generated every time you run the prover using your script. Prover conf files are an alternate way to run the prover by calling certoraRun and giving it the prover file `certoraRun path/to/prover/conf/file.conf`. Auto-generated prover conf files are in `.certora_internal/latest/run.conf`. Copy this to a conf file in `./certora/conf`. The gambit conf file points to the contract you want to mutate, and num_mutants specifies the number of mutations to generate. Gambit runs the spec with the original code and the mutations generated. Analyzing which mutations your spec caught can give you a pretty good understanding of your spec coverage.
 
 Run the following command from the root:
 
@@ -7,18 +7,21 @@ certoraMutate --prover_conf path/to/conf/file.conf --mutation_conf path/to/gambi
 ```
 
 example
+
 ```bash
 certoraMutate --prover_conf certora/conf/safe.conf --mutation_conf gambit.conf
 ```
 
-After submitting all the mutation testing jobs to the server, gambit generates a ``collect.json`` file with all the information needed to collect the results of mutation testing. After a few hours, you can collect these results with the following command:
+After submitting all the mutation testing jobs to the server, the gambit generates a `collect.json` file with all the information needed to collect the mutation testing results. After a few hours, you can collect these results with the following command:
 
 ```bash
 certoraMutate --collect_file collect.json
 ```
+
 You will get a link to the mutation test report after all the results have been collected successfully.
 
 Optionally, you can also have the results of mutation testing dumped into a csv file as follows:
+
 ```bash
 certoraMutate --collect_file collect.json --dump_csv path/to/csv/file.csv
-```
+```

certora/scripts/verifyModules.sh

@@ -6,13 +6,6 @@ if [[ -n "$CI" ]]; then
     params=()
 fi
 
-certoraRun  certora/harnesses/SafeHarness.sol \
-    --verify SafeHarness:certora/specs/ModuleReach.spec \
-    --solc solc7.6 \
-    --optimistic_loop \
-    --prover_args '-smt_groundQuantifiers false' \
-    --loop_iter 3 \
-    --optimistic_hashing \
-    --hashing_length_bound 352 \
+certoraRun certora/conf/module.conf \
     "${params[@]}" \
     --msg "Safe $1 "

certora/scripts/verifyNativeTokenRefund.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/NativeTokenRefund.spec \
+    --solc solc7.6 \
+    --optimistic_loop \
+    --prover_args '-optimisticFallback true -s z3' \
+    --loop_iter 3 \
+    --optimistic_hashing \
+    --hashing_length_bound 352 \
+    --rule_sanity \
+    "${params[@]}" \
+    --msg "Safe $1 "

certora/scripts/verifyOwners.sh

@@ -6,13 +6,6 @@ if [[ -n "$CI" ]]; then
     params=()
 fi
 
-certoraRun  certora/harnesses/SafeHarness.sol \
-    --verify SafeHarness:certora/specs/OwnerReach.spec \
-    --solc solc7.6 \
-    --optimistic_loop \
-    --prover_args '-smt_groundQuantifiers false' \
-    --loop_iter 3 \
-    --optimistic_hashing \
-    --hashing_length_bound 352 \
+certoraRun certora/conf/owner.conf \
     "${params[@]}" \
     --msg "Safe $1 "

certora/scripts/verifySafe.sh

@@ -6,15 +6,6 @@ if [[ -n "$CI" ]]; then
     params=()
 fi
 
-certoraRun  certora/harnesses/SafeHarness.sol \
-    --verify SafeHarness:certora/specs/Safe.spec \
-    --solc solc7.6 \
-    --optimistic_loop \
-    --prover_args '-optimisticFallback true -s z3' \
-    --loop_iter 3 \
-    --optimistic_hashing \
-    --hashing_length_bound 352 \
-    --rule_sanity \
-    --rule setupCorrectlyConfiguresSafe \
+certoraRun certora/conf/safe.conf \
     "${params[@]}" \
     --msg "Safe $1 "

certora/specs/NativeTokenRefund.spec

@@ -0,0 +1,60 @@
+// This spec is a separate file because we summarize checkSignatures here
+
+methods {
+    function checkSignatures(bytes32, bytes memory, bytes memory) internal => NONDET;
+
+    function getNativeTokenBalanceFor(address) external returns (uint256) envfree;
+    function getSafeGuard() external returns (address) envfree;
+}
+
+ghost uint256 gasPriceEnv {
+    init_state axiom gasPriceEnv == 1;
+}
+
+// We need to make sure that the gas price is not zero. There's no env variable available in the CVL, so we use an opcode hook with a
+// ghost variable.
+hook GASPRICE uint v {
+    require v > 0;
+    gasPriceEnv = v;
+}
+
+rule nativeTokenRefundIsSentToRefundReceiver(
+    address to,
+    uint256 value,
+    bytes data,
+    Enum.Operation operation,
+    uint64 safeTxGas,
+    uint64 baseGas,
+    uint256 gasPrice,
+    address gasToken,
+    address refundReceiver,
+    bytes signatures
+) {
+    env e;
+
+    // gas token address must be zero for native token refund
+    require gasToken == 0;
+    // gas refund parameters must be set
+    require baseGas > 0 && gasPrice > 0;
+
+    // the refund receiver must not be zero, because in such a case tx.origin will be used and it'll come up with countexamples related to overflow
+    // and adding pre-requirements is tricky
+    // also, it shouldn't be the safe itself 
+    require refundReceiver != 0 && refundReceiver != currentContract;
+    // // We're being optimistic about the delegatecall and in the munged contracts the actuall call was removed
+    // // So it's possible the gas used to be 0 in the munged contracts, so no refund would be sent (a counterexample)
+    // require operation == Enum.Operation.Call;
+
+    // The guard has to be zero, because otherwise it makes an extcall and the prover HAVOCs;
+    require getSafeGuard() == 0;
+
+    uint256 balanceBefore = getNativeTokenBalanceFor(refundReceiver);
+    require balanceBefore == 0;
+
+    execTransaction(e, to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, signatures);
+
+    uint256 balanceAfter = getNativeTokenBalanceFor(refundReceiver);
+
+    // It's not possible to calculate the exact amount because it varies on many factors (such as gas used, actual gas price used, etc)
+    assert to_mathint(balanceAfter) > to_mathint(balanceBefore);
+}

certora/specs/Safe.spec

@@ -16,6 +16,8 @@ methods {
     function execTransactionFromModuleReturnData(address,uint256,bytes,Enum.Operation) external returns (bool, bytes memory);
     function execTransactionFromModule(address,uint256,bytes,Enum.Operation) external returns (bool);
     function execTransaction(address,uint256,bytes,Enum.Operation,uint256,uint256,uint256,address,address,bytes) external returns (bool);
+
+    function checkSignatures(bytes32, bytes memory, bytes memory) internal => NONDET;
 }
 
 definition noHavoc(method f) returns bool =
@@ -31,7 +33,7 @@ definition reachableOnly(method f) returns bool =
     // "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;
+definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff;
 
 /// Nonce must never decrease
 rule nonceMonotonicity(method f) filtered {
@@ -76,17 +78,6 @@ ghost address fallbackHandlerAddress {
     init_state axiom fallbackHandlerAddress == 0;
 }
 
-ghost mapping(address => address) ghostOwners {
-    init_state axiom forall address X. to_mathint(ghostOwners[X]) == 0;
-}
-
-// hook to update the ghostOwners and the reach ghost state whenever the owners field
-// in storage is written. 
-// This also checks that the reach_succ invariant is preserved. 
-hook Sstore currentContract.owners[KEY address key] address value STORAGE {
-    ghostOwners[key] = value;
-}
-
 // This is Safe's fallback handler storage slot:
 // 0x6c9a6c4a39284e37ed1cf53d337577d14212a4870fb976a4366c693b939918d5
 // converted to decimal because certora doesn't seem to support hex yet.

gambit.conf

@@ -1,6 +1,6 @@
-
-{ "gambit": {
-      "filename" : "certora/munged/Safe.sol",
-      "num_mutants": 15
-   }
-}
+{
+  "gambit": {
+    "filename": "certora/munged/Safe.sol",
+    "num_mutants": 15
+  }
+}

mutationSafe.conf

@@ -1,13 +1,12 @@
-
-{ "gambit": [
 {
-      "filename" : "certora/munged/Safe.sol",
+  "gambit": [
+    {
+      "filename": "certora/munged/Safe.sol",
       "num_mutants": 5
-   },
-{
-      "filename" : "certora/munged/base/OwnerManager.sol",
+    },
+    {
+      "filename": "certora/munged/base/OwnerManager.sol",
       "num_mutants": 5
-   }
-
-   ]
-}
+    }
+  ]
+}