Add owner related invariants

safe-global · Jul 4, 2023 · 15e7d27 · 15e7d27
1 parent 64a0851
commit 15e7d27
Show file tree

Hide file tree

Showing 4 changed files with 43 additions and 16 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -25,8 +25,8 @@ jobs:
               uses: actions/setup-java@v3
               with: { java-version: "17", java-package: jre, distribution: semeru }
 
-            - name: Install certora cli-beta
-              run: pip install -Iv certora-cli-beta==4.2.0
+            - name: Install certora cli
+              run: pip install -Iv certora-cli
 
             - name: Install solc
               run: |

diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol
@@ -24,6 +24,10 @@ contract SafeHarness is Safe {
         return getGuard();
     }
 
+    function getOwnersCount() public view returns (uint256) {
+        return ownerCount;
+    }
+
     function getNativeTokenBalance() public view returns (uint256) {
         return address(this).balance;
     }

diff --git a/certora/scripts/verifySafe.sh b/certora/scripts/verifySafe.sh
@@ -10,7 +10,7 @@ certoraRun  certora/harnesses/SafeHarness.sol \
     --verify SafeHarness:certora/specs/Safe.spec \
     --solc solc7.6 \
     --optimistic_loop \
-    --prover_args "-optimisticFallback true" \
+    --prover_args '-optimisticFallback true' \
     --loop_iter 3 \
     --optimistic_hashing \
     --hashing_length_bound 352 \

diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec
@@ -9,17 +9,18 @@ methods {
     function getModule(address) external returns (address) envfree;
     function getSafeGuard() external returns (address) envfree;
     function getNativeTokenBalance() external returns (uint256) envfree;
+    function getOwnersCount() external returns (uint256) 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);
+    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);
 }
 
 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;
+    f.selector != sig:execTransactionFromModuleReturnData(address,uint256,bytes,Enum.Operation).selector
+    && f.selector != sig:execTransactionFromModule(address,uint256,bytes,Enum.Operation).selector 
+    && f.selector != sig:execTransaction(address,uint256,bytes,Enum.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
@@ -46,7 +47,7 @@ rule nonceMonotonicity(method f) filtered {
     uint256 nonceAfter = nonce();
 
     assert nonceAfter != nonceBefore => 
-        to_mathint(nonceAfter) == nonceBefore + 1 && f.selector == sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes).selector;
+        to_mathint(nonceAfter) == nonceBefore + 1 && f.selector == sig:execTransaction(address,uint256,bytes,Enum.Operation,uint256,uint256,uint256,address,address,bytes).selector;
 }
 
 
@@ -128,6 +129,28 @@ hook Sstore SafeHarness.(slot 49122629484629529244014240937346711770925847994644
     fallbackHandlerAddress = newFallbackHandlerAddress;
 }
 
+invariant threholdShouldBeLessThanOwners() getOwnersCount() >= getThreshold()
+    filtered { f -> reachableOnly(f) }
+    { preserved {
+        // The prover found a counterexample if the owners count is max uint256,
+        // but this is not a realistic scenario.
+        require getOwnersCount() >= 1 && getOwnersCount() < MAX_UINT256();
+      }
+    }
+
+invariant safeOwnerCannotBeItself(env e) !isOwner(e, currentContract)
+    filtered { f -> reachableOnly(f) }
+
+rule safeOwnerCannotBeSentinelAddress(env e, method f) filtered {
+    f -> reachableOnly(f)
+} {
+    calldataarg args; env e;
+    f(e, args);
+
+    assert isOwner(e, 1) == false;
+}
+
+
 rule fallbackHandlerAddressChange(method f) filtered {
     f -> f.selector != sig:simulateAndRevert(address,bytes).selector &&
          f.selector != sig:getStorageAt(uint256,uint256).selector
@@ -174,16 +197,16 @@ rule nativeTokenBalanceSpending(method f) filtered {
     uint256 balanceAfter = getNativeTokenBalance();
 
     assert balanceAfter < balanceBefore => 
-        f.selector == sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes).selector
-        || f.selector == sig:execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation).selector
-        || f.selector == sig:execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation).selector;
+        f.selector == sig:execTransaction(address,uint256,bytes,Enum.Operation,uint256,uint256,uint256,address,address,bytes).selector
+        || f.selector == sig:execTransactionFromModule(address,uint256,bytes,Enum.Operation).selector
+        || f.selector == sig:execTransactionFromModuleReturnData(address,uint256,bytes,Enum.Operation).selector;
 }
 
 rule nativeTokenBalanceSpendingExecTransaction(
         address to,
         uint256 value,
         bytes data,
-        SafeHarness.Operation operation,
+        Enum.Operation operation,
         uint256 safeTxGas,
         uint256 baseGas, 
         uint256 gasPrice, 
@@ -208,7 +231,7 @@ rule nativeTokenBalanceSpendingExecTransactionFromModule(
         address to,
         uint256 value,
         bytes data,
-        SafeHarness.Operation operation
+        Enum.Operation operation
     ) {
     uint256 balanceBefore = getNativeTokenBalance();
     env e;
@@ -226,7 +249,7 @@ rule nativeTokenBalanceSpendingExecTransactionFromModuleReturnData(
         address to,
         uint256 value,
         bytes data,
-        SafeHarness.Operation operation
+        Enum.Operation operation
 ) {
     uint256 balanceBefore = getNativeTokenBalance();
     env e;