From 0c2e1e9518765c717b0022105c3a554f05988e81 Mon Sep 17 00:00:00 2001 From: Shebin John Date: Mon, 15 Jul 2024 15:40:14 +0200 Subject: [PATCH 01/10] Signature Length Check FV --- .../certora/conf/SignatureLengthCheck.conf | 15 ++++ modules/4337/certora/harnesses/Account.sol | 89 +++++++++++++++++++ .../harnesses/Safe4337ModuleHarness.sol | 15 ++++ .../certora/specs/SignatureLengthCheck.spec | 27 ++++++ 4 files changed, 146 insertions(+) create mode 100644 modules/4337/certora/conf/SignatureLengthCheck.conf create mode 100644 modules/4337/certora/harnesses/Safe4337ModuleHarness.sol create mode 100644 modules/4337/certora/specs/SignatureLengthCheck.spec diff --git a/modules/4337/certora/conf/SignatureLengthCheck.conf b/modules/4337/certora/conf/SignatureLengthCheck.conf new file mode 100644 index 000000000..055bca8a5 --- /dev/null +++ b/modules/4337/certora/conf/SignatureLengthCheck.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "certora/harnesses/Safe4337ModuleHarness.sol", + "certora/harnesses/Account.sol", + ], + "optimistic_loop": true, + "msg": "Safe4337Module: Signatures Length Check", + "rule_sanity": "basic", + "solc": "solc8.23", + "verify": "Safe4337ModuleHarness:certora/specs/SignatureLengthCheck.spec", + "packages": [ + "@account-abstraction=../../node_modules/.pnpm/@account-abstraction+contracts@0.7.0/node_modules/@account-abstraction", + "@safe-global=../../node_modules/.pnpm/@safe-global+safe-contracts@1.4.1-build.0_ethers@6.13.1_bufferutil@4.0.8_utf-8-validate@5.0.10_/node_modules/@safe-global" + ] +} diff --git a/modules/4337/certora/harnesses/Account.sol b/modules/4337/certora/harnesses/Account.sol index 680111031..788881671 100644 --- a/modules/4337/certora/harnesses/Account.sol +++ b/modules/4337/certora/harnesses/Account.sol @@ -53,6 +53,95 @@ contract Account is Safe { function getValidUntilTimestamp(bytes calldata sigs) external pure returns (uint48) { return uint48(bytes6(sigs[6:12])); } + + /* + 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 + "0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 2 + "0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000efbeef" // length of bytes + data of bytes of signature 3 + + 0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c30000000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000103000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000014700000000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef00000000000000000000000000000000000000000000000000000000000000030000000000000000000000000000000000000000000000000000000000efbeef + + 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 + + 0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c30000000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000103000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000014700000000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef00000000000000000000000000000000000000000000000000000000000000030000000000000000000000000000000000000000000000000000000000efbeefdeadbeefdeadbeefdeadbeef + + 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 + "0000000000000000000000000000000000000000000000000000000000000024 deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" // length of bytes + data of bytes of signature 2 + "0000000000000000000000000000000000000000000000000000000000000003 0000000000000000000000000000000000000000000000000000000000efbeef" // length of bytes + data of bytes of signature 3 + + 0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c30000000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000107000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000014b00000000000000000000000000000000000000000000000000000000000000000400000000000000000000000000000000000000000000000000000000deadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef00000000000000000000000000000000000000000000000000000000000000030000000000000000000000000000000000000000000000000000000000efbeef + + All three will have the same canonical hash: 0xe304234a47e4f89d0a95d9fafb42e9c3143e23e951d38add9f781c34f962deb7 + */ + function canonicalSignatureHash(bytes calldata signatures, uint256 threshold) public pure returns (bytes32 canonical) { + uint256 dynamicOffset = threshold * 0x41; + bytes memory staticPart = signatures[:dynamicOffset]; + bytes memory dynamicPart = ""; + + for (uint256 i = 0; i < threshold; i++) { + uint256 ptr = i * 0x41; + uint8 v = uint8(signatures[ptr + 0x40]); + + // Check to see if we have a smart contract signature, and if we do, then append + // the signature to the dynamic part. + if (v == 0) { + uint256 signatureOffset = uint256(bytes32(signatures[ptr + 0x20:])); + require(signatureOffset >= dynamicOffset, "Invalid signature offset"); + + 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]; + } + + // Make sure to update the static part so that the smart contract signature + // points to the "canonical" signature offset (i.e. that all contract + // signatures are tightly packed one after the other in order). This ensures + // a canonical representation for the signatures. + /* solhint-disable no-inline-assembly */ + assembly ("memory-safe") { + mstore(add(staticPart, add(0x40, ptr)), dynamicOffset) + } + /* solhint-enable no-inline-assembly */ + dynamicOffset += signatureLength + 0x20; + dynamicPart = abi.encodePacked(dynamicPart, signatureLength, signature); + } + } + canonical = keccak256(abi.encodePacked(staticPart, dynamicPart)); + } + + function containsContractSignature(bytes calldata signatures, uint256 threshold) public pure returns (bool) { + for (uint256 i = 0; i < threshold; i++) { + uint256 ptr = i * 0x41; + uint8 v = uint8(signatures[ptr + 0x40]); + if (v == 0) { + return true; + } + } + return false; + } } // @notice This is a harness contract for the rule that verfies the validation data diff --git a/modules/4337/certora/harnesses/Safe4337ModuleHarness.sol b/modules/4337/certora/harnesses/Safe4337ModuleHarness.sol new file mode 100644 index 000000000..5552c88b0 --- /dev/null +++ b/modules/4337/certora/harnesses/Safe4337ModuleHarness.sol @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: LGPL-3.0-only +pragma solidity >=0.8.0; +import {Safe4337Module} from "./../../contracts/Safe4337Module.sol"; + +contract Safe4337ModuleHarness is Safe4337Module { + constructor(address entryPoint) Safe4337Module(entryPoint) {} + + function checkSignaturesLength(bytes calldata signatures, uint256 threshold) external pure returns (bool) { + return _checkSignaturesLength(signatures, threshold); + } + + function combineBytes(bytes calldata signatures, bytes calldata data) external pure returns (bytes memory) { + return abi.encode(signatures, data); + } +} diff --git a/modules/4337/certora/specs/SignatureLengthCheck.spec b/modules/4337/certora/specs/SignatureLengthCheck.spec new file mode 100644 index 000000000..ba80d9348 --- /dev/null +++ b/modules/4337/certora/specs/SignatureLengthCheck.spec @@ -0,0 +1,27 @@ +using Account as safeContract; + +methods { + function checkSignaturesLength(bytes, uint256) external returns(bool) envfree; + function combineBytes(bytes, bytes) external returns(bytes) envfree; + + // Safe Contract functions + function safeContract.containsContractSignature(bytes, uint256) external returns(bool) envfree; + 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. +rule canonicalHashBasedLengthCheck(bytes signatures, bytes griefedSignatures, uint256 threshold) { + require safeContract.canonicalSignatureHash(signatures, threshold) == safeContract.canonicalSignatureHash(griefedSignatures, threshold); + require signatures.length < griefedSignatures.length; + require safeContract.containsContractSignature(signatures, threshold); + + assert checkSignaturesLength(signatures, threshold) => !checkSignaturesLength(griefedSignatures, threshold); +} From 764de0977215870291f46dfbc872f06619ada665 Mon Sep 17 00:00:00 2001 From: Shebin John Date: Mon, 15 Jul 2024 15:53:53 +0200 Subject: [PATCH 02/10] Adding CI workflow --- .github/workflows/certora_4337.yml | 2 +- .../certora/scripts/verifySignatureLengthCheck.sh | 12 ++++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) create mode 100755 modules/4337/certora/scripts/verifySignatureLengthCheck.sh diff --git a/.github/workflows/certora_4337.yml b/.github/workflows/certora_4337.yml index d6dd5c0ee..510c2c78e 100644 --- a/.github/workflows/certora_4337.yml +++ b/.github/workflows/certora_4337.yml @@ -19,7 +19,7 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - rule: ['verify4337Module.sh', 'verifyTransactionExecutionMethods.sh', 'verifyValidationData.sh'] + rule: ['verify4337Module.sh', 'verifyTransactionExecutionMethods.sh', 'verifyValidationData.sh', 'verifySignatureLengthCheck.sh'] steps: - uses: actions/checkout@v3 diff --git a/modules/4337/certora/scripts/verifySignatureLengthCheck.sh b/modules/4337/certora/scripts/verifySignatureLengthCheck.sh new file mode 100755 index 000000000..702f55feb --- /dev/null +++ b/modules/4337/certora/scripts/verifySignatureLengthCheck.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +params=() + +if [[ -n "$CI" ]]; then + params=("--wait_for_results") +fi + +certoraRun certora/conf/SignatureLengthCheck.conf \ + "${params[@]}" \ + "$@" + From 0d9a30e5428e0d9832e69022fa7e5b031a612e0d Mon Sep 17 00:00:00 2001 From: Shebin John Date: Tue, 16 Jul 2024 10:11:20 +0200 Subject: [PATCH 03/10] Unnecessary check removed --- modules/4337/certora/harnesses/Account.sol | 17 +++-------------- .../certora/specs/SignatureLengthCheck.spec | 4 +--- 2 files changed, 4 insertions(+), 17 deletions(-) diff --git a/modules/4337/certora/harnesses/Account.sol b/modules/4337/certora/harnesses/Account.sol index 788881671..812914337 100644 --- a/modules/4337/certora/harnesses/Account.sol +++ b/modules/4337/certora/harnesses/Account.sol @@ -90,12 +90,12 @@ contract Account is Safe { All three will have the same canonical hash: 0xe304234a47e4f89d0a95d9fafb42e9c3143e23e951d38add9f781c34f962deb7 */ - function canonicalSignatureHash(bytes calldata signatures, uint256 threshold) public pure returns (bytes32 canonical) { - uint256 dynamicOffset = threshold * 0x41; + function canonicalSignatureHash(bytes calldata signatures, uint256 safeThreshold) public pure returns (bytes32 canonical) { + uint256 dynamicOffset = safeThreshold * 0x41; bytes memory staticPart = signatures[:dynamicOffset]; bytes memory dynamicPart = ""; - for (uint256 i = 0; i < threshold; i++) { + for (uint256 i = 0; i < safeThreshold; i++) { uint256 ptr = i * 0x41; uint8 v = uint8(signatures[ptr + 0x40]); @@ -131,17 +131,6 @@ contract Account is Safe { } canonical = keccak256(abi.encodePacked(staticPart, dynamicPart)); } - - function containsContractSignature(bytes calldata signatures, uint256 threshold) public pure returns (bool) { - for (uint256 i = 0; i < threshold; i++) { - uint256 ptr = i * 0x41; - uint8 v = uint8(signatures[ptr + 0x40]); - if (v == 0) { - return true; - } - } - return false; - } } // @notice This is a harness contract for the rule that verfies the validation data diff --git a/modules/4337/certora/specs/SignatureLengthCheck.spec b/modules/4337/certora/specs/SignatureLengthCheck.spec index ba80d9348..a25c3ad5b 100644 --- a/modules/4337/certora/specs/SignatureLengthCheck.spec +++ b/modules/4337/certora/specs/SignatureLengthCheck.spec @@ -5,7 +5,6 @@ methods { function combineBytes(bytes, bytes) external returns(bytes) envfree; // Safe Contract functions - function safeContract.containsContractSignature(bytes, uint256) external returns(bool) envfree; function safeContract.canonicalSignatureHash(bytes, uint256) external returns(bytes32) envfree; } @@ -13,7 +12,7 @@ methods { 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); + 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 @@ -21,7 +20,6 @@ rule signatureLengthCheckDirectly(bytes signatures, bytes gasGriefingData, uint2 rule canonicalHashBasedLengthCheck(bytes signatures, bytes griefedSignatures, uint256 threshold) { require safeContract.canonicalSignatureHash(signatures, threshold) == safeContract.canonicalSignatureHash(griefedSignatures, threshold); require signatures.length < griefedSignatures.length; - require safeContract.containsContractSignature(signatures, threshold); assert checkSignaturesLength(signatures, threshold) => !checkSignaturesLength(griefedSignatures, threshold); } From 4aac4f234e29fb11f0f69423a6520706c1a2e13e Mon Sep 17 00:00:00 2001 From: Shebin John Date: Tue, 16 Jul 2024 12:26:27 +0200 Subject: [PATCH 04/10] Updated the rules and conf --- .../certora/conf/SignatureLengthCheck.conf | 1 + modules/4337/certora/harnesses/Account.sol | 42 ++++++++----------- .../certora/specs/SignatureLengthCheck.spec | 11 +---- 3 files changed, 21 insertions(+), 33 deletions(-) diff --git a/modules/4337/certora/conf/SignatureLengthCheck.conf b/modules/4337/certora/conf/SignatureLengthCheck.conf index 055bca8a5..a18b86fde 100644 --- a/modules/4337/certora/conf/SignatureLengthCheck.conf +++ b/modules/4337/certora/conf/SignatureLengthCheck.conf @@ -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", diff --git a/modules/4337/certora/harnesses/Account.sol b/modules/4337/certora/harnesses/Account.sol index 812914337..51680a142 100644 --- a/modules/4337/certora/harnesses/Account.sol +++ b/modules/4337/certora/harnesses/Account.sol @@ -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 */ @@ -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 diff --git a/modules/4337/certora/specs/SignatureLengthCheck.spec b/modules/4337/certora/specs/SignatureLengthCheck.spec index a25c3ad5b..bff7104a4 100644 --- a/modules/4337/certora/specs/SignatureLengthCheck.spec +++ b/modules/4337/certora/specs/SignatureLengthCheck.spec @@ -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; From ef7b231ec338334323ef9c1e342ab878675d1ad6 Mon Sep 17 00:00:00 2001 From: Shebin John Date: Tue, 16 Jul 2024 16:16:53 +0200 Subject: [PATCH 05/10] Removed some dead code --- modules/4337/certora/harnesses/Safe4337ModuleHarness.sol | 4 ---- modules/4337/certora/specs/SignatureLengthCheck.spec | 1 - 2 files changed, 5 deletions(-) diff --git a/modules/4337/certora/harnesses/Safe4337ModuleHarness.sol b/modules/4337/certora/harnesses/Safe4337ModuleHarness.sol index 5552c88b0..f3253048e 100644 --- a/modules/4337/certora/harnesses/Safe4337ModuleHarness.sol +++ b/modules/4337/certora/harnesses/Safe4337ModuleHarness.sol @@ -8,8 +8,4 @@ contract Safe4337ModuleHarness is Safe4337Module { function checkSignaturesLength(bytes calldata signatures, uint256 threshold) external pure returns (bool) { return _checkSignaturesLength(signatures, threshold); } - - function combineBytes(bytes calldata signatures, bytes calldata data) external pure returns (bytes memory) { - return abi.encode(signatures, data); - } } diff --git a/modules/4337/certora/specs/SignatureLengthCheck.spec b/modules/4337/certora/specs/SignatureLengthCheck.spec index bff7104a4..251aeef1a 100644 --- a/modules/4337/certora/specs/SignatureLengthCheck.spec +++ b/modules/4337/certora/specs/SignatureLengthCheck.spec @@ -2,7 +2,6 @@ using Account as safeContract; methods { function checkSignaturesLength(bytes, uint256) external returns(bool) envfree; - function combineBytes(bytes, bytes) external returns(bytes) envfree; // Safe Contract functions function safeContract.canonicalSignatureHash(bytes, uint256) external returns(bytes32) envfree; From 636e169f93994856e4acca5b338e0df3a2211ec0 Mon Sep 17 00:00:00 2001 From: Shebin John Date: Tue, 16 Jul 2024 16:32:48 +0200 Subject: [PATCH 06/10] Updated comment --- modules/4337/certora/harnesses/Account.sol | 38 ++++++---------------- 1 file changed, 10 insertions(+), 28 deletions(-) diff --git a/modules/4337/certora/harnesses/Account.sol b/modules/4337/certora/harnesses/Account.sol index 51680a142..677382e26 100644 --- a/modules/4337/certora/harnesses/Account.sol +++ b/modules/4337/certora/harnesses/Account.sol @@ -55,40 +55,22 @@ contract Account is Safe { } /* - Actual Signature: - "0x" + - "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 efbeef" // length of bytes + data of bytes of signature 3 - - 0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c300000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000e7000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000012b000000000000000000000000000000000000000000000000000000000000000004deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000003efbeef + This function is used to calculate the hash of the signatures in a standard way. This will result in signatures having possible excess data to result in the same hash + as the same signatures without the excess data. This is required for formal verification. - With Excess Data Type 1: + Actual Signature: "0x" + - "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 + "0000000000000000000000000000000000000000000000000000000000000001 0000000000000000000000000000000000000000000000000000000000000041 00" + // encoded EIP-1271 signature 1 + "0000000000000000000000000000000000000000000000000000000000000004 deadbeef" // length of bytes + data of bytes of signature 1 - 0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c300000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000e7000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000012b000000000000000000000000000000000000000000000000000000000000000004deadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000003efbeefdeadbeefdeadbeefdeadbeef + 0x00000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000041000000000000000000000000000000000000000000000000000000000000000004deadbeef - With Excess Data Type 2: + With Excess Data: "0x" + - "0000000000000000000000000000000000000000000000000000000000000001 00000000000000000000000000000000000000000000000000000000000000c3 00" + // encoded EIP-1271 signature 1 - "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 efbeef" // length of bytes + data of bytes of signature 3 - - 0x000000000000000000000000000000000000000000000000000000000000000100000000000000000000000000000000000000000000000000000000000000c300000000000000000000000000000000000000000000000000000000000000000200000000000000000000000000000000000000000000000000000000000000eb000000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000012f000000000000000000000000000000000000000000000000000000000000000004deadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000024deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef0000000000000000000000000000000000000000000000000000000000000003efbeef + "0000000000000000000000000000000000000000000000000000000000000001 0000000000000000000000000000000000000000000000000000000000000041 00" + // encoded EIP-1271 signature 1 + "0000000000000000000000000000000000000000000000000000000000000004 deadbeefdeadbeef" // length of bytes + data of bytes of signature 1 + excess data - All three will have the same canonical hash: 0xe304234a47e4f89d0a95d9fafb42e9c3143e23e951d38add9f781c34f962deb7 + Both will have the same canonical hash: 0xc860b1a81652620308a8138a17ef5105d9b18e6e766516ffd3de9897260d1320 */ function canonicalSignatureHash(bytes calldata signatures, uint256 safeThreshold) public pure returns (bytes32 canonical) { uint256 dynamicOffset = safeThreshold * 0x41; From 3df8b0cfe283c3e7e9aa4ec5bc6119c4997bdf66 Mon Sep 17 00:00:00 2001 From: Shebin John Date: Tue, 16 Jul 2024 17:06:25 +0200 Subject: [PATCH 07/10] Comment Update --- modules/4337/certora/harnesses/Account.sol | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/modules/4337/certora/harnesses/Account.sol b/modules/4337/certora/harnesses/Account.sol index 677382e26..913c9aed8 100644 --- a/modules/4337/certora/harnesses/Account.sol +++ b/modules/4337/certora/harnesses/Account.sol @@ -63,12 +63,11 @@ contract Account is Safe { "0000000000000000000000000000000000000000000000000000000000000001 0000000000000000000000000000000000000000000000000000000000000041 00" + // encoded EIP-1271 signature 1 "0000000000000000000000000000000000000000000000000000000000000004 deadbeef" // length of bytes + data of bytes of signature 1 - 0x00000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000041000000000000000000000000000000000000000000000000000000000000000004deadbeef - With Excess Data: "0x" + "0000000000000000000000000000000000000000000000000000000000000001 0000000000000000000000000000000000000000000000000000000000000041 00" + // encoded EIP-1271 signature 1 - "0000000000000000000000000000000000000000000000000000000000000004 deadbeefdeadbeef" // length of bytes + data of bytes of signature 1 + excess data + "0000000000000000000000000000000000000000000000000000000000000004 deadbeef" // length of bytes + data of bytes of signature 1 + "ffffff" // excess data Both will have the same canonical hash: 0xc860b1a81652620308a8138a17ef5105d9b18e6e766516ffd3de9897260d1320 */ From f72107828db4c06d3a81ee1563dca721a54e845a Mon Sep 17 00:00:00 2001 From: Shebin John Date: Tue, 16 Jul 2024 17:17:34 +0200 Subject: [PATCH 08/10] Info added --- modules/4337/certora/conf/SignatureLengthCheck.conf | 2 +- modules/4337/certora/harnesses/Account.sol | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/modules/4337/certora/conf/SignatureLengthCheck.conf b/modules/4337/certora/conf/SignatureLengthCheck.conf index a18b86fde..b7090c48d 100644 --- a/modules/4337/certora/conf/SignatureLengthCheck.conf +++ b/modules/4337/certora/conf/SignatureLengthCheck.conf @@ -4,7 +4,7 @@ "certora/harnesses/Account.sol", ], "loop_iter": "3", - "optimistic_loop": true, + "optimistic_loop": true, "msg": "Safe4337Module: Signatures Length Check", "rule_sanity": "basic", "solc": "solc8.23", diff --git a/modules/4337/certora/harnesses/Account.sol b/modules/4337/certora/harnesses/Account.sol index 913c9aed8..c114e28f5 100644 --- a/modules/4337/certora/harnesses/Account.sol +++ b/modules/4337/certora/harnesses/Account.sol @@ -70,6 +70,8 @@ contract Account is Safe { "ffffff" // excess data Both will have the same canonical hash: 0xc860b1a81652620308a8138a17ef5105d9b18e6e766516ffd3de9897260d1320 + + For more details: https://docs.safe.global/advanced/smart-account-signatures */ function canonicalSignatureHash(bytes calldata signatures, uint256 safeThreshold) public pure returns (bytes32 canonical) { uint256 dynamicOffset = safeThreshold * 0x41; From 8f9aeea121e53f5eff19361ba22e58351e37c3be Mon Sep 17 00:00:00 2001 From: Shebin John Date: Wed, 17 Jul 2024 14:35:17 +0200 Subject: [PATCH 09/10] Removed signature length check --- modules/4337/certora/harnesses/Account.sol | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/modules/4337/certora/harnesses/Account.sol b/modules/4337/certora/harnesses/Account.sol index c114e28f5..5195465f4 100644 --- a/modules/4337/certora/harnesses/Account.sol +++ b/modules/4337/certora/harnesses/Account.sol @@ -74,7 +74,8 @@ contract Account is Safe { For more details: https://docs.safe.global/advanced/smart-account-signatures */ function canonicalSignatureHash(bytes calldata signatures, uint256 safeThreshold) public pure returns (bytes32 canonical) { - uint256 dynamicOffset = safeThreshold * 0x41; + uint256 dynamicOffsetStart = safeThreshold * 0x41; + uint256 dynamicOffset = dynamicOffsetStart; bytes memory staticPart = signatures[:dynamicOffset]; bytes memory dynamicPart = ""; @@ -86,11 +87,9 @@ contract Account is Safe { // the signature to the dynamic part. if (v == 0) { uint256 signatureOffset = uint256(bytes32(signatures[ptr + 0x20:])); - require(signatureOffset >= dynamicOffset, "Invalid signature offset"); + require(signatureOffset >= dynamicOffsetStart, "Invalid signature offset"); uint256 signatureLength = uint256(bytes32(signatures[signatureOffset:])); - require(signatureLength > 0, "Invalid signature length"); - bytes memory signature = signatures[signatureOffset+0x20:][:signatureLength]; // Make sure to update the static part so that the smart contract signature From fd3e6de9d56a0e77d7696f39a91d8474d28f7d77 Mon Sep 17 00:00:00 2001 From: Shebin John Date: Thu, 18 Jul 2024 10:27:41 +0200 Subject: [PATCH 10/10] Rule length updated --- modules/4337/certora/harnesses/Account.sol | 33 +++++-------------- .../certora/specs/SignatureLengthCheck.spec | 10 +++--- 2 files changed, 13 insertions(+), 30 deletions(-) diff --git a/modules/4337/certora/harnesses/Account.sol b/modules/4337/certora/harnesses/Account.sol index 5195465f4..d0e951253 100644 --- a/modules/4337/certora/harnesses/Account.sol +++ b/modules/4337/certora/harnesses/Account.sol @@ -54,28 +54,14 @@ contract Account is Safe { return uint48(bytes6(sigs[6:12])); } - /* - This function is used to calculate the hash of the signatures in a standard way. This will result in signatures having possible excess data to result in the same hash - as the same signatures without the excess data. This is required for formal verification. - - Actual Signature: - "0x" + - "0000000000000000000000000000000000000000000000000000000000000001 0000000000000000000000000000000000000000000000000000000000000041 00" + // encoded EIP-1271 signature 1 - "0000000000000000000000000000000000000000000000000000000000000004 deadbeef" // length of bytes + data of bytes of signature 1 - - With Excess Data: - "0x" + - "0000000000000000000000000000000000000000000000000000000000000001 0000000000000000000000000000000000000000000000000000000000000041 00" + // encoded EIP-1271 signature 1 - "0000000000000000000000000000000000000000000000000000000000000004 deadbeef" // length of bytes + data of bytes of signature 1 - "ffffff" // excess data - - Both will have the same canonical hash: 0xc860b1a81652620308a8138a17ef5105d9b18e6e766516ffd3de9897260d1320 - - For more details: https://docs.safe.global/advanced/smart-account-signatures + /** + * @dev This function encodes signature in a canonical format. This is required for formal verification. + * The canonical format ensures the signatures are tightly packed one after the other in order. + * + * For more details on signature encoding: https://docs.safe.global/advanced/smart-account-signatures */ - function canonicalSignatureHash(bytes calldata signatures, uint256 safeThreshold) public pure returns (bytes32 canonical) { - uint256 dynamicOffsetStart = safeThreshold * 0x41; - uint256 dynamicOffset = dynamicOffsetStart; + function canonicalSignature(bytes calldata signatures, uint256 safeThreshold) public pure returns (bytes memory canonical) { + uint256 dynamicOffset = safeThreshold * 0x41; bytes memory staticPart = signatures[:dynamicOffset]; bytes memory dynamicPart = ""; @@ -87,7 +73,6 @@ contract Account is Safe { // the signature to the dynamic part. if (v == 0) { uint256 signatureOffset = uint256(bytes32(signatures[ptr + 0x20:])); - require(signatureOffset >= dynamicOffsetStart, "Invalid signature offset"); uint256 signatureLength = uint256(bytes32(signatures[signatureOffset:])); bytes memory signature = signatures[signatureOffset+0x20:][:signatureLength]; @@ -105,8 +90,8 @@ contract Account is Safe { dynamicPart = abi.encodePacked(dynamicPart, signatureLength, signature); } } - canonical = keccak256(abi.encodePacked(staticPart, dynamicPart)); - } + canonical = abi.encodePacked(staticPart, dynamicPart); + } } // @notice This is a harness contract for the rule that verfies the validation data diff --git a/modules/4337/certora/specs/SignatureLengthCheck.spec b/modules/4337/certora/specs/SignatureLengthCheck.spec index 251aeef1a..119e58818 100644 --- a/modules/4337/certora/specs/SignatureLengthCheck.spec +++ b/modules/4337/certora/specs/SignatureLengthCheck.spec @@ -4,14 +4,12 @@ methods { function checkSignaturesLength(bytes, uint256) external returns(bool) envfree; // Safe Contract functions - function safeContract.canonicalSignatureHash(bytes, uint256) external returns(bytes32) envfree; + function safeContract.canonicalSignature(bytes, uint256) external returns(bytes) envfree; } // 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; - - assert checkSignaturesLength(signatures, threshold) => !checkSignaturesLength(griefedSignatures, threshold); +rule signatureCannotBeLongerThanCanonicalEncoding(bytes signatures, uint256 threshold) { + bytes canonical = safeContract.canonicalSignature(signatures, threshold); + assert checkSignaturesLength(signatures, threshold) => signatures.length <= canonical.length; }