Uncomment the execTransaction rule (#705)

A follow up on: #702 It uncomments the rule the ghost was meant for and adds a public method for the summarized method (summaries only work for internal methods). Removes some unused methods.
safe-global · Nov 22, 2023 · fec4b80 · fec4b80
1 parent 69caefc
commit fec4b80
Show file tree

Hide file tree

Showing 4 changed files with 67 additions and 47 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -29,7 +29,7 @@ jobs:
               with: { java-version: "17", java-package: jre, distribution: semeru }
 
             - name: Install certora cli
-              run: pip install -Iv certora-cli==4.13.1
+              run: pip install -Iv certora-cli
 
             - name: Install solc
               run: |

diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch
@@ -1,6 +1,6 @@
 diff -druN Safe.sol Safe.sol
---- Safe.sol	2023-09-29 15:38:28
-+++ Safe.sol	2023-09-29 15:40:17
+--- Safe.sol	2023-11-10 09:50:31
++++ Safe.sol	2023-11-20 11:06:39
 @@ -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,9 +31,19 @@ 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);
+@@ -451,7 +453,8 @@
+         address gasToken,
+         address refundReceiver,
+         uint256 _nonce
+-    ) public view returns (bytes32) {
++    ) internal view returns (bytes32) {
++        // MUNGED: The function was made internal to enable CVL summaries.
+         return keccak256(encodeTransactionData(to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, _nonce));
+     }
+ }
 diff -druN base/Executor.sol base/Executor.sol
---- base/Executor.sol	2023-09-26 16:12:09
-+++ base/Executor.sol	2023-09-26 16:10:42
+--- base/Executor.sol	2023-11-10 09:50:31
++++ base/Executor.sol	2023-11-20 10:28:47
 @@ -26,12 +26,8 @@
          uint256 txGas
      ) internal returns (bool success) {

diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol
@@ -56,7 +56,19 @@ contract SafeHarness is Safe {
         return getOwners().length;
     }
 
-    function callKeccak256(bytes memory data) external view returns (bytes32) {
-        return keccak256(data);
+    function getTransactionHashPublic(
+        address to,
+        uint256 value,
+        bytes calldata data,
+        Enum.Operation operation,
+        uint256 safeTxGas,
+        uint256 baseGas,
+        uint256 gasPrice,
+        address gasToken,
+        address refundReceiver,
+        uint256 _nonce
+    ) public view returns (bytes32) {
+        // MUNGED: The function was made internal to enable CVL summaries.
+        return getTransactionHash(to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, _nonce);
     }
 }
diff --git a/certora/specs/Signatures.spec b/certora/specs/Signatures.spec
@@ -6,14 +6,14 @@ methods {
     // harnessed
     function signatureSplitPublic(bytes,uint256) external returns (uint8,bytes32,bytes32) envfree;
     function getCurrentOwner(bytes32, uint8, bytes32, bytes32) external returns (address) envfree;
+    function getTransactionHashPublic(address, uint256, bytes, Enum.Operation, uint256, uint256, uint256, address, address, uint256) external returns (bytes32) envfree;
     // needed for the getTransactionHash ghost for the execTransaction <> signatures rule
-    // function callKeccak256(bytes) external returns (bytes32) envfree;
 
     // summaries
     function SignatureDecoder.signatureSplit(bytes memory signatures, uint256 pos) internal returns (uint8,bytes32,bytes32) => signatureSplitGhost(signatures,pos);
     function Safe.checkContractSignature(address, bytes32, bytes memory, uint256) internal => NONDET;
     // needed for the execTransaction <> signatures rule
-    function getTransactionHash(
+    function Safe.getTransactionHash(
         address to,
         uint256 value,
         bytes calldata data,
@@ -24,7 +24,7 @@ methods {
         address gasToken,
         address refundReceiver,
         uint256 _nonce
-    ) internal returns (bytes32) => transactionHashGhost(to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, _nonce) ;
+    ) internal returns (bytes32) => CONSTANT;
 
     // optional
     function checkSignatures(bytes32,bytes) external;
@@ -93,40 +93,38 @@ rule checkSignatures() {
 }
 
 // This rule doesn't run because of a prover error at the moment.
-// 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
-//     );
-
-//     env e;
-//     require e.msg.value == 0;
-//     bytes encodedTransactionData;
-//     require encodedTransactionData.length <= 66;
-//     checkSignatures@withrevert(e, transactionHash, encodedTransactionData, signatures);
-//     bool checkSignaturesOk = !lastReverted;
-
-//     execTransaction(e, to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, signatures);
-
-//     assert checkSignaturesOk, "transaction executed without valid signatures";
-// }
+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 = getTransactionHashPublic(
+        to,
+        value,
+        data,
+        operation,
+        safeTxGas,
+        baseGas,
+        gasPrice,
+        gasToken,
+        refundReceiver,
+        nonce
+    );
+
+    env e;
+    require e.msg.value == 0;
+    checkSignatures@withrevert(e, transactionHash, signatures);
+    bool checkSignaturesOk = !lastReverted;
+
+    execTransaction(e, to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, signatures);
+
+    assert checkSignaturesOk, "transaction executed without valid signatures";
+}