Merge pull request #600 from safe-global/certora/treshold-ownercount

Formal verification: add owner related invariants
safe-global · Jul 4, 2023 · 47a3620 · 47a3620
2 parents 325aa47 + b2006f7
commit 47a3620
Show file tree

Hide file tree

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

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
@@ -130,6 +130,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(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