Skip to content

Commit fec4b80

Browse files
mmv08mmv08
authored
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.
1 parent 69caefc commit fec4b80

File tree

4 files changed

+67
-47
lines changed

4 files changed

+67
-47
lines changed

‎.github/workflows/certora.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ jobs:
2929
with: { java-version: "17", java-package: jre, distribution: semeru }
3030

3131
- name: Install certora cli
32-
run: pip install -Iv certora-cli==4.13.1
32+
run: pip install -Iv certora-cli
3333

3434
- name: Install solc
3535
run: |

‎certora/applyHarness.patch‎

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
diff -druN Safe.sol Safe.sol
2-
--- Safe.sol 2023-09-29 15:38:28
3-
+++ Safe.sol 2023-09-29 15:40:17
2+
--- Safe.sol 2023-11-10 09:50:31
3+
+++ Safe.sol 2023-11-20 11:06:39
44
@@ -76,7 +76,7 @@
55
* so we create a Safe with 0 owners and threshold 1.
66
* This is an unusable Safe, perfect for the singleton
@@ -31,9 +31,19 @@ diff -druN Safe.sol Safe.sol
3131
// setupOwners checks if the Threshold is already set, therefore preventing that this method is called twice
3232
setupOwners(_owners, _threshold);
3333
if (fallbackHandler != address(0)) internalSetFallbackHandler(fallbackHandler);
34+
@@ -451,7 +453,8 @@
35+
address gasToken,
36+
address refundReceiver,
37+
uint256 _nonce
38+
- ) public view returns (bytes32) {
39+
+ ) internal view returns (bytes32) {
40+
+ // MUNGED: The function was made internal to enable CVL summaries.
41+
return keccak256(encodeTransactionData(to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, _nonce));
42+
}
43+
}
3444
diff -druN base/Executor.sol base/Executor.sol
35-
--- base/Executor.sol 2023-09-26 16:12:09
36-
+++ base/Executor.sol 2023-09-26 16:10:42
45+
--- base/Executor.sol 2023-11-10 09:50:31
46+
+++ base/Executor.sol 2023-11-20 10:28:47
3747
@@ -26,12 +26,8 @@
3848
uint256 txGas
3949
) internal returns (bool success) {

‎certora/harnesses/SafeHarness.sol‎

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,19 @@ contract SafeHarness is Safe {
5656
return getOwners().length;
5757
}
5858

59-
function callKeccak256(bytes memory data) external view returns (bytes32) {
60-
return keccak256(data);
59+
function getTransactionHashPublic(
60+
address to,
61+
uint256 value,
62+
bytes calldata data,
63+
Enum.Operation operation,
64+
uint256 safeTxGas,
65+
uint256 baseGas,
66+
uint256 gasPrice,
67+
address gasToken,
68+
address refundReceiver,
69+
uint256 _nonce
70+
) public view returns (bytes32) {
71+
// MUNGED: The function was made internal to enable CVL summaries.
72+
return getTransactionHash(to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, _nonce);
6173
}
6274
}

‎certora/specs/Signatures.spec‎

Lines changed: 38 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,14 @@ methods {
66
// harnessed
77
function signatureSplitPublic(bytes,uint256) external returns (uint8,bytes32,bytes32) envfree;
88
function getCurrentOwner(bytes32, uint8, bytes32, bytes32) external returns (address) envfree;
9+
function getTransactionHashPublic(address, uint256, bytes, Enum.Operation, uint256, uint256, uint256, address, address, uint256) external returns (bytes32) envfree;
910
// needed for the getTransactionHash ghost for the execTransaction <> signatures rule
10-
// function callKeccak256(bytes) external returns (bytes32) envfree;
1111

1212
// summaries
1313
function SignatureDecoder.signatureSplit(bytes memory signatures, uint256 pos) internal returns (uint8,bytes32,bytes32) => signatureSplitGhost(signatures,pos);
1414
function Safe.checkContractSignature(address, bytes32, bytes memory, uint256) internal => NONDET;
1515
// needed for the execTransaction <> signatures rule
16-
function getTransactionHash(
16+
function Safe.getTransactionHash(
1717
address to,
1818
uint256 value,
1919
bytes calldata data,
@@ -24,7 +24,7 @@ methods {
2424
address gasToken,
2525
address refundReceiver,
2626
uint256 _nonce
27-
) internal returns (bytes32) => transactionHashGhost(to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, _nonce) ;
27+
) internal returns (bytes32) => CONSTANT;
2828

2929
// optional
3030
function checkSignatures(bytes32,bytes) external;
@@ -93,40 +93,38 @@ rule checkSignatures() {
9393
}
9494

9595
// This rule doesn't run because of a prover error at the moment.
96-
// rule ownerSignaturesAreProvidedForExecTransaction(
97-
// address to,
98-
// uint256 value,
99-
// bytes data,
100-
// Enum.Operation operation,
101-
// uint256 safeTxGas,
102-
// uint256 baseGas,
103-
// uint256 gasPrice,
104-
// address gasToken,
105-
// address refundReceiver,
106-
// bytes signatures
107-
// ) {
108-
// uint256 nonce = nonce();
109-
// bytes32 transactionHash = getTransactionHash(
110-
// to,
111-
// value,
112-
// data,
113-
// operation,
114-
// safeTxGas,
115-
// baseGas,
116-
// gasPrice,
117-
// gasToken,
118-
// refundReceiver,
119-
// nonce
120-
// );
121-
122-
// env e;
123-
// require e.msg.value == 0;
124-
// bytes encodedTransactionData;
125-
// require encodedTransactionData.length <= 66;
126-
// checkSignatures@withrevert(e, transactionHash, encodedTransactionData, signatures);
127-
// bool checkSignaturesOk = !lastReverted;
128-
129-
// execTransaction(e, to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, signatures);
130-
131-
// assert checkSignaturesOk, "transaction executed without valid signatures";
132-
// }
96+
rule ownerSignaturesAreProvidedForExecTransaction(
97+
address to,
98+
uint256 value,
99+
bytes data,
100+
Enum.Operation operation,
101+
uint256 safeTxGas,
102+
uint256 baseGas,
103+
uint256 gasPrice,
104+
address gasToken,
105+
address refundReceiver,
106+
bytes signatures
107+
) {
108+
uint256 nonce = nonce();
109+
bytes32 transactionHash = getTransactionHashPublic(
110+
to,
111+
value,
112+
data,
113+
operation,
114+
safeTxGas,
115+
baseGas,
116+
gasPrice,
117+
gasToken,
118+
refundReceiver,
119+
nonce
120+
);
121+
122+
env e;
123+
require e.msg.value == 0;
124+
checkSignatures@withrevert(e, transactionHash, signatures);
125+
bool checkSignaturesOk = !lastReverted;
126+
127+
execTransaction(e, to, value, data, operation, safeTxGas, baseGas, gasPrice, gasToken, refundReceiver, signatures);
128+
129+
assert checkSignaturesOk, "transaction executed without valid signatures";
130+
}

0 commit comments

Comments
 (0)