Skip to content

Commit

Permalink
Updated the rules and conf
Browse files Browse the repository at this point in the history
  • Loading branch information
@remedcu
remedcu committed Jul 16, 2024
1 parent 0d9a30e commit 4aac4f2
Show file tree
Hide file tree
Showing 3 changed files with 21 additions and 33 deletions.
1 change: 1 addition & 0 deletions modules/4337/certora/conf/SignatureLengthCheck.conf
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
"certora/harnesses/Safe4337ModuleHarness.sol",
"certora/harnesses/Account.sol",
],
"loop_iter": "3",
"optimistic_loop": true,
"msg": "Safe4337Module: Signatures Length Check",
"rule_sanity": "basic",
Expand Down
42 changes: 18 additions & 24 deletions modules/4337/certora/harnesses/Account.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,35 +58,35 @@ contract Account is Safe {
Actual Signature:
"0x" +
"0000000000000000000000000000000000000000000000000000000000000001 00000000000000000000000000000000000000000000000000000000000000c3 00" + // encoded EIP-1271 signature 1
"0000000000000000000000000000000000000000000000000000000000000002 0000000000000000000000000000000000000000000000000000000000000103 00" + // encoded EIP-1271 signature 2
"0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000000147 00" + // encoded EIP-1271 signature 3
"0000000000000000000000000000000000000000000000000000000000000004 00000000000000000000000000000000000000000000000000000000deadbeef" // length of bytes + data of bytes of signature 1
"0000000000000000000000000000000000000000000000000000000000000002 00000000000000000000000000000000000000000000000000000000000000e7 00" + // encoded EIP-1271 signature 2
"0000000000000000000000000000000000000000000000000000000000000003 000000000000000000000000000000000000000000000000000000000000012b 00" + // encoded EIP-1271 signature 3
"0000000000000000000000000000000000000000000000000000000000000004 deadbeef" // length of bytes + data of bytes of signature 1
"0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 2
"0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000efbeef" // length of bytes + data of bytes of signature 3
"0000000000000000000000000000000000000000000000000000000000000003 efbeef" // length of bytes + data of bytes of signature 3
0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c30000000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000103000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000014700000000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef00000000000000000000000000000000000000000000000000000000000000030000000000000000000000000000000000000000000000000000000000efbeef
0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c300000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000e7000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000012b000000000000000000000000000000000000000000000000000000000000000004deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000003efbeef
With Excess Data Type 1:
"0x" +
"0000000000000000000000000000000000000000000000000000000000000001 00000000000000000000000000000000000000000000000000000000000000c3 00" + // encoded EIP-1271 signature 1
"0000000000000000000000000000000000000000000000000000000000000002 0000000000000000000000000000000000000000000000000000000000000103 00" + // encoded EIP-1271 signature 2
"0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000000147 00" + // encoded EIP-1271 signature 3
"0000000000000000000000000000000000000000000000000000000000000008 00000000000000000000000000000000000000000000000000000000deadbeef" // length of bytes + data of bytes of signature 1
"0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 2
"0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000efbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 3 + excess data
"0000000000000000000000000000000000000000000000000000000000000001 00000000000000000000000000000000000000000000000000000000000000c3 00" + // encoded EIP-1271 signature 1
"0000000000000000000000000000000000000000000000000000000000000002 00000000000000000000000000000000000000000000000000000000000000e7 00" + // encoded EIP-1271 signature 2
"0000000000000000000000000000000000000000000000000000000000000003 000000000000000000000000000000000000000000000000000000000000012b 00" + // encoded EIP-1271 signature 3
"0000000000000000000000000000000000000000000000000000000000000004 deadbeef" // length of bytes + data of bytes of signature 1
"0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 2
"0000000000000000000000000000000000000000000000000000000000000003 efbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 3 + excess data
0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c30000000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000103000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000014700000000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef00000000000000000000000000000000000000000000000000000000000000030000000000000000000000000000000000000000000000000000000000efbeefdeadbeefdeadbeefdeadbeef
0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c300000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000e7000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000012b000000000000000000000000000000000000000000000000000000000000000004deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000003efbeefdeadbeefdeadbeefdeadbeef
With Excess Data Type 2:
"0x" +
"0000000000000000000000000000000000000000000000000000000000000001 00000000000000000000000000000000000000000000000000000000000000c3 00" + // encoded EIP-1271 signature 1
"0000000000000000000000000000000000000000000000000000000000000002 0000000000000000000000000000000000000000000000000000000000000107 00" + // encoded EIP-1271 signature 2
"0000000000000000000000000000000000000000000000000000000000000003 000000000000000000000000000000000000000000000000000000000000014b 00" + // encoded EIP-1271 signature 3
"0000000000000000000000000000000000000000000000000000000000000008 00000000000000000000000000000000000000000000000000000000deadbeefdeadbeef" // length of bytes + data of bytes of signature 1 + excess data
"0000000000000000000000000000000000000000000000000000000000000002 00000000000000000000000000000000000000000000000000000000000000eb 00" + // encoded EIP-1271 signature 2
"0000000000000000000000000000000000000000000000000000000000000003 000000000000000000000000000000000000000000000000000000000000012f 00" + // encoded EIP-1271 signature 3
"0000000000000000000000000000000000000000000000000000000000000004 deadbeefdeadbeef" // length of bytes + data of bytes of signature 1 + excess data
"0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 2
"0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000efbeef" // length of bytes + data of bytes of signature 3
"0000000000000000000000000000000000000000000000000000000000000003 efbeef" // length of bytes + data of bytes of signature 3
0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c30000000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000107000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000014b00000000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000deadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef00000000000000000000000000000000000000000000000000000000000000030000000000000000000000000000000000000000000000000000000000efbeef
0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c300000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000eb000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000012f000000000000000000000000000000000000000000000000000000000000000004deadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000003efbeef
All three will have the same canonical hash: 0xe304234a47e4f89d0a95d9fafb42e9c3143e23e951d38add9f781c34f962deb7
*/
Expand All @@ -108,13 +108,7 @@ contract Account is Safe {
uint256 signatureLength = uint256(bytes32(signatures[signatureOffset:]));
require(signatureLength > 0, "Invalid signature length");

bytes memory signature;
if (signatureLength < 0x20) {
signature = signatures[signatureOffset+0x40-signatureLength:][:signatureLength];
}
else {
signature = signatures[signatureOffset+0x20:][:signatureLength];
}
bytes memory signature = signatures[signatureOffset+0x20:][:signatureLength];

// Make sure to update the static part so that the smart contract signature
// points to the "canonical" signature offset (i.e. that all contract
Expand Down
11 changes: 2 additions & 9 deletions modules/4337/certora/specs/SignatureLengthCheck.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,15 +8,8 @@ methods {
function safeContract.canonicalSignatureHash(bytes, uint256) external returns(bytes32) envfree;
}

// This rule verifies that if excess data is added to the dynamic part of the signature, then the signature check will fail.
rule signatureLengthCheckDirectly(bytes signatures, bytes gasGriefingData, uint256 threshold) {
require signatures.length > 0;
require gasGriefingData.length > 0;
assert checkSignaturesLength(signatures, threshold) => !checkSignaturesLength(combineBytes(signatures, gasGriefingData), threshold);
}

// This rule verifies that if excess data is added to the dynamic part of the signature, though it could pass in the safe contract's
// `checkSignatures(...)`, it will be caught within the `_checkSignaturesLength(...)` call, as the dynamic length is checked.
// This rule verifies that if excess data is added to the signature, though it could pass in the safe contract's `checkSignatures(...)`,
// it will be caught within the `_checkSignaturesLength(...)` call, as the dynamic length is checked.
rule canonicalHashBasedLengthCheck(bytes signatures, bytes griefedSignatures, uint256 threshold) {
require safeContract.canonicalSignatureHash(signatures, threshold) == safeContract.canonicalSignatureHash(griefedSignatures, threshold);
require signatures.length < griefedSignatures.length;
Expand Down

0 comments on commit 4aac4f2

Please sign in to comment.