Fix the methods block in the specs

safe-global · Sep 27, 2023 · bc08fb0 · bc08fb0
1 parent 1abedf3
commit bc08fb0
Show file tree

Hide file tree

Showing 9 changed files with 191 additions and 228 deletions.
diff --git a/.github/workflows/certora.yml b/.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", "verifySignatures.sh"]
 
         steps:
             - uses: actions/checkout@v3

diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch
@@ -1,6 +1,6 @@
 diff -druN Safe.sol Safe.sol
---- Safe.sol	2023-09-27 10:13:46
-+++ Safe.sol	2023-09-27 10:14:12
+--- Safe.sol	2023-09-27 13:31:45
++++ Safe.sol	2023-09-27 14:34:22
 @@ -76,7 +76,7 @@
           * so we create a Safe with 0 owners and threshold 1.
           * This is an unusable Safe, perfect for the singleton
@@ -31,7 +31,7 @@ diff -druN Safe.sol Safe.sol
          // setupOwners checks if the Threshold is already set, therefore preventing that this method is called twice
          setupOwners(_owners, _threshold);
          if (fallbackHandler != address(0)) internalSetFallbackHandler(fallbackHandler);
-@@ -349,7 +351,6 @@
+@@ -362,7 +364,6 @@
              lastOwner = currentOwner;
          }
      }

diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol
@@ -52,7 +52,7 @@ contract SafeHarness is Safe {
         return getOwners().length;
     }
 
-    function call_keccak256(bytes memory b) external view returns (bytes32) {
-        return keccak256(b);
+    function callKeccak256(bytes memory data) external view returns (bytes32) {
+        return keccak256(data);
     }
 }
diff --git a/certora/scripts/verifySafe.sh b/certora/scripts/verifySafe.sh
@@ -11,8 +11,7 @@ certoraRun  certora/harnesses/SafeHarness.sol \
     --solc solc7.6 \
     --optimistic_loop \
     --prover_args '-optimisticFallback true -mediumTimeout 30' \
-    --loop_iter 2 \
-    --rule checkSignatures \
+    --loop_iter 3 \
     --optimistic_hashing \
     --hashing_length_bound 352 \
     --rule_sanity \

diff --git a/certora/scripts/verifySafeSummarize.sh → certora/scripts/verifySignatures.sh b/certora/scripts/verifySafeSummarize.sh → certora/scripts/verifySignatures.sh
@@ -7,14 +7,14 @@ if [[ -n "$CI" ]]; then
 fi
 
 certoraRun  certora/harnesses/SafeHarness.sol \
-    --verify SafeHarness:certora/specs/SafeSummarize.spec \
+    --verify SafeHarness:certora/specs/Signatures.spec \
     --solc solc7.6 \
     --optimistic_loop \
-    --prover_args '-optimisticFallback true -s z3 -copyLoopUnroll 5 -mediumTimeout 5 -depth 30' \
-    --loop_iter 2 \
-    --rule ownerSignaturesAreProvidedForExecTransaction \
+    --prover_args '-optimisticFallback true -mediumTimeout 30' \
+    --loop_iter 3 \
     --optimistic_hashing \
     --hashing_length_bound 352 \
     --rule_sanity \
     "${params[@]}" \
-    --msg "Safe $1 "
+    --msg "Safe $*" \
+    "$@"
diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec
@@ -2,36 +2,21 @@ methods {
     function getThreshold() external returns (uint256) envfree;
     function disableModule(address,address) external;
     function nonce() external returns (uint256) envfree;
-    function isOwner(address) external returns (bool) envfree;
     function signedMessages(bytes32) external returns (uint256) envfree;
-    function signatureSplitPublic(bytes,uint256) external returns (uint8,bytes32,bytes32) envfree;
-    function getTransactionHash(address,uint256,bytes,Enum.Operation,uint256,uint256,uint256,address,address,uint256) external returns (bytes32) envfree;
 
     // harnessed
     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;
     function getOwnersCountFromArray() external returns (uint256) envfree;
-    function getCurrentOwner(bytes32, uint8, bytes32, bytes32) external returns (address) envfree;
-
-    // summaries
-    function SignatureDecoder.signatureSplit(bytes memory signatures, uint256 pos) internal returns (uint8,bytes32,bytes32) => mySignatureSplit(signatures,pos);
-    function Safe.checkExternalSignature(address, bytes32, bytes memory) internal => NONDET;
 
     // optional
-    function checkSignatures(bytes32,bytes,bytes) external envfree;
     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 _.isValidSignature(bytes32, bytes) external => NONDET;
 }
 
-definition noHavoc(method f) returns bool =
-    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
     && f.selector != sig:simulateAndRevert(address,bytes).selector
@@ -40,15 +25,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;
-
-ghost mapping(bytes => mapping(uint256 => uint8)) mySigSplitV;
-ghost mapping(bytes => mapping(uint256 => bytes32)) mySigSplitR;
-ghost mapping(bytes => mapping(uint256 => bytes32)) mySigSplitS;
-
-function mySignatureSplit(bytes signatures, uint256 pos) returns (uint8,bytes32,bytes32) {
-    return (mySigSplitV[signatures][pos], mySigSplitR[signatures][pos], mySigSplitS[signatures][pos]);
-}
+definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff;
 
 /// Nonce must never decrease
 rule nonceMonotonicity(method f) filtered {
@@ -151,86 +128,6 @@ rule nativeTokenBalanceSpending(method f) filtered {
         || f.selector == sig:execTransactionFromModuleReturnData(address,uint256,bytes,Enum.Operation).selector;
 }
 
-// checkSignatures called once is equivalent to checkSignatures called twice
-rule checkSignatures() {
-    bytes32 dataHash;
-    bytes data;
-    address executor;
-    env e;
-    bytes signaturesAB;
-    bytes signaturesA;
-    bytes signaturesB;
-    uint8 vA; bytes32 rA; bytes32 sA;
-    uint8 vB; bytes32 rB; bytes32 sB;
-    uint8 vAB1; bytes32 rAB1; bytes32 sAB1;
-    uint8 vAB2; bytes32 rAB2; bytes32 sAB2;
-    vA, rA, sA = signatureSplitPublic(signaturesA, 0);
-    vB, rB, sB = signatureSplitPublic(signaturesB, 0);
-    vAB1, rAB1, sAB1 = signatureSplitPublic(signaturesAB, 0);
-    vAB2, rAB2, sAB2 = signatureSplitPublic(signaturesAB, 1);
-    require to_mathint(signaturesAB.length) == signaturesA.length + signaturesB.length;
-
-    require vA == vAB1 && rA == rAB1 && sA == sAB1;
-    require vB == vAB2 && rB == rAB2 && sB == sAB2;
-    require vA != 0 && vB != 0;
-    require data.length < 1000;
-    require signaturesA.length < 1000;
-    require signaturesB.length < 1000;
-    require signaturesAB.length < 1000;
-    require signaturesA.length >= 65;
-    require signaturesB.length >= 65;
-    require signaturesAB.length >= 130;
-    require !isOwner(currentContract);
-    require getThreshold() <= 2;
-    require getCurrentOwner(dataHash, vA, rA, sA) < getCurrentOwner(dataHash, vB, rB, sB);
-
-    checkNSignatures@withrevert(e, executor, dataHash, data, signaturesA, 1);
-    bool successA = !lastReverted;
-    checkNSignatures@withrevert(e, executor, dataHash, data, signaturesB, 1);
-    bool successB = !lastReverted;
-
-    checkNSignatures@withrevert(e, executor, dataHash, data, signaturesAB, 2);
-    bool successAB = !lastReverted;
-
-    assert (successA && successB) <=> successAB, "checkSignatures called must be equivalent to checkSignatures called twice";
-}
-
-rule ownerSignaturesAreProvidedForExecTransaction(
-        address to,
-        uint256 value,
-        bytes data,
-        Enum.Operation operation,
-        uint256 safeTxGas,
-        uint256 baseGas,
-        uint256 gasPrice,
-        address gasToken,
-        address refundReceiver,
-        bytes signatures
-    ) {
-    uint256 nonce = nonce();
-    bytes32 transactionHash = getTransactionHash(
-        to,
-        value,
-        data,
-        operation,
-        safeTxGas,
-        baseGas,
-        gasPrice,
-        gasToken,
-        refundReceiver,
-        nonce
-    );
-
-    bytes encodedTransactionData;
-    checkSignatures@withrevert(transactionHash, encodedTransactionData, signatures);
-    bool checkSignaturesOk = !lastReverted;
-
-    env e;
-    execTransaction(e, to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, signatures);
-
-    assert checkSignaturesOk, "transaction executed without valid signatures";
-}
-
 
 rule nativeTokenBalanceSpendingExecTransaction(
         address to,

diff --git a/certora/specs/SafeSummarize.spec b/certora/specs/SafeSummarize.spec